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_obj {X Y : Top.{w}} (f : X ⟶ Y) (ℱ : X.presheaf C) : Y.presheaf C
with notationf _* ℱ
and forℱ : X.presheaf C
provide 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
.
The category of C
-valued presheaves on a (bundled) topological space X
.
Equations
- Top.presheaf C X = ((topological_space.opens ↥X)ᵒᵖ ⥤ C)
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 ⋙ ℱ
An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf along those maps.
Equations
The natural isomorphism between the pushforward of a presheaf along the identity continuous map and the original presheaf.
The natural isomorphism between the pushforward of a presheaf along the composition of two continuous maps and the corresponding pushforward of a pushforward.
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' := _}
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
Pulling back along continuous maps is functorial.
Equations
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) := {left := opposite.op ⟨⇑f '' ↑U, H⟩, right := subtype.cases_on U (λ (U_val : set ↥X) (U_property : is_open U_val) (H : is_open (⇑f '' ↑⟨U_val, U_property⟩)), id (λ {X Y : Top} (f : X ⟶ Y) (ℱ : Top.presheaf C Y) (U_val : set ↥X) (U_property : is_open U_val) (H : is_open (⇑f '' U_val)), {as := punit.star}) f ℱ U_val U_property H) H, hom := (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)))
The pullback along the identity is isomorphic to the original presheaf.
Equations
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' := _}
A homeomorphism of spaces gives an equivalence of categories of presheaves.
Equations
If H : X ≅ Y
is a homeomorphism,
then given an H _* ℱ ⟶ 𝒢
, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢
.
Equations
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₂
Pullback a presheaf on Y
along a continuous map f : X ⟶ Y
, obtaining a presheaf
on X
.
Equations
The pullback and pushforward along a continuous map are adjoint to each other.
Pulling back along a homeomorphism is the same as pushing forward along its inverse.
Pulling back along the inverse of a homeomorphism is the same as pushing forward along it.