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) [CategoryTheory.Category.{v, u} C] (X : TopCat) : Type (max u v w)

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

Equations

• TopCat.Presheaf C X = CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C

instance TopCat.instCategoryPresheaf (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) : CategoryTheory.Category.{max v w, max (max u v) w} (TopCat.Presheaf C X)

Equations

• TopCat.instCategoryPresheaf C X = inferInstanceAs (CategoryTheory.Category.{max v w, max (max u v) w} (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C))

@[simp]

theorem TopCat.Presheaf.comp_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {P : TopCat.Presheaf C X} {Q : TopCat.Presheaf C X} {R : TopCat.Presheaf C X} (f : P ⟶ Q) (g : Q ⟶ R) : (CategoryTheory.CategoryStruct.comp f g).app U = CategoryTheory.CategoryStruct.comp (f.app U) (g.app U)

theorem TopCat.Presheaf.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {P : TopCat.Presheaf C X} {Q : TopCat.Presheaf C X} {f : P ⟶ Q} {g : P ⟶ Q} (w : ∀ (U : TopologicalSpace.Opens ↑X), f.app { unop := U } = g.app { unop := U }) : f = g

def TopCat.Presheaf.attrSheaf_restrict : Lean.ParserDescr

attribute sheaf_restrict to mark lemmas related to restricting sheaves

Equations

• TopCat.Presheaf.attrSheaf_restrict = Lean.ParserDescr.node `TopCat.Presheaf.attrSheaf_restrict 1024 (Lean.ParserDescr.nonReservedSymbol "sheaf_restrict" false)

def TopCat.Presheaf.restrict_tac : Lean.ParserDescr

restrict_tac solves relations among subsets (copied from aesop cat)

Equations

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

def TopCat.Presheaf.restrict_tac? : Lean.ParserDescr

restrict_tac? passes along Try this from aesop

Equations

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

def TopCat.Presheaf.restrict {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {V : TopologicalSpace.Opens ↑X} (x : (CategoryTheory.forget C).obj (F.obj { unop := V })) {U : TopologicalSpace.Opens ↑X} (h : U ⟶ V) : (CategoryTheory.forget C).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

• TopCat.Presheaf.restrict x h = (F.map h.op) x

def AlgebraicGeometry.«term_|_ₕ_» : Lean.TrailingParserDescr

restriction of a section along an inclusion

Equations

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

def AlgebraicGeometry.«term_|_ₗ_⟪_⟫» : Lean.TrailingParserDescr

restriction of a section along a subset relation

Equations

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

@[reducible, inline]

abbrev TopCat.Presheaf.restrictOpen {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {V : TopologicalSpace.Opens ↑X} (x : (CategoryTheory.forget C).obj (F.obj { unop := V })) (U : TopologicalSpace.Opens ↑X) (e : autoParam (U ≤ V) _auto✝) : (CategoryTheory.forget C).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

• TopCat.Presheaf.restrictOpen x U e = TopCat.Presheaf.restrict x (CategoryTheory.homOfLE e)

def AlgebraicGeometry.«term_|__» : Lean.TrailingParserDescr

restriction of a section to open subset

Equations

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

theorem TopCat.Presheaf.restrict_restrict {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {U : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑X} {W : TopologicalSpace.Opens ↑X} (e₁ : U ≤ V) (e₂ : V ≤ W) (x : (CategoryTheory.forget C).obj (F.obj { unop := W })) : TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen x V e₂) U e₁ = TopCat.Presheaf.restrictOpen x U ⋯

theorem TopCat.Presheaf.map_restrict {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {G : TopCat.Presheaf C X} (e : F ⟶ G) {U : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑X} (h : U ≤ V) (x : (CategoryTheory.forget C).obj (F.obj { unop := V })) : (e.app { unop := U }) (TopCat.Presheaf.restrictOpen x U h) = TopCat.Presheaf.restrictOpen ((e.app { unop := V }) x) U h

def TopCat.Presheaf.pushforwardObj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C X) : TopCat.Presheaf C Y

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

Equations

• f _* ℱ = (TopologicalSpace.Opens.map f).op.comp ℱ

def TopCat.Presheaf.«term__*_» : Lean.TrailingParserDescr

push forward of a presheaf

Equations

• TopCat.Presheaf.«term__*_» = Lean.ParserDescr.trailingNode `TopCat.Presheaf.term__*_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " _* ") (Lean.ParserDescr.cat `term 81))

@[simp]

theorem TopCat.Presheaf.pushforwardObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : (f _* ℱ).obj U = ℱ.obj ((TopologicalSpace.Opens.map f).op.obj U)

@[simp]

theorem TopCat.Presheaf.pushforwardObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C X) {U : (TopologicalSpace.Opens ↑Y)ᵒᵖ} {V : (TopologicalSpace.Opens ↑Y)ᵒᵖ} (i : U ⟶ V) : (f _* ℱ).map i = ℱ.map ((TopologicalSpace.Opens.map f).op.map i)

def TopCat.Presheaf.pushforwardEq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (ℱ : TopCat.Presheaf C X) : f _* ℱ ≅ g _* ℱ

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

Equations

• TopCat.Presheaf.pushforwardEq h ℱ = CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.op (TopologicalSpace.Opens.mapIso f g h).symm) ℱ

theorem TopCat.Presheaf.pushforward_eq' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (ℱ : TopCat.Presheaf C X) : f _* ℱ = g _* ℱ

@[simp]

theorem TopCat.Presheaf.pushforwardEq_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : (TopCat.Presheaf.pushforwardEq h ℱ).hom.app U = ℱ.map (id (CategoryTheory.eqToHom ⋯).op)

theorem TopCat.Presheaf.pushforward_eq'_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : (CategoryTheory.eqToHom ⋯).app U = ℱ.map (CategoryTheory.eqToHom ⋯)

@[simp]

theorem TopCat.Presheaf.pushforwardEq_rfl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑Y) : (TopCat.Presheaf.pushforwardEq ⋯ ℱ).hom.app { unop := U } = CategoryTheory.CategoryStruct.id ((f _* ℱ).obj { unop := U })

theorem TopCat.Presheaf.pushforwardEq_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h₁ : f = g) (h₂ : f = g) (ℱ : TopCat.Presheaf C X) : TopCat.Presheaf.pushforwardEq h₁ ℱ = TopCat.Presheaf.pushforwardEq h₂ ℱ

def TopCat.Presheaf.Pushforward.id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) : CategoryTheory.CategoryStruct.id X _* ℱ ≅ ℱ

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

Equations

• TopCat.Presheaf.Pushforward.id ℱ = CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.op (TopologicalSpace.Opens.mapId X).symm) ℱ ≪≫ CategoryTheory.Functor.leftUnitor ℱ

theorem TopCat.Presheaf.Pushforward.id_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) : CategoryTheory.CategoryStruct.id X _* ℱ = ℱ

@[simp]

theorem TopCat.Presheaf.Pushforward.id_hom_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : Set ↑X) (p : IsOpen U) : (TopCat.Presheaf.Pushforward.id ℱ).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} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.Presheaf.Pushforward.id ℱ).hom.app U = ℱ.map (CategoryTheory.eqToHom ⋯)

@[simp]

theorem TopCat.Presheaf.Pushforward.id_inv_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : Set ↑X) (p : IsOpen U) : (TopCat.Presheaf.Pushforward.id ℱ).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} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp 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

• TopCat.Presheaf.Pushforward.comp ℱ f g = CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.op (TopologicalSpace.Opens.mapComp f g).symm) ℱ

theorem TopCat.Presheaf.Pushforward.comp_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g _* ℱ = g _* (f _* ℱ)

@[simp]

theorem TopCat.Presheaf.Pushforward.comp_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z)ᵒᵖ) : (TopCat.Presheaf.Pushforward.comp ℱ f g).hom.app U = CategoryTheory.CategoryStruct.id ((CategoryTheory.CategoryStruct.comp f g _* ℱ).obj U)

@[simp]

theorem TopCat.Presheaf.Pushforward.comp_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z)ᵒᵖ) : (TopCat.Presheaf.Pushforward.comp ℱ f g).inv.app U = CategoryTheory.CategoryStruct.id ((g _* (f _* ℱ)).obj U)

@[simp]

theorem TopCat.Presheaf.pushforwardMap_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : ℱ ⟶ 𝒢) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : (TopCat.Presheaf.pushforwardMap f α).app U = α.app ((TopologicalSpace.Opens.map f).op.obj U)

def TopCat.Presheaf.pushforwardMap {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : ℱ ⟶ 𝒢) : f _* ℱ ⟶ f _* 𝒢

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

Equations

• TopCat.Presheaf.pushforwardMap f α = { app := fun (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) => α.app ((TopologicalSpace.Opens.map f).op.obj U), naturality := ⋯ }

@[simp]

theorem TopCat.Presheaf.pullbackObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) {x : (TopologicalSpace.Opens ↑X)ᵒᵖ} {y : (TopologicalSpace.Opens ↑X)ᵒᵖ} (f : x ⟶ y) : (TopCat.Presheaf.pullbackObj f✝ ℱ).map f = CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f✝).op ℱ y) (CategoryTheory.CostructuredArrow.map f)

@[simp]

theorem TopCat.Presheaf.pullbackObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) (x : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.Presheaf.pullbackObj f ℱ).obj x = CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ x)

def TopCat.Presheaf.pullbackObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) : TopCat.Presheaf C X

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

• TopCat.Presheaf.pullbackObj f ℱ = (CategoryTheory.lan (TopologicalSpace.Opens.map f).op).obj ℱ

def TopCat.Presheaf.pullbackMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {ℱ : TopCat.Presheaf C Y} {𝒢 : TopCat.Presheaf C Y} (α : ℱ ⟶ 𝒢) : TopCat.Presheaf.pullbackObj f ℱ ⟶ TopCat.Presheaf.pullbackObj f 𝒢

Pulling back along continuous maps is functorial.

Equations

• TopCat.Presheaf.pullbackMap f α = (CategoryTheory.lan (TopologicalSpace.Opens.map f).op).map α

@[simp]

theorem TopCat.Presheaf.pullbackObjObjOfImageOpen_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (H : IsOpen (⇑f '' ↑U)) : (TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ U H).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ { unop := U }) (CategoryTheory.Limits.coconeOfDiagramTerminal { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty (CategoryTheory.CostructuredArrow (TopologicalSpace.Opens.map f).op { unop := U }))) => CategoryTheory.CostructuredArrow.homMk (CategoryTheory.homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ } (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ { unop := U }))

@[simp]

theorem TopCat.Presheaf.pullbackObjObjOfImageOpen_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (H : IsOpen (⇑f '' ↑U)) : (TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ U H).inv = (CategoryTheory.Limits.colimitOfDiagramTerminal { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty (CategoryTheory.CostructuredArrow (TopologicalSpace.Opens.map f).op { unop := U }))) => CategoryTheory.CostructuredArrow.homMk (CategoryTheory.homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ } (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ { unop := U })).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ { unop := U }))

def TopCat.Presheaf.pullbackObjObjOfImageOpen {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (H : IsOpen (⇑f '' ↑U)) : (TopCat.Presheaf.pullbackObj f ℱ).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.

def TopCat.Presheaf.Pullback.id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {Y : TopCat} (ℱ : TopCat.Presheaf C Y) : TopCat.Presheaf.pullbackObj (CategoryTheory.CategoryStruct.id Y) ℱ ≅ ℱ

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

Equations

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

theorem TopCat.Presheaf.Pullback.id_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {Y : TopCat} (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑Y) : (TopCat.Presheaf.Pullback.id ℱ).inv.app { unop := U } = CategoryTheory.Limits.colimit.ι (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id Y)).op ℱ { unop := U }) (CategoryTheory.CostructuredArrow.mk (CategoryTheory.eqToHom ⋯))

def TopCat.Presheaf.pushforward (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Functor (TopCat.Presheaf C X) (TopCat.Presheaf C Y)

The pushforward functor.

Equations

• TopCat.Presheaf.pushforward C f = { obj := TopCat.Presheaf.pushforwardObj f, map := @TopCat.Presheaf.pushforwardMap C inst X Y f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem TopCat.Presheaf.pushforward_map_app' (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : ℱ ⟶ 𝒢) {U : (TopologicalSpace.Opens ↑Y)ᵒᵖ} : ((TopCat.Presheaf.pushforward C f).map α).app U = α.app { unop := (TopologicalSpace.Opens.map f).obj U.unop }

theorem TopCat.Presheaf.id_pushforward (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} : TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.id X) = CategoryTheory.Functor.id (TopCat.Presheaf C X)

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝ ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑X✝)ᵒᵖ) : ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.obj G).obj X = G.obj { unop := (TopologicalSpace.Opens.map H.inv).obj X.unop }

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ ≅ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : ((TopCat.Presheaf.presheafEquivOfIso C H).counitIso.hom.app X✝).app X = X✝.map (CategoryTheory.eqToHom ⋯)

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝ ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X✝)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : ((TopCat.Presheaf.presheafEquivOfIso C H).functor.obj G).obj X = G.obj { unop := (TopologicalSpace.Opens.map H.hom).obj X.unop }

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ ≅ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑X✝¹)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑X✝¹)ᵒᵖ) : ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unit.app X)) (CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.map H.hom).map ((TopologicalSpace.Opens.mapMapIso H).symm.op.counitInv.app { unop := (TopologicalSpace.Opens.map H.inv).obj X.unop }).unop).op) (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unitInv.app { unop := (TopologicalSpace.Opens.map H.hom).obj ((TopologicalSpace.Opens.map H.inv).obj X.unop) })))

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ ≅ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : ((TopCat.Presheaf.presheafEquivOfIso C H).counitIso.inv.app X✝).app X = X✝.map (CategoryTheory.eqToHom ⋯)

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_inverse_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) : ∀ {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C} (α : X_1 ⟶ Y_1) (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.map α).app X_2 = α.app { unop := (TopologicalSpace.Opens.map H.inv).obj X_2.unop }

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_functor_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) : ∀ {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C} (α : X_1 ⟶ Y_1) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.map α).app X_2 = α.app { unop := (TopologicalSpace.Opens.map H.hom).obj X_2.unop }

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_functor_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) : ∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ} (f : X_1 ⟶ Y_1), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.obj G).map f = G.map ((TopologicalSpace.Opens.map H.hom).map f.unop).op

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) : ∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ} (f : X_1 ⟶ Y_1), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.obj G).map f = G.map ((TopologicalSpace.Opens.map H.inv).map f.unop).op

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ ≅ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑X✝¹)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑X✝¹)ᵒᵖ) : ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unit.app { unop := (TopologicalSpace.Opens.map H.hom).obj ((TopologicalSpace.Opens.map H.inv).obj X.unop) })) (CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.map H.hom).map ((TopologicalSpace.Opens.mapMapIso H).symm.op.counit.app { unop := (TopologicalSpace.Opens.map H.inv).obj X.unop }).unop).op) (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unitInv.app X)))

def TopCat.Presheaf.presheafEquivOfIso (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) : TopCat.Presheaf C X ≌ TopCat.Presheaf C Y

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

Equations

• TopCat.Presheaf.presheafEquivOfIso C H = (TopologicalSpace.Opens.mapMapIso H).symm.op.congrLeft

def TopCat.Presheaf.toPushforwardOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C Y} (α : H.hom _* ℱ ⟶ 𝒢) : ℱ ⟶ H.inv _* 𝒢

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

Equations

• TopCat.Presheaf.toPushforwardOfIso H α = ((TopCat.Presheaf.presheafEquivOfIso C H).toAdjunction.homEquiv ℱ 𝒢) α

@[simp]

theorem TopCat.Presheaf.toPushforwardOfIso_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C Y} (H₂ : H₁.hom _* ℱ ⟶ 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.Presheaf.toPushforwardOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (ℱ.map (CategoryTheory.eqToHom ⋯)) (H₂.app { unop := (TopologicalSpace.Opens.map H₁.inv).obj U.unop })

def TopCat.Presheaf.pushforwardToOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C Y} {𝒢 : TopCat.Presheaf C X} (H₂ : ℱ ⟶ H₁.hom _* 𝒢) : H₁.inv _* ℱ ⟶ 𝒢

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

Equations

• TopCat.Presheaf.pushforwardToOfIso H₁ H₂ = ((TopCat.Presheaf.presheafEquivOfIso C H₁.symm).toAdjunction.homEquiv ℱ 𝒢).symm H₂

@[simp]

theorem TopCat.Presheaf.pushforwardToOfIso_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C Y} {𝒢 : TopCat.Presheaf C X} (H₂ : ℱ ⟶ H₁.hom _* 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.Presheaf.pushforwardToOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (H₂.app { unop := (TopologicalSpace.Opens.map H₁.inv).obj U.unop }) (𝒢.map (CategoryTheory.eqToHom ⋯))

@[simp]

theorem TopCat.Presheaf.pullback_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X✝ ⟶ Y) {X : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C} {X' : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C} (f : X ⟶ X') (x : (TopologicalSpace.Opens ↑X✝)ᵒᵖ) : ((TopCat.Presheaf.pullback C f✝).map f).app x = CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f✝).op X x) { pt := CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f✝).op X' x), ι := { app := fun (i : CategoryTheory.CostructuredArrow (TopologicalSpace.Opens.map f✝).op x) => CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (f.app i.left) (((CategoryTheory.Lan.equiv (TopologicalSpace.Opens.map f✝).op X' (CategoryTheory.Lan.loc (TopologicalSpace.Opens.map f✝).op X')) (CategoryTheory.CategoryStruct.id (CategoryTheory.Lan.loc (TopologicalSpace.Opens.map f✝).op X'))).app i.left)) (CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f✝).op X' x) (CategoryTheory.CostructuredArrow.map i.hom)), naturality := ⋯ } }

def TopCat.Presheaf.pullback (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Functor (TopCat.Presheaf C Y) (TopCat.Presheaf C X)

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

Equations

• TopCat.Presheaf.pullback C f = CategoryTheory.lan (TopologicalSpace.Opens.map f).op

@[simp]

theorem TopCat.Presheaf.pullbackObj_eq_pullbackObj {C : Type u_1} [CategoryTheory.Category.{w, u_1} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) : (TopCat.Presheaf.pullback C f).obj ℱ = TopCat.Presheaf.pullbackObj f ℱ

@[simp]

theorem TopCat.Presheaf.pushforwardPullbackAdjunction_counit_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y✝) (Y : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (x : (TopologicalSpace.Opens ↑X)ᵒᵖ) : ((TopCat.Presheaf.pushforwardPullbackAdjunction C f).counit.app Y).app x = CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ((TopologicalSpace.Opens.map f).op.comp Y) x) { pt := Y.obj x, ι := { app := fun (i : CategoryTheory.CostructuredArrow (TopologicalSpace.Opens.map f).op x) => CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Y.obj { unop := (TopologicalSpace.Opens.map f).obj i.left.unop })) (Y.map i.hom), naturality := ⋯ } }

@[simp]

theorem TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X✝ ⟶ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (x : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : ((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app X).app x = CategoryTheory.Limits.colimit.ι (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op X { unop := (TopologicalSpace.Opens.map f).obj x.unop }) (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id { unop := (TopologicalSpace.Opens.map f).obj x.unop }))

def TopCat.Presheaf.pushforwardPullbackAdjunction (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) : TopCat.Presheaf.pullback C f ⊣ TopCat.Presheaf.pushforward C f

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

Equations

• TopCat.Presheaf.pushforwardPullbackAdjunction C f = CategoryTheory.Lan.adjunction C (TopologicalSpace.Opens.map f).op

def TopCat.Presheaf.pullbackHomIsoPushforwardInv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) : TopCat.Presheaf.pullback C H.hom ≅ TopCat.Presheaf.pushforward C H.inv

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

Equations

• TopCat.Presheaf.pullbackHomIsoPushforwardInv C H = (TopCat.Presheaf.pushforwardPullbackAdjunction C H.hom).leftAdjointUniq (TopCat.Presheaf.presheafEquivOfIso C H.symm).toAdjunction

def TopCat.Presheaf.pullbackInvIsoPushforwardHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) : TopCat.Presheaf.pullback C H.inv ≅ TopCat.Presheaf.pushforward C H.hom

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

Equations

• TopCat.Presheaf.pullbackInvIsoPushforwardHom C H = (TopCat.Presheaf.pushforwardPullbackAdjunction C H.inv).leftAdjointUniq (TopCat.Presheaf.presheafEquivOfIso C H).toAdjunction