mathlib documentation

topology.sheaves.presheaf

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

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.

@[nolint]
def Top.presheaf (C : Type u) [category_theory.category C] (X : Top) :
Type (max u v w)

The category of C-valued presheaves on a (bundled) topological space X.

Equations
Instances for Top.presheaf

A tactic to discharge goals of type U ≤ V for Top.presheaf.restrict_open

A tactic to discharge goals of type U ≤ V for Top.presheaf.restrict_open. Defaults to three iterations.

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
@[reducible]

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'

def Top.presheaf.pushforward_obj {C : Type u} [category_theory.category C] {X Y : Top} (f : X Y) (ℱ : Top.presheaf C X) :

Pushforward a presheaf on X along a continuous map f : X ⟶ Y, obtaining a presheaf on Y.

Equations
@[simp]
@[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) :
(f _* ℱ).map i = ℱ.map ((topological_space.opens.map f).op.map i)
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) :
f _* g _*

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) :
f _* = g _*
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) :
𝟙 X _*

The natural isomorphism between the pushforward of a presheaf along the identity continuous map and the original presheaf.

Equations
theorem Top.presheaf.pushforward.id_eq {C : Type u} [category_theory.category C] {X : Top} (ℱ : Top.presheaf C X) :
𝟙 X _* =
@[simp]
@[simp]
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) :
(f g) _* g _* (f _* ℱ)

The natural isomorphism between the pushforward of a presheaf along the composition of two continuous maps and the corresponding pushforward of a pushforward.

Equations
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) :
(f g) _* = g _* (f _* ℱ)
@[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)ᵒᵖ) :
(Top.presheaf.pushforward.comp f g).hom.app U = 𝟙 (((f g) _* ℱ).obj U)
@[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)ᵒᵖ) :
(Top.presheaf.pushforward.comp f g).inv.app U = 𝟙 ((g _* (f _* ℱ)).obj U)
def Top.presheaf.pushforward_map {C : Type u} [category_theory.category C] {X Y : Top} (f : X Y) {ℱ 𝒢 : Top.presheaf C X} (α : ℱ 𝒢) :
f _* f _* 𝒢

A morphism of presheaves gives rise to a morphisms of the pushforwards of those presheaves.

Equations
@[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)ᵒᵖ) :
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) :

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

If f '' U is open, then f⁻¹ℱ U ≅ ℱ (f '' U).

Equations
@[simp]

A homeomorphism of spaces gives an equivalence of categories of presheaves.

Equations
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 _* 𝒢) :
H.inv _* 𝒢

If H : X ≅ Y is a homeomorphism, then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.

Equations
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 _* 𝒢) :
H₁.inv _* 𝒢

If H : X ≅ Y is a homeomorphism, then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.

Equations

Pullback a presheaf on Y along a continuous map f : X ⟶ Y, obtaining a presheaf on X.

Equations