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.

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

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

Equations
Instances for Top.presheaf
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]
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)ᵒᵖ) :
(f _* ℱ).obj U = ℱ.obj ((topological_space.opens.map f).op.obj U)
@[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 _*
@[simp]
@[simp]
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]
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) :
@[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) :
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
def Top.presheaf.pushforward (C : Type u) [category_theory.category C] {X Y : Top} (f : X Y) :

The pushforward functor.

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)ᵒᵖ} :

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
@[simp]
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
@[simp]
noncomputable def Top.presheaf.pullback (C : Type u) [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : Top} (f : X Y) :

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.

Equations