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.

source

@[instance]

def Top.presheaf.category (C : Type u) [category_theory.category C] (X : Top) :

category_theory.category (Top.presheaf C X)

source

def Top.presheaf (C : Type u) [category_theory.category C] (X : Top) :

Type (max v u)

Equations

Top.presheaf C X = ((topological_space.opens ↥X)ᵒᵖ ⥤ C)

source

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

Top.presheaf C Y

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

Equations

f _* ℱ = (topological_space.opens.map f).op ⋙ ℱ

source

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

source

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

source

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 _* ℱ

Equations

Top.presheaf.pushforward_eq h ℱ = category_theory.iso_whisker_right (category_theory.nat_iso.op (topological_space.opens.map_iso f g h).symm) ℱ

source

@[simp]

theorem Top.presheaf.pushforward_eq_hom_app {C : Type u} [category_theory.category C] {X Y : Top} {f g : X ⟶ Y} (h : f = g) (ℱ : Top.presheaf C X) (U : (topological_space.opens ↥Y)ᵒᵖ) :

(Top.presheaf.pushforward_eq h ℱ).hom.app U = ℱ.map (id (category_theory.eq_to_hom _).op)

source

@[simp]

theorem Top.presheaf.pushforward_eq_rfl {C : Type u} [category_theory.category C] {X Y : Top} (f : X ⟶ Y) (ℱ : Top.presheaf C X) (U : topological_space.opens ↥Y) :

(Top.presheaf.pushforward_eq rfl ℱ).hom.app (opposite.op U) = 𝟙 ((f _* ℱ).obj (opposite.op U))

source

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

Top.presheaf.pushforward_eq h₁ ℱ = Top.presheaf.pushforward_eq h₂ ℱ

source

def Top.presheaf.pushforward.id {C : Type u} [category_theory.category C] {X : Top} (ℱ : Top.presheaf C X) :

𝟙 X _* ℱ ≅ ℱ

Equations

Top.presheaf.pushforward.id ℱ = category_theory.iso_whisker_right (category_theory.nat_iso.op (topological_space.opens.map_id X).symm) ℱ ≪≫ category_theory.functor.left_unitor ℱ

source

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

(Top.presheaf.pushforward.id ℱ).hom.app (opposite.op ⟨U, p⟩) = ℱ.map (𝟙 (opposite.op ⟨U, p⟩))

source

@[simp]

theorem Top.presheaf.pushforward.id_hom_app {C : Type u} [category_theory.category C] {X : Top} (ℱ : Top.presheaf C X) (U : (topological_space.opens ↥X)ᵒᵖ) :

(Top.presheaf.pushforward.id ℱ).hom.app U = ℱ.map (category_theory.eq_to_hom _)

source

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

(Top.presheaf.pushforward.id ℱ).inv.app (opposite.op ⟨U, p⟩) = ℱ.map (𝟙 (opposite.op ⟨U, p⟩))

source

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 _* ℱ)

Equations

Top.presheaf.pushforward.comp ℱ f g = category_theory.iso_whisker_right (category_theory.nat_iso.op (topological_space.opens.map_comp f g).symm) ℱ

source

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

source

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

source

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

Top.presheaf.pushforward_map f α = {app := λ (U : (topological_space.opens ↥Y)ᵒᵖ), α.app ((topological_space.opens.map f).op.obj U), naturality' := _}

source

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

(Top.presheaf.pushforward_map f α).app U = α.app ((topological_space.opens.map f).op.obj U)