# mathlibdocumentation

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

• pushforward_obj {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : X.presheaf C) : Y.presheaf C with notation f _* ℱ and for ℱ : X.presheaf C provide the natural isomorphisms
• pushforward.id : (𝟙 X) _* ℱ ≅ ℱ
• pushforward.comp : (f ≫ g) _* ℱ ≅ g _* (f _* ℱ) along with their @[simp] lemmas.
@[instance]
def Top.presheaf.category (C : Type u) (X : Top) :
def Top.presheaf (C : Type u) (X : Top) :
Type (max v u)

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

Equations
def Top.presheaf.pushforward_obj {C : Type u} {X Y : Top} (f : X Y) (ℱ : X) :
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} {X Y : Top} (f : X Y) (ℱ : X) (U : ᵒᵖ) :
(f _* ℱ).obj U = ℱ.obj U)
@[simp]
theorem Top.presheaf.pushforward_obj_map {C : Type u} {X Y : Top} (f : X Y) (ℱ : X) {U V : ᵒᵖ} (i : U V) :
(f _* ℱ).map i = ℱ.map i)
def Top.presheaf.pushforward_eq {C : Type u} {X Y : Top} {f g : X Y} (h : f = g) (ℱ : X) :
f _* g _*

An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf along those maps.

Equations
@[simp]
theorem Top.presheaf.pushforward_eq_hom_app {C : Type u} {X Y : Top} {f g : X Y} (h : f = g) (ℱ : X) (U : ᵒᵖ) :
U = ℱ.map
@[simp]
theorem Top.presheaf.pushforward_eq_rfl {C : Type u} {X Y : Top} (f : X Y) (ℱ : X) (U : topological_space.opens Y) :
= 𝟙 ((f _* ℱ).obj (opposite.op U))
theorem Top.presheaf.pushforward_eq_eq {C : Type u} {X Y : Top} {f g : X Y} (h₁ h₂ : f = g) (ℱ : X) :
def Top.presheaf.pushforward.id {C : Type u} {X : Top} (ℱ : X) :
𝟙 X _*

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

Equations
@[simp]
theorem Top.presheaf.pushforward.id_hom_app' {C : Type u} {X : Top} (ℱ : X) (U : set X) (p : is_open U) :
(opposite.op U, p⟩) = ℱ.map (𝟙 (opposite.op U, p⟩))
@[simp]
theorem Top.presheaf.pushforward.id_hom_app {C : Type u} {X : Top} (ℱ : X) (U : ᵒᵖ) :
@[simp]
theorem Top.presheaf.pushforward.id_inv_app' {C : Type u} {X : Top} (ℱ : X) (U : set X) (p : is_open U) :
(opposite.op U, p⟩) = ℱ.map (𝟙 (opposite.op U, p⟩))
def Top.presheaf.pushforward.comp {C : Type u} {X : Top} (ℱ : 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
@[simp]
theorem Top.presheaf.pushforward.comp_hom_app {C : Type u} {X : Top} (ℱ : X) {Y Z : Top} (f : X Y) (g : Y Z) (U : ᵒᵖ) :
.hom.app U = 𝟙 (((f g) _* ℱ).obj U)
@[simp]
theorem Top.presheaf.pushforward.comp_inv_app {C : Type u} {X : Top} (ℱ : X) {Y Z : Top} (f : X Y) (g : Y Z) (U : ᵒᵖ) :
.inv.app U = 𝟙 ((g _* (f _* ℱ)).obj U)
def Top.presheaf.pushforward_map {C : Type u} {X Y : Top} (f : X Y) {ℱ 𝒢 : 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} {X Y : Top} (f : X Y) {ℱ 𝒢 : X} (α : ℱ 𝒢) (U : ᵒᵖ) :
U = α.app U)