Presheaves on a topological space
We define presheaf C X simply as (opens X)ᵒᵖ ⥤ C,
and inherit the category structure with natural transformations as morphisms.
We define
pushforward {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : X.presheaf C) : Y.presheaf Cwith notationf _* ℱand forℱ : X.presheaf Cprovide the natural isomorphisms- `pushforward.id : (𝟙 X) _* ℱ ≅ ℱ``
pushforward.comp : (f ≫ g) _* ℱ ≅ g _* (f _* ℱ)along with their@[simp]lemmas.
Equations
- Top.presheaf C X = ((topological_space.opens ↥X)ᵒᵖ ⥤ C)
@[instance]
def
Top.presheaf.pushforward
{C : Type u}
[category_theory.category C]
{X Y : Top} :
(X ⟶ Y) → Top.presheaf C X → Top.presheaf C Y
Equations
- f _* ℱ = (topological_space.opens.map f).op ⋙ ℱ
def
Top.presheaf.pushforward_eq
{C : Type u}
[category_theory.category C]
{X Y : Top}
{f g : X ⟶ Y}
(h : f = g)
(ℱ : Top.presheaf C X) :
Equations
theorem
Top.presheaf.pushforward_eq_eq
{C : Type u}
[category_theory.category C]
{X Y : Top}
{f g : X ⟶ Y}
(h₁ h₂ : f = g)
(ℱ : Top.presheaf C X) :
def
Top.presheaf.pushforward.id
{C : Type u}
[category_theory.category C]
{X : Top}
(ℱ : Top.presheaf C X) :
@[simp]
theorem
Top.presheaf.pushforward.id_hom_app'
{C : Type u}
[category_theory.category C]
{X : Top}
(ℱ : Top.presheaf C X)
(U : set ↥X)
(p : is_open U) :
(Top.presheaf.pushforward.id ℱ).hom.app (opposite.op ⟨U, p⟩) = ℱ.map (𝟙 (opposite.op ⟨U, p⟩))
@[simp]
theorem
Top.presheaf.pushforward.id_hom_app
{C : Type u}
[category_theory.category C]
{X : Top}
(ℱ : Top.presheaf C X)
(U : (topological_space.opens ↥X)ᵒᵖ) :
(Top.presheaf.pushforward.id ℱ).hom.app U = ℱ.map (category_theory.eq_to_hom _)
@[simp]
theorem
Top.presheaf.pushforward.id_inv_app'
{C : Type u}
[category_theory.category C]
{X : Top}
(ℱ : Top.presheaf C X)
(U : set ↥X)
(p : is_open U) :
(Top.presheaf.pushforward.id ℱ).inv.app (opposite.op ⟨U, p⟩) = ℱ.map (𝟙 (opposite.op ⟨U, p⟩))
def
Top.presheaf.pushforward.comp
{C : Type u}
[category_theory.category C]
{X : Top}
(ℱ : Top.presheaf C X)
{Y Z : Top}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
@[simp]
theorem
Top.presheaf.pushforward.comp_hom_app
{C : Type u}
[category_theory.category C]
{X : Top}
(ℱ : Top.presheaf C X)
{Y Z : Top}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(U : (topological_space.opens ↥Z)ᵒᵖ) :
@[simp]
theorem
Top.presheaf.pushforward.comp_inv_app
{C : Type u}
[category_theory.category C]
{X : Top}
(ℱ : Top.presheaf C X)
{Y Z : Top}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(U : (topological_space.opens ↥Z)ᵒᵖ) :