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

def Top.presheaf (C : Type u) [category_theory.category C] :
TopType (max v u)

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

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)

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

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

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