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] (X : Top) :
Type (max v u)
Equations
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)
@[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)ᵒᵖ) :