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

• Given {X Y : TopCat.{w}} and f : X ⟶ Y, we define TopCat.Presheaf.pushforward C f : X.Presheaf C ⥤ Y.Presheaf C, with notation f _* ℱ for ℱ : X.Presheaf C. 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 pullback C f : Y.Presheaf C ⥤ X.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 (Opposite.op U) = g.app (Opposite.op 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 (Opposite.op V))) {U : TopologicalSpace.Opens ↑X} (h : U ⟶ V) : (CategoryTheory.forget C).obj (F.obj (Opposite.op 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 (Opposite.op V))) (U : TopologicalSpace.Opens ↑X) (e : autoParam (U ≤ V) _auto✝) : (CategoryTheory.forget C).obj (F.obj (Opposite.op 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 (Opposite.op 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 (Opposite.op V))) : (e.app (Opposite.op U)) (TopCat.Presheaf.restrictOpen x U h) = TopCat.Presheaf.restrictOpen ((e.app (Opposite.op V)) x) U h

@[simp]

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

@[simp]

theorem TopCat.Presheaf.pushforward_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) : ∀ {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C} (α : X_1 ⟶ Y_1) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.pushforward C f).map α).app X_2 = α.app (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop X_2)))

@[simp]

theorem TopCat.Presheaf.pushforward_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X✝ ⟶ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X✝)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : ((TopCat.Presheaf.pushforward C f).obj G).obj X = G.obj (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop X)))

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 = (CategoryTheory.whiskeringLeft (TopologicalSpace.Opens ↑Y)ᵒᵖ (TopologicalSpace.Opens ↑X)ᵒᵖ C).obj (TopologicalSpace.Opens.map f).op

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

push forward of a presheaf

Equations

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

@[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 (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop U)))

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)

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

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

Equations

• TopCat.Presheaf.Pushforward.id ℱ = CategoryTheory.Iso.refl ((TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.id X)).obj ℱ)

@[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 = CategoryTheory.CategoryStruct.id (((TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.id X)).obj ℱ).obj U)

@[simp]

theorem TopCat.Presheaf.Pushforward.id_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.Presheaf.Pushforward.id ℱ).inv.app U = CategoryTheory.CategoryStruct.id (ℱ.obj U)

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

def TopCat.Presheaf.Pushforward.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : TopCat.Presheaf C X) : (TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.comp f g)).obj ℱ ≅ (TopCat.Presheaf.pushforward C g).obj ((TopCat.Presheaf.pushforward C f).obj ℱ)

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.Iso.refl ((TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.comp f g)).obj ℱ)

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

@[simp]

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

@[simp]

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

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) : (TopCat.Presheaf.pushforward C f).obj ℱ ≅ (TopCat.Presheaf.pushforward C g).obj ℱ

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) : (TopCat.Presheaf.pushforward C f).obj ℱ = (TopCat.Presheaf.pushforward C g).obj ℱ

@[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 (CategoryTheory.eqToHom ⋯)

@[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 (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X)))

@[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_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 (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X)))).unop).op) (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unitInv.app (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X)))))))

@[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 (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj (Opposite.unop X_2)))

@[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 (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj (Opposite.unop X)))

@[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 (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_2)))

@[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 (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X)))))) (CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.map H.hom).map ((TopologicalSpace.Opens.mapMapIso H).symm.op.counit.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X)))).unop).op) (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unitInv.app X)))

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

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} (α : (TopCat.Presheaf.pushforward C H.hom).obj ℱ ⟶ 𝒢) : ℱ ⟶ (TopCat.Presheaf.pushforward C H.inv).obj 𝒢

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₂ : (TopCat.Presheaf.pushforward C H₁.hom).obj ℱ ⟶ 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.Presheaf.toPushforwardOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (ℱ.map (CategoryTheory.eqToHom ⋯)) (H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).obj (Opposite.unop U))))

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₂ : ℱ ⟶ (TopCat.Presheaf.pushforward C H₁.hom).obj 𝒢) : (TopCat.Presheaf.pushforward C H₁.inv).obj ℱ ⟶ 𝒢

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₂ : ℱ ⟶ (TopCat.Presheaf.pushforward C H₁.hom).obj 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.Presheaf.pushforwardToOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).obj (Opposite.unop U)))) (𝒢.map (CategoryTheory.eqToHom ⋯))

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 = (TopologicalSpace.Opens.map f).op.lan

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 = (TopologicalSpace.Opens.map f).op.lanAdjunction C

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

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.pullback C f).obj ℱ).obj (Opposite.op U) ≅ ℱ.obj (Opposite.op { 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.