Presheaves on a topological space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define presheaf C X simply as (opens X)ᵒᵖ ⥤ C,
and inherit the category structure with natural transformations as morphisms.
We define
pushforward_obj {X Y : Top.{w}} (f : X ⟶ Y) (ℱ : X.presheaf C) : Y.presheaf Cwith notationf _* ℱand forℱ : X.presheaf Cprovide the natural isomorphismspushforward.id : (𝟙 X) _* ℱ ≅ ℱpushforward.comp : (f ≫ g) _* ℱ ≅ g _* (f _* ℱ)along with their@[simp]lemmas.
We also define the functors pushforward and pullback between the categories
X.presheaf C and Y.presheaf C, and provide their adjunction at
pushforward_pullback_adjunction.
@[protected, instance]
@[nolint]
The category of C-valued presheaves on a (bundled) topological space X.
Equations
- Top.presheaf C X = ((topological_space.opens ↥X)ᵒᵖ ⥤ C)
def
Top.presheaf.restrict
{X : Top}
{C : Type u_2}
[category_theory.category C]
[category_theory.concrete_category C]
{F : Top.presheaf C X}
{V : topological_space.opens ↥X}
(x : ↥(F.obj (opposite.op V)))
{U : topological_space.opens ↥X}
(h : U ⟶ V) :
↥(F.obj (opposite.op U))
The restriction of a section along an inclusion of open sets.
For x : F.obj (op V), we provide the notation x |_ₕ i (h stands for hom) for i : U ⟶ V,
and the notation x |_ₗ U ⟪i⟫ (l stands for le) for i : U ≤ V.
Equations
- Top.presheaf.restrict x h = ⇑(F.map h.op) x
@[reducible]
def
Top.presheaf.restrict_open
{X : Top}
{C : Type u_2}
[category_theory.category C]
[category_theory.concrete_category C]
{F : Top.presheaf C X}
{V : topological_space.opens ↥X}
(x : ↥(F.obj (opposite.op V)))
(U : topological_space.opens ↥X)
(e : U ≤ V . "restrict_tac'") :
↥(F.obj (opposite.op U))
The restriction of a section along an inclusion of open sets.
For x : F.obj (op V), we provide the notation x |_ U, where the proof U ≤ V is inferred by
the tactic Top.presheaf.restrict_tac'
@[simp]
theorem
Top.presheaf.restrict_restrict
{X : Top}
{C : Type u_2}
[category_theory.category C]
[category_theory.concrete_category C]
{F : Top.presheaf C X}
{U V W : topological_space.opens ↥X}
(e₁ : U ≤ V)
(e₂ : V ≤ W)
(x : ↥(F.obj (opposite.op W))) :
Top.presheaf.restrict_open (Top.presheaf.restrict_open x V e₂) U e₁ = Top.presheaf.restrict_open x U _
@[simp]
theorem
Top.presheaf.map_restrict
{X : Top}
{C : Type u_2}
[category_theory.category C]
[category_theory.concrete_category C]
{F G : Top.presheaf C X}
(e : F ⟶ G)
{U V : topological_space.opens ↥X}
(h : U ≤ V)
(x : ↥(F.obj (opposite.op V))) :
⇑(e.app (opposite.op U)) (Top.presheaf.restrict_open x U h) = Top.presheaf.restrict_open (⇑(e.app (opposite.op V)) x) U h
def
Top.presheaf.pushforward_obj
{C : Type u}
[category_theory.category C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C X) :
Top.presheaf C Y
Pushforward a presheaf on X along a continuous map f : X ⟶ Y, obtaining a presheaf
on Y.
Equations
- f _* ℱ = (topological_space.opens.map f).op ⋙ ℱ
@[simp]
theorem
Top.presheaf.pushforward_obj_obj
{C : Type u}
[category_theory.category C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C X)
(U : (topological_space.opens ↥Y)ᵒᵖ) :
@[simp]
theorem
Top.presheaf.pushforward_obj_map
{C : Type u}
[category_theory.category C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C X)
{U V : (topological_space.opens ↥Y)ᵒᵖ}
(i : U ⟶ V) :
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) :
An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf along those maps.
Equations
theorem
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) :
@[simp]
theorem
Top.presheaf.pushforward_eq_hom_app
{C : Type u}
[category_theory.category C]
{X Y : Top}
{f g : X ⟶ Y}
(h : f = g)
(ℱ : Top.presheaf C X)
(U : (topological_space.opens ↥Y)ᵒᵖ) :
(Top.presheaf.pushforward_eq h ℱ).hom.app U = ℱ.map (id (category_theory.eq_to_hom _).op)
theorem
Top.presheaf.pushforward_eq'_hom_app
{C : Type u}
[category_theory.category C]
{X Y : Top}
{f g : X ⟶ Y}
(h : f = g)
(ℱ : Top.presheaf C X)
(U : (topological_space.opens ↥Y)ᵒᵖ) :
(category_theory.eq_to_hom _).app U = ℱ.map (category_theory.eq_to_hom _)
@[simp]
theorem
Top.presheaf.pushforward_eq_rfl
{C : Type u}
[category_theory.category C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C X)
(U : topological_space.opens ↥Y) :
(Top.presheaf.pushforward_eq rfl ℱ).hom.app (opposite.op U) = 𝟙 ((f _* ℱ).obj (opposite.op U))
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) :
The natural isomorphism between the pushforward of a presheaf along the identity continuous map and the original presheaf.
theorem
Top.presheaf.pushforward.id_eq
{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 {carrier := U, is_open' := p}) = ℱ.map (𝟙 (opposite.op {carrier := U, is_open' := 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 {carrier := U, is_open' := p}) = ℱ.map (𝟙 (opposite.op {carrier := U, is_open' := 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) :
The natural isomorphism between the pushforward of a presheaf along the composition of two continuous maps and the corresponding pushforward of a pushforward.
theorem
Top.presheaf.pushforward.comp_eq
{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)ᵒᵖ) :
def
Top.presheaf.pushforward_map
{C : Type u}
[category_theory.category C]
{X Y : Top}
(f : X ⟶ Y)
{ℱ 𝒢 : Top.presheaf C X}
(α : ℱ ⟶ 𝒢) :
A morphism of presheaves gives rise to a morphisms of the pushforwards of those presheaves.
Equations
- Top.presheaf.pushforward_map f α = {app := λ (U : (topological_space.opens ↥Y)ᵒᵖ), α.app ((topological_space.opens.map f).op.obj U), naturality' := _}
@[simp]
theorem
Top.presheaf.pushforward_map_app
{C : Type u}
[category_theory.category C]
{X Y : Top}
(f : X ⟶ Y)
{ℱ 𝒢 : Top.presheaf C X}
(α : ℱ ⟶ 𝒢)
(U : (topological_space.opens ↥Y)ᵒᵖ) :
(Top.presheaf.pushforward_map f α).app U = α.app ((topological_space.opens.map f).op.obj U)
@[simp]
theorem
Top.presheaf.pullback_obj_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C Y)
(x : (topological_space.opens ↥X)ᵒᵖ) :
@[simp]
theorem
Top.presheaf.pullback_obj_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C Y)
(x y : (topological_space.opens ↥X)ᵒᵖ)
(f_1 : x ⟶ y) :
noncomputable
def
Top.presheaf.pullback_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C Y) :
Top.presheaf C X
Pullback a presheaf on Y along a continuous map f : X ⟶ Y, obtaining a presheaf on X.
This is defined in terms of left Kan extensions, which is just a fancy way of saying "take the colimits over the open sets whose preimage contains U".
Equations
noncomputable
def
Top.presheaf.pullback_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
{ℱ 𝒢 : Top.presheaf C Y}
(α : ℱ ⟶ 𝒢) :
Pulling back along continuous maps is functorial.
Equations
@[simp]
theorem
Top.presheaf.pullback_obj_obj_of_image_open_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C Y)
(U : topological_space.opens ↥X)
(H : is_open (⇑f '' ↑U)) :
(Top.presheaf.pullback_obj_obj_of_image_open f ℱ U H).hom = category_theory.limits.colimit.desc (category_theory.Lan.diagram (topological_space.opens.map f).op ℱ (opposite.op U)) (category_theory.limits.cocone_of_diagram_terminal {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty (category_theory.costructured_arrow (topological_space.opens.map f).op (opposite.op U)))), category_theory.costructured_arrow.hom_mk (category_theory.hom_of_le _).op _, fac' := _, uniq' := _} (category_theory.Lan.diagram (topological_space.opens.map f).op ℱ (opposite.op U)))
@[simp]
theorem
Top.presheaf.pullback_obj_obj_of_image_open_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C Y)
(U : topological_space.opens ↥X)
(H : is_open (⇑f '' ↑U)) :
(Top.presheaf.pullback_obj_obj_of_image_open f ℱ U H).inv = (category_theory.limits.colimit_of_diagram_terminal {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty (category_theory.costructured_arrow (topological_space.opens.map f).op (opposite.op U)))), category_theory.costructured_arrow.hom_mk (category_theory.hom_of_le _).op _, fac' := _, uniq' := _} (category_theory.Lan.diagram (topological_space.opens.map f).op ℱ (opposite.op U))).desc (category_theory.limits.colimit.cocone (category_theory.Lan.diagram (topological_space.opens.map f).op ℱ (opposite.op U)))
noncomputable
def
Top.presheaf.pullback_obj_obj_of_image_open
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C Y)
(U : topological_space.opens ↥X)
(H : is_open (⇑f '' ↑U)) :
(Top.presheaf.pullback_obj f ℱ).obj (opposite.op U) ≅ ℱ.obj (opposite.op {carrier := ⇑f '' ↑U, is_open' := H})
If f '' U is open, then f⁻¹ℱ U ≅ ℱ (f '' U).
Equations
- Top.presheaf.pullback_obj_obj_of_image_open f ℱ U H = let x : category_theory.costructured_arrow (topological_space.opens.map f).op (opposite.op U) := category_theory.costructured_arrow.mk (category_theory.hom_of_le _).op in (category_theory.limits.colimit.is_colimit (category_theory.Lan.diagram (topological_space.opens.map f).op ℱ (opposite.op U))).cocone_point_unique_up_to_iso (category_theory.limits.colimit_of_diagram_terminal {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty (category_theory.costructured_arrow (topological_space.opens.map f).op (opposite.op U)))), category_theory.costructured_arrow.hom_mk (id (category_theory.hom_of_le _).op) _, fac' := _, uniq' := _} (category_theory.Lan.diagram (topological_space.opens.map f).op ℱ (opposite.op U)))
noncomputable
def
Top.presheaf.pullback.id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{Y : Top}
(ℱ : Top.presheaf C Y) :
Top.presheaf.pullback_obj (𝟙 Y) ℱ ≅ ℱ
The pullback along the identity is isomorphic to the original presheaf.
Equations
theorem
Top.presheaf.pullback.id_inv_app
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{Y : Top}
(ℱ : Top.presheaf C Y)
(U : topological_space.opens ↥Y) :
def
Top.presheaf.pushforward
(C : Type u)
[category_theory.category C]
{X Y : Top}
(f : X ⟶ Y) :
Top.presheaf C X ⥤ Top.presheaf C Y
The pushforward functor.
Equations
- Top.presheaf.pushforward C f = {obj := Top.presheaf.pushforward_obj f, map := Top.presheaf.pushforward_map f, map_id' := _, map_comp' := _}
@[simp]
theorem
Top.presheaf.pushforward_map_app'
(C : Type u)
[category_theory.category C]
{X Y : Top}
(f : X ⟶ Y)
{ℱ 𝒢 : Top.presheaf C X}
(α : ℱ ⟶ 𝒢)
{U : (topological_space.opens ↥Y)ᵒᵖ} :
((Top.presheaf.pushforward C f).map α).app U = α.app (opposite.op ((topological_space.opens.map f).obj (opposite.unop U)))
theorem
Top.presheaf.id_pushforward
(C : Type u)
[category_theory.category C]
{X : Top} :
Top.presheaf.pushforward C (𝟙 X) = 𝟭 (Top.presheaf C X)
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_unit_iso_hom_app_app
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(X_1 : (topological_space.opens ↥X)ᵒᵖ ⥤ C)
(X_2 : (topological_space.opens ↥X)ᵒᵖ) :
((Top.presheaf.presheaf_equiv_of_iso C H).unit_iso.hom.app X_1).app X_2 = X_1.map (category_theory.eq_to_hom _) ≫ X_1.map ((topological_space.opens.map H.hom).map (category_theory.eq_to_hom _)).op ≫ X_1.map (category_theory.eq_to_hom _)
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_unit_iso_inv_app_app
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(X_1 : (topological_space.opens ↥X)ᵒᵖ ⥤ C)
(X_2 : (topological_space.opens ↥X)ᵒᵖ) :
((Top.presheaf.presheaf_equiv_of_iso C H).unit_iso.inv.app X_1).app X_2 = X_1.map (category_theory.eq_to_hom _) ≫ X_1.map ((topological_space.opens.map H.hom).map (category_theory.eq_to_hom _)).op ≫ X_1.map (category_theory.eq_to_hom _)
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_functor_obj_map
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(G : (topological_space.opens ↥X)ᵒᵖ ⥤ C)
(_x _x_1 : (topological_space.opens ↥Y)ᵒᵖ)
(f : _x ⟶ _x_1) :
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_counit_iso_hom_app_app
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(X_1 : (topological_space.opens ↥Y)ᵒᵖ ⥤ C)
(X_2 : (topological_space.opens ↥Y)ᵒᵖ) :
((Top.presheaf.presheaf_equiv_of_iso C H).counit_iso.hom.app X_1).app X_2 = X_1.map (category_theory.eq_to_hom _)
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_functor_obj_obj
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(G : (topological_space.opens ↥X)ᵒᵖ ⥤ C)
(X_1 : (topological_space.opens ↥Y)ᵒᵖ) :
((Top.presheaf.presheaf_equiv_of_iso C H).functor.obj G).obj X_1 = G.obj (opposite.op ((topological_space.opens.map H.hom).obj (opposite.unop X_1)))
def
Top.presheaf.presheaf_equiv_of_iso
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y) :
Top.presheaf C X ≌ Top.presheaf C Y
A homeomorphism of spaces gives an equivalence of categories of presheaves.
Equations
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_inverse_obj_map
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(G : (topological_space.opens ↥Y)ᵒᵖ ⥤ C)
(_x _x_1 : (topological_space.opens ↥X)ᵒᵖ)
(f : _x ⟶ _x_1) :
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_inverse_map_app
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(G H_1 : (topological_space.opens ↥Y)ᵒᵖ ⥤ C)
(α : G ⟶ H_1)
(X_1 : (topological_space.opens ↥X)ᵒᵖ) :
((Top.presheaf.presheaf_equiv_of_iso C H).inverse.map α).app X_1 = α.app (opposite.op ((topological_space.opens.map H.inv).obj (opposite.unop X_1)))
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_inverse_obj_obj
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(G : (topological_space.opens ↥Y)ᵒᵖ ⥤ C)
(X_1 : (topological_space.opens ↥X)ᵒᵖ) :
((Top.presheaf.presheaf_equiv_of_iso C H).inverse.obj G).obj X_1 = G.obj (opposite.op ((topological_space.opens.map H.inv).obj (opposite.unop X_1)))
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_functor_map_app
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(G H_1 : (topological_space.opens ↥X)ᵒᵖ ⥤ C)
(α : G ⟶ H_1)
(X_1 : (topological_space.opens ↥Y)ᵒᵖ) :
((Top.presheaf.presheaf_equiv_of_iso C H).functor.map α).app X_1 = α.app (opposite.op ((topological_space.opens.map H.hom).obj (opposite.unop X_1)))
@[simp]
theorem
Top.presheaf.presheaf_equiv_of_iso_counit_iso_inv_app_app
(C : Type u)
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
(X_1 : (topological_space.opens ↥Y)ᵒᵖ ⥤ C)
(X_2 : (topological_space.opens ↥Y)ᵒᵖ) :
((Top.presheaf.presheaf_equiv_of_iso C H).counit_iso.inv.app X_1).app X_2 = X_1.map (category_theory.eq_to_hom _)
def
Top.presheaf.to_pushforward_of_iso
{C : Type u}
[category_theory.category C]
{X Y : Top}
(H : X ≅ Y)
{ℱ : Top.presheaf C X}
{𝒢 : Top.presheaf C Y}
(α : H.hom _* ℱ ⟶ 𝒢) :
If H : X ≅ Y is a homeomorphism,
then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.
Equations
@[simp]
theorem
Top.presheaf.to_pushforward_of_iso_app
{C : Type u}
[category_theory.category C]
{X Y : Top}
(H₁ : X ≅ Y)
{ℱ : Top.presheaf C X}
{𝒢 : Top.presheaf C Y}
(H₂ : H₁.hom _* ℱ ⟶ 𝒢)
(U : (topological_space.opens ↥X)ᵒᵖ) :
(Top.presheaf.to_pushforward_of_iso H₁ H₂).app U = ℱ.map (category_theory.eq_to_hom _) ≫ H₂.app (opposite.op ((topological_space.opens.map H₁.inv).obj (opposite.unop U)))
def
Top.presheaf.pushforward_to_of_iso
{C : Type u}
[category_theory.category C]
{X Y : Top}
(H₁ : X ≅ Y)
{ℱ : Top.presheaf C Y}
{𝒢 : Top.presheaf C X}
(H₂ : ℱ ⟶ H₁.hom _* 𝒢) :
If H : X ≅ Y is a homeomorphism,
then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.
Equations
- Top.presheaf.pushforward_to_of_iso H₁ H₂ = ⇑(((Top.presheaf.presheaf_equiv_of_iso C H₁.symm).to_adjunction.hom_equiv ℱ 𝒢).symm) H₂
@[simp]
theorem
Top.presheaf.pushforward_to_of_iso_app
{C : Type u}
[category_theory.category C]
{X Y : Top}
(H₁ : X ≅ Y)
{ℱ : Top.presheaf C Y}
{𝒢 : Top.presheaf C X}
(H₂ : ℱ ⟶ H₁.hom _* 𝒢)
(U : (topological_space.opens ↥X)ᵒᵖ) :
(Top.presheaf.pushforward_to_of_iso H₁ H₂).app U = H₂.app (opposite.op ((topological_space.opens.map H₁.inv).obj (opposite.unop U))) ≫ 𝒢.map (category_theory.eq_to_hom _)
@[simp]
theorem
Top.presheaf.pullback_map_app
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(X_1 X' : (topological_space.opens ↥Y)ᵒᵖ ⥤ C)
(f_1 : X_1 ⟶ X')
(x : (topological_space.opens ↥X)ᵒᵖ) :
((Top.presheaf.pullback C f).map f_1).app x = category_theory.limits.colimit.desc (category_theory.Lan.diagram (topological_space.opens.map f).op X_1 x) {X := category_theory.limits.colimit (category_theory.Lan.diagram (topological_space.opens.map f).op X' x) _, ι := {app := λ (i : category_theory.costructured_arrow (topological_space.opens.map f).op x), (f_1.app i.left ≫ category_theory.limits.colimit.ι (category_theory.Lan.diagram (topological_space.opens.map f).op X' (opposite.op ((topological_space.opens.map f).obj (opposite.unop i.left)))) (category_theory.costructured_arrow.mk (𝟙 (opposite.op ((topological_space.opens.map f).obj (opposite.unop i.left))))) ≫ 𝟙 (category_theory.limits.colimit (category_theory.Lan.diagram (topological_space.opens.map f).op X' (opposite.op ((topological_space.opens.map f).obj (opposite.unop i.left)))))) ≫ category_theory.limits.colimit.pre (category_theory.Lan.diagram (topological_space.opens.map f).op X' x) (category_theory.costructured_arrow.map i.hom), naturality' := _}}
noncomputable
def
Top.presheaf.pullback
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y) :
Top.presheaf C Y ⥤ Top.presheaf C X
Pullback a presheaf on Y along a continuous map f : X ⟶ Y, obtaining a presheaf
on X.
Equations
@[simp]
theorem
Top.presheaf.pullback_obj_eq_pullback_obj
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C Y) :
(Top.presheaf.pullback C f).obj ℱ = Top.presheaf.pullback_obj f ℱ
noncomputable
def
Top.presheaf.pushforward_pullback_adjunction
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y) :
The pullback and pushforward along a continuous map are adjoint to each other.
@[simp]
theorem
Top.presheaf.pushforward_pullback_adjunction_counit_app_app
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(Y_1 : (topological_space.opens ↥X)ᵒᵖ ⥤ C)
(x : (topological_space.opens ↥X)ᵒᵖ) :
((Top.presheaf.pushforward_pullback_adjunction C f).counit.app Y_1).app x = category_theory.limits.colimit.desc (category_theory.Lan.diagram (topological_space.opens.map f).op ((topological_space.opens.map f).op ⋙ Y_1) x) {X := Y_1.obj x, ι := {app := λ (i : category_theory.costructured_arrow (topological_space.opens.map f).op x), 𝟙 (Y_1.obj (opposite.op ((topological_space.opens.map f).obj (opposite.unop i.left)))) ≫ Y_1.map i.hom, naturality' := _}}
@[simp]
theorem
Top.presheaf.pushforward_pullback_adjunction_unit_app_app
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(X_1 : (topological_space.opens ↥Y)ᵒᵖ ⥤ C)
(x : (topological_space.opens ↥Y)ᵒᵖ) :
((Top.presheaf.pushforward_pullback_adjunction C f).unit.app X_1).app x = category_theory.limits.colimit.ι (category_theory.Lan.diagram (topological_space.opens.map f).op X_1 (opposite.op ((topological_space.opens.map f).obj (opposite.unop x)))) (category_theory.costructured_arrow.mk (𝟙 (opposite.op ((topological_space.opens.map f).obj (opposite.unop x)))))
noncomputable
def
Top.presheaf.pullback_hom_iso_pushforward_inv
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(H : X ≅ Y) :
Pulling back along a homeomorphism is the same as pushing forward along its inverse.
noncomputable
def
Top.presheaf.pullback_inv_iso_pushforward_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(H : X ≅ Y) :
Pulling back along the inverse of a homeomorphism is the same as pushing forward along it.