# Presheaves on a topological space #

We define TopCat.Presheaf C X simply as (TopologicalSpace.Opens X)ᵒᵖ ⥤ C, and inherit the category structure with natural transformations as morphisms.

We define

• TopCat.Presheaf.pushforwardObj {X Y : Top.{w}} (f : X ⟶ Y) (ℱ : X.Presheaf C) : Y.Presheaf C with notation f _* ℱ and for ℱ : X.Presheaf C provide the natural isomorphisms
• TopCat.Presheaf.Pushforward.id : (𝟙 X) _* ℱ ≅ ℱ
• TopCat.Presheaf.Pushforward.comp : (f ≫ g) _* ℱ ≅ g _* (f _* ℱ) along with their @[simp] lemmas.

We also define the functors pushforward and pullback between the categories X.Presheaf C and Y.Presheaf C, and provide their adjunction at TopCat.Presheaf.pushforwardPullbackAdjunction.

def TopCat.Presheaf (C : Type u) (X : TopCat) :
Type (max u v w)

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

Equations
Instances For
instance TopCat.instCategoryPresheaf (C : Type u) (X : TopCat) :
Equations
@[simp]
theorem TopCat.Presheaf.comp_app {C : Type u} {X : TopCat} {U : } {P : } {Q : } {R : } (f : P Q) (g : Q R) :
.app U = CategoryTheory.CategoryStruct.comp (f.app U) (g.app U)
theorem TopCat.Presheaf.ext {C : Type u} {X : TopCat} {P : } {Q : } {f : P Q} {g : P Q} (w : ∀ (U : ), f.app { unop := U } = g.app { unop := U }) :
f = g

attribute sheaf_restrict to mark lemmas related to restricting sheaves

Equations
Instances For

restrict_tac solves relations among subsets (copied from aesop cat)

Equations
• One or more equations did not get rendered due to their size.
Instances For

restrict_tac? passes along Try this from aesop

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.restrict {X : TopCat} {C : Type u_1} [] {F : } {V : } (x : .obj (F.obj { unop := V })) {U : } (h : U V) :
.obj (F.obj { unop := U })

The restriction of a section along an inclusion of open sets. For x : F.obj (op V), we provide the notation x |_ₕ i (h stands for hom) for i : U ⟶ V, and the notation x |_ₗ U ⟪i⟫ (l stands for le) for i : U ≤ V.

Equations
• = (F.map h.op) x
Instances For

restriction of a section along an inclusion

Equations
• One or more equations did not get rendered due to their size.
Instances For

restriction of a section along a subset relation

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev TopCat.Presheaf.restrictOpen {X : TopCat} {C : Type u_1} [] {F : } {V : } (x : .obj (F.obj { unop := V })) (U : ) (e : autoParam (U V) _auto✝) :
.obj (F.obj { unop := U })

The restriction of a section along an inclusion of open sets. For x : F.obj (op V), we provide the notation x |_ U, where the proof U ≤ V is inferred by the tactic Top.presheaf.restrict_tac'

Equations
Instances For

restriction of a section to open subset

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TopCat.Presheaf.restrict_restrict {X : TopCat} {C : Type u_1} [] {F : } {U : } {V : } {W : } (e₁ : U V) (e₂ : V W) (x : .obj (F.obj { unop := W })) :
theorem TopCat.Presheaf.map_restrict {X : TopCat} {C : Type u_1} [] {F : } {G : } (e : F G) {U : } {V : } (h : U V) (x : .obj (F.obj { unop := V })) :
(e.app { unop := U }) () = TopCat.Presheaf.restrictOpen ((e.app { unop := V }) x) U h
def TopCat.Presheaf.pushforwardObj {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) :

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

Equations
• f _* = .op.comp
Instances For

push forward of a presheaf

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopCat.Presheaf.pushforwardObj_obj {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) (U : ) :
(f _* ).obj U = .obj (.op.obj U)
@[simp]
theorem TopCat.Presheaf.pushforwardObj_map {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) {U : } {V : } (i : U V) :
(f _* ).map i = .map (.op.map i)
def TopCat.Presheaf.pushforwardEq {C : Type u} {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h : f = g) (ℱ : ) :
f _* g _*

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

Equations
Instances For
theorem TopCat.Presheaf.pushforward_eq' {C : Type u} {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h : f = g) (ℱ : ) :
f _* = g _*
@[simp]
theorem TopCat.Presheaf.pushforwardEq_hom_app {C : Type u} {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h : f = g) (ℱ : ) (U : ) :
.hom.app U = .map (id .op)
theorem TopCat.Presheaf.pushforward_eq'_hom_app {C : Type u} {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h : f = g) (ℱ : ) (U : ) :
.app U = .map
@[simp]
theorem TopCat.Presheaf.pushforwardEq_rfl {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) (U : ) :
.hom.app { unop := U } = CategoryTheory.CategoryStruct.id ((f _* ).obj { unop := U })
theorem TopCat.Presheaf.pushforwardEq_eq {C : Type u} {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h₁ : f = g) (h₂ : f = g) (ℱ : ) :
def TopCat.Presheaf.Pushforward.id {C : Type u} {X : TopCat} (ℱ : ) :

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

Equations
Instances For
theorem TopCat.Presheaf.Pushforward.id_eq {C : Type u} {X : TopCat} (ℱ : ) :
@[simp]
theorem TopCat.Presheaf.Pushforward.id_hom_app' {C : Type u} {X : TopCat} (ℱ : ) (U : Set X) (p : ) :
.hom.app { unop := { carrier := U, is_open' := p } } = .map (CategoryTheory.CategoryStruct.id { unop := { carrier := U, is_open' := p } })
@[simp]
theorem TopCat.Presheaf.Pushforward.id_hom_app {C : Type u} {X : TopCat} (ℱ : ) (U : ) :
.hom.app U = .map
@[simp]
theorem TopCat.Presheaf.Pushforward.id_inv_app' {C : Type u} {X : TopCat} (ℱ : ) (U : Set X) (p : ) :
.inv.app { unop := { carrier := U, is_open' := p } } = .map (CategoryTheory.CategoryStruct.id { unop := { carrier := U, is_open' := p } })
def TopCat.Presheaf.Pushforward.comp {C : Type u} {X : TopCat} (ℱ : ) {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :
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
Instances For
theorem TopCat.Presheaf.Pushforward.comp_eq {C : Type u} {X : TopCat} (ℱ : ) {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :
= g _* (f _* )
@[simp]
theorem TopCat.Presheaf.Pushforward.comp_hom_app {C : Type u} {X : TopCat} (ℱ : ) {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : ) :
().hom.app U = CategoryTheory.CategoryStruct.id (().obj U)
@[simp]
theorem TopCat.Presheaf.Pushforward.comp_inv_app {C : Type u} {X : TopCat} (ℱ : ) {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : ) :
().inv.app U = CategoryTheory.CategoryStruct.id ((g _* (f _* )).obj U)
@[simp]
theorem TopCat.Presheaf.pushforwardMap_app {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) {ℱ : } {𝒢 : } (α : 𝒢) (U : ) :
.app U = α.app (.op.obj U)
def TopCat.Presheaf.pushforwardMap {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) {ℱ : } {𝒢 : } (α : 𝒢) :
f _* f _* 𝒢

A morphism of presheaves gives rise to a morphisms of the pushforwards of those presheaves.

Equations
• = { app := fun (U : ) => α.app (.op.obj U), naturality := }
Instances For
@[simp]
theorem TopCat.Presheaf.pullbackObj_map {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) {x : } {y : } (f : x y) :
().map f =
@[simp]
theorem TopCat.Presheaf.pullbackObj_obj {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) (x : ) :
def TopCat.Presheaf.pullbackObj {C : Type u} {X : TopCat} {Y : TopCat} (f : X 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
• = .obj
Instances For
def TopCat.Presheaf.pullbackMap {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) {ℱ : } {𝒢 : } (α : 𝒢) :

Pulling back along continuous maps is functorial.

Equations
• = .map α
Instances For
@[simp]
theorem TopCat.Presheaf.pullbackObjObjOfImageOpen_hom {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) (U : ) (H : IsOpen (f '' U)) :
@[simp]
theorem TopCat.Presheaf.pullbackObjObjOfImageOpen_inv {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) (U : ) (H : IsOpen (f '' U)) :
def TopCat.Presheaf.pullbackObjObjOfImageOpen {C : Type u} {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) (U : ) (H : IsOpen (f '' U)) :
.obj { unop := U } .obj { unop := { carrier := f '' U, is_open' := H } }

If f '' U is open, then f⁻¹ℱ U ≅ ℱ (f '' U).

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.Pullback.id {C : Type u} {Y : TopCat} (ℱ : ) :

The pullback along the identity is isomorphic to the original presheaf.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TopCat.Presheaf.Pullback.id_inv_app {C : Type u} {Y : TopCat} (ℱ : ) (U : ) :
.inv.app { unop := U } =
def TopCat.Presheaf.pushforward (C : Type u) {X : TopCat} {Y : TopCat} (f : X Y) :

The pushforward functor.

Equations
Instances For
@[simp]
theorem TopCat.Presheaf.pushforward_map_app' (C : Type u) {X : TopCat} {Y : TopCat} (f : X Y) {ℱ : } {𝒢 : } (α : 𝒢) {U : } :
(.map α).app U = α.app { unop := .obj U.unop }
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj (C : Type u) {X : TopCat} {Y : TopCat} (H : X✝ Y) (G : ) (X : ()ᵒᵖ) :
(.inverse.obj G).obj X = G.obj { unop := ().obj X.unop }
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app (C : Type u) {X : TopCat} {Y : TopCat} (H : X✝¹ Y) (X : ) (X : ) :
(.counitIso.hom.app X✝).app X = X✝.map
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj (C : Type u) {X : TopCat} {Y : TopCat} (H : X✝ Y) (G : ) (X : ) :
(.functor.obj G).obj X = G.obj { unop := ().obj X.unop }
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app (C : Type u) {X : TopCat} {Y : TopCat} (H : X✝¹ Y) (X : ) (X : ()ᵒᵖ) :
(.unitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.comp (X✝.map (.symm.op.unit.app X)) (CategoryTheory.CategoryStruct.comp (X✝.map (().map (.symm.op.counitInv.app { unop := ().obj X.unop }).unop).op) (X✝.map (.symm.op.unitInv.app { unop := ().obj (().obj X.unop) })))
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app (C : Type u) {X : TopCat} {Y : TopCat} (H : X✝¹ Y) (X : ) (X : ) :
(.counitIso.inv.app X✝).app X = X✝.map
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_inverse_map_app (C : Type u) {X : TopCat} {Y : TopCat} (H : X Y) :
∀ {X_1 Y_1 : } (α : X_1 Y_1) (X_2 : ), (.inverse.map α).app X_2 = α.app { unop := ().obj X_2.unop }
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_functor_map_app (C : Type u) {X : TopCat} {Y : TopCat} (H : X Y) :
∀ {X_1 Y_1 : } (α : X_1 Y_1) (X_2 : ), (.functor.map α).app X_2 = α.app { unop := ().obj X_2.unop }
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_functor_obj_map (C : Type u) {X : TopCat} {Y : TopCat} (H : X Y) (G : ) :
∀ {X_1 Y_1 : } (f : X_1 Y_1), (.functor.obj G).map f = G.map (().map f.unop).op
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map (C : Type u) {X : TopCat} {Y : TopCat} (H : X Y) (G : ) :
∀ {X_1 Y_1 : } (f : X_1 Y_1), (.inverse.obj G).map f = G.map (().map f.unop).op
@[simp]
theorem TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app (C : Type u) {X : TopCat} {Y : TopCat} (H : X✝¹ Y) (X : ) (X : ()ᵒᵖ) :
(.unitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.comp (X✝.map (.symm.op.unit.app { unop := ().obj (().obj X.unop) })) (CategoryTheory.CategoryStruct.comp (X✝.map (().map (.symm.op.counit.app { unop := ().obj X.unop }).unop).op) (X✝.map (.symm.op.unitInv.app X)))
def TopCat.Presheaf.presheafEquivOfIso (C : Type u) {X : TopCat} {Y : TopCat} (H : X Y) :

A homeomorphism of spaces gives an equivalence of categories of presheaves.

Equations
• = .symm.op.congrLeft
Instances For
def TopCat.Presheaf.toPushforwardOfIso {C : Type u} {X : TopCat} {Y : TopCat} (H : X Y) {ℱ : } {𝒢 : } (α : H.hom _* 𝒢) :
H.inv _* 𝒢

If H : X ≅ Y is a homeomorphism, then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.

Equations
• = (.toAdjunction.homEquiv 𝒢) α
Instances For
@[simp]
theorem TopCat.Presheaf.toPushforwardOfIso_app {C : Type u} {X : TopCat} {Y : TopCat} (H₁ : X Y) {ℱ : } {𝒢 : } (H₂ : H₁.hom _* 𝒢) (U : ) :
.app U = CategoryTheory.CategoryStruct.comp (.map ) (H₂.app { unop := ().obj U.unop })
def TopCat.Presheaf.pushforwardToOfIso {C : Type u} {X : TopCat} {Y : TopCat} (H₁ : X Y) {ℱ : } {𝒢 : } (H₂ : H₁.hom _* 𝒢) :
H₁.inv _* 𝒢

If H : X ≅ Y is a homeomorphism, then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.

Equations
• = (().toAdjunction.homEquiv 𝒢).symm H₂
Instances For
@[simp]
theorem TopCat.Presheaf.pushforwardToOfIso_app {C : Type u} {X : TopCat} {Y : TopCat} (H₁ : X Y) {ℱ : } {𝒢 : } (H₂ : H₁.hom _* 𝒢) (U : ) :
.app U = CategoryTheory.CategoryStruct.comp (H₂.app { unop := ().obj U.unop }) (𝒢.map )
@[simp]
theorem TopCat.Presheaf.pullback_map_app (C : Type u) {X : TopCat} {Y : TopCat} (f : X✝ Y) {X : } {X' : } (f : X X') (x : ()ᵒᵖ) :
(().map f).app x = CategoryTheory.Limits.colimit.desc () { pt := , ι := { app := fun (i : ) => CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (f.app i.left) ((() ()).app i.left)) (), naturality := } }
def TopCat.Presheaf.pullback (C : Type u) {X : TopCat} {Y : TopCat} (f : X Y) :

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

Equations
Instances For
@[simp]
theorem TopCat.Presheaf.pullbackObj_eq_pullbackObj {C : Type u_1} [] {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : ) :
().obj =
@[simp]
theorem TopCat.Presheaf.pushforwardPullbackAdjunction_counit_app_app (C : Type u) {X : TopCat} {Y : TopCat} (f : X Y✝) (Y : ) (x : ) :
(.counit.app Y).app x = CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram .op (.op.comp Y) x) { pt := Y.obj x, ι := { app := fun (i : ) => CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Y.obj { unop := .obj i.left.unop })) (Y.map i.hom), naturality := } }
@[simp]
theorem TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app (C : Type u) {X : TopCat} {Y : TopCat} (f : X✝ Y) (X : ) (x : ) :

The pullback and pushforward along a continuous map are adjoint to each other.

Equations
Instances For

Pulling back along a homeomorphism is the same as pushing forward along its inverse.

Equations
• = .leftAdjointUniq ().toAdjunction
Instances For

Pulling back along the inverse of a homeomorphism is the same as pushing forward along it.

Equations
• = .leftAdjointUniq .toAdjunction
Instances For