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.pullbackPushforwardAdjunction.

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

@[implicit_reducible]

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

Equations

• TopCat.instCategoryPresheaf C X = inferInstanceAs (CategoryTheory.Category.{max ?u.19 ?u.20, max (max ?u.18 ?u.19) ?u.20} (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 Q R : 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 Q : Presheaf C X} {f g : P ⟶ Q} (w : ∀ (U : TopologicalSpace.Opens ↑X), f.app (Opposite.op U) = g.app (Opposite.op U)) : f = g

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

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} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {F : Presheaf C X} {V : TopologicalSpace.Opens ↑X} (x : CategoryTheory.ToType (F.obj (Opposite.op V))) {U : TopologicalSpace.Opens ↑X} (h : U ⟶ V) : CategoryTheory.ToType (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 = (CategoryTheory.ConcreteCategory.hom (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} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {F : Presheaf C X} {V : TopologicalSpace.Opens ↑X} (x : CategoryTheory.ToType (F.obj (Opposite.op V))) (U : TopologicalSpace.Opens ↑X) (e : U ≤ V := by restrict_tac) : CategoryTheory.ToType (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} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {F : Presheaf C X} {U V W : TopologicalSpace.Opens ↑X} (e₁ : U ≤ V) (e₂ : V ≤ W) (x : CategoryTheory.ToType (F.obj (Opposite.op W))) : restrictOpen (restrictOpen x V e₂) U e₁ = restrictOpen x U ⋯

theorem TopCat.Presheaf.map_restrict {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {F G : Presheaf C X} (e : F ⟶ G) {U V : TopologicalSpace.Opens ↑X} (h : U ≤ V) (x : CategoryTheory.ToType (F.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (e.app (Opposite.op U))) (restrictOpen x U h) = restrictOpen ((CategoryTheory.ConcreteCategory.hom (e.app (Opposite.op V))) x) U h

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

The pushforward functor.

Equations

• TopCat.Presheaf.pushforward C f = (CategoryTheory.Functor.whiskeringLeft (TopologicalSpace.Opens ↑Y)ᵒᵖ (TopologicalSpace.Opens ↑X)ᵒᵖ C).obj (TopologicalSpace.Opens.map f).op

@[simp]

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.«term__*_» : Lean.TrailingParserDescr

push forward of a presheaf

Equations

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

@[simp]

theorem TopCat.Presheaf.pushforward_map_app' (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) {ℱ 𝒢 : Presheaf C X} (α : ℱ ⟶ 𝒢) {U : (TopologicalSpace.Opens ↑Y)ᵒᵖ} : ((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) : pushforward C (CategoryTheory.CategoryStruct.id X) = CategoryTheory.Functor.id (Presheaf C X)

def TopCat.Presheaf.Pushforward.id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : Presheaf C X) : (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} (ℱ : Presheaf C X) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (id ℱ).hom.app U = CategoryTheory.CategoryStruct.id (((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} (ℱ : Presheaf C X) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (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} (ℱ : Presheaf C X) : (pushforward C (CategoryTheory.CategoryStruct.id X)).obj ℱ = ℱ

def TopCat.Presheaf.Pushforward.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : Presheaf C X) : (pushforward C (CategoryTheory.CategoryStruct.comp f g)).obj ℱ ≅ (pushforward C g).obj ((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 Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : Presheaf C X) : (pushforward C (CategoryTheory.CategoryStruct.comp f g)).obj ℱ = (pushforward C g).obj ((pushforward C f).obj ℱ)

@[simp]

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

def TopCat.Presheaf.pushforwardEq {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : TopCat} {f g : X ⟶ Y} (h : f = g) (ℱ : Presheaf C X) : (pushforward C f).obj ℱ ≅ (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.Functor.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 Y : TopCat} {f g : X ⟶ Y} (h : f = g) (ℱ : Presheaf C X) : (pushforward C f).obj ℱ = (pushforward C g).obj ℱ

@[simp]

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

def TopCat.Presheaf.presheafEquivOfIso (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) : Presheaf C X ≌ 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

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_functor_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) {X✝ Y✝ : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C} (α : X✝ ⟶ Y✝) (X✝¹ : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : ((presheafEquivOfIso C H).functor.map α).app X✝¹ = α.app (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 Y : TopCat} (H : X ≅ Y) {X✝ Y✝ : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C} (α : X✝ ⟶ Y✝) (X✝¹ : (TopologicalSpace.Opens ↑X)ᵒᵖ) : ((presheafEquivOfIso C H).inverse.map α).app X✝¹ = α.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X✝¹)))

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_functor_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) {X✝ Y✝ : (TopologicalSpace.Opens ↑Y)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((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_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) (X✝ : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X✝¹ : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : ((presheafEquivOfIso C H).counitIso.hom.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 Y : TopCat} (H : X ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) {X✝ Y✝ : (TopologicalSpace.Opens ↑X)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((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_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) (X✝ : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (X✝¹ : (TopologicalSpace.Opens ↑X)ᵒᵖ) : ((presheafEquivOfIso C H).unitIso.hom.app X✝).app X✝¹ = X✝.map (CategoryTheory.eqToHom ⋯)

@[simp]

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

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X✝ : (TopologicalSpace.Opens ↑X)ᵒᵖ) : ((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_functor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (X✝ : (TopologicalSpace.Opens ↑Y)ᵒᵖ) : ((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_unitIso_inv_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) (X✝ : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (X✝¹ : (TopologicalSpace.Opens ↑X)ᵒᵖ) : ((presheafEquivOfIso C H).unitIso.inv.app X✝).app X✝¹ = X✝.map (CategoryTheory.eqToHom ⋯)

def TopCat.Presheaf.toPushforwardOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y) {ℱ : Presheaf C X} {𝒢 : Presheaf C Y} (α : (pushforward C H.hom).obj ℱ ⟶ 𝒢) : ℱ ⟶ (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 Y : TopCat} (H₁ : X ≅ Y) {ℱ : Presheaf C X} {𝒢 : Presheaf C Y} (H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (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 Y : TopCat} (H₁ : X ≅ Y) {ℱ : Presheaf C Y} {𝒢 : Presheaf C X} (H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢) : (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 Y : TopCat} (H₁ : X ≅ Y) {ℱ : Presheaf C Y} {𝒢 : Presheaf C X} (H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (pushforwardToOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).obj (Opposite.unop U)))) (𝒢.map (CategoryTheory.eqToHom ⋯))

noncomputable def TopCat.Presheaf.pullback (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Functor (Presheaf C Y) (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

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

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

Equations

• TopCat.Presheaf.pullbackPushforwardAdjunction C f = (TopologicalSpace.Opens.map f).op.lanAdjunction C

@[deprecated TopCat.Presheaf.pullbackPushforwardAdjunction (since := "2026-03-03")]

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

Alias of TopCat.Presheaf.pullbackPushforwardAdjunction.

---

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

Equations

• TopCat.Presheaf.pushforwardPullbackAdjunction = TopCat.Presheaf.pullbackPushforwardAdjunction

noncomputable def TopCat.Presheaf.pullbackHomIsoPushforwardInv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (H : X ≅ Y) : pullback C H.hom ≅ 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.pullbackPushforwardAdjunction C H.hom).leftAdjointUniq (TopCat.Presheaf.presheafEquivOfIso C H.symm).toAdjunction

noncomputable def TopCat.Presheaf.pullbackInvIsoPushforwardHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (H : X ≅ Y) : pullback C H.inv ≅ 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.pullbackPushforwardAdjunction C H.inv).leftAdjointUniq (TopCat.Presheaf.presheafEquivOfIso C H).toAdjunction

noncomputable def TopCat.Presheaf.pullbackObjObjOfImageOpen {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (ℱ : Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (H : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U)) : ((pullback C f).obj ℱ).obj (Opposite.op U) ≅ ℱ.obj (Opposite.op { carrier := ⇑(CategoryTheory.ConcreteCategory.hom 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.

theorem TopCat.Presheaf.pullbackObjObjOfImageOpen_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (ℱ : Presheaf C Y) {U V : TopologicalSpace.Opens ↑X} (HU : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U)) (HV : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑V)) (le : U ≤ V) : CategoryTheory.CategoryStruct.comp (((pullback C f).obj ℱ).map (CategoryTheory.homOfLE le).op) (pullbackObjObjOfImageOpen f ℱ U HU).hom = CategoryTheory.CategoryStruct.comp (pullbackObjObjOfImageOpen f ℱ V HV).hom (ℱ.map (IsOpenMap.functorMap HU HV le).op)

If U ⊆ V and f '' U, f '' V are open, then the isomorphisms f⁻¹ℱ U ≅ ℱ (f '' U), f⁻¹ℱ V ≅ ℱ (f '' V) given by pullbackObjObjOfImageOpen are compatible with the restriction maps.

noncomputable def IsOpenMap.pullbackObjIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (ℱ : TopCat.Presheaf C Y) : (TopCat.Presheaf.pullback C f).obj ℱ ≅ hf.functor.op.comp ℱ

If f : X ⟶ Y is an open map and ℱ is a presheaf on Y, then the pullback of ℱ by f is isomorphic to the composition of ℱ and of the functor (Open X)ᵒᵖ ⥤ (Open Y)ᵒᵖ induced by f.

Equations

• hf.pullbackObjIso ℱ = CategoryTheory.NatIso.ofComponents (fun (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) => TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ (Opposite.unop U) ⋯) ⋯

@[simp]

theorem IsOpenMap.pullbackObjIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (ℱ : TopCat.Presheaf C Y) (X✝ : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (hf.pullbackObjIso ℱ).inv.app X✝ = (TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ (Opposite.unop X✝) ⋯).inv

@[simp]

theorem IsOpenMap.pullbackObjIso_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (ℱ : TopCat.Presheaf C Y) (X✝ : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (hf.pullbackObjIso ℱ).hom.app X✝ = (TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ (Opposite.unop X✝) ⋯).hom

theorem IsOpenMap.pullbackObjIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) {ℱ 𝒢 : TopCat.Presheaf C Y} (u : ℱ ⟶ 𝒢) : CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.pullback C f).map u) (hf.pullbackObjIso 𝒢).hom = CategoryTheory.CategoryStruct.comp (hf.pullbackObjIso ℱ).hom (hf.functor.op.whiskerLeft u)

If f : X ⟶ Y is an open map, this expresses the naturality of the isomorphism IsOpenMap.pullbackObjIso between the pullback by f of a presheaf and the composition of that presheaf and of the functor (Open X)ᵒᵖ ⥤ (Open Y)ᵒᵖ induced by f.

noncomputable def IsOpenMap.pullbackIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) : TopCat.Presheaf.pullback C f ≅ (CategoryTheory.Functor.whiskeringLeft (TopologicalSpace.Opens ↑X)ᵒᵖ (TopologicalSpace.Opens ↑Y)ᵒᵖ C).obj hf.functor.op

If f : X ⟶ Y, this is the isomorphism between the pullback functor by f and the "naive" pullback given by composing presheaves with the functor (Open X)ᵒᵖ ⥤ (Open Y)ᵒᵖ induced by f.

Equations

• hf.pullbackIso = CategoryTheory.NatIso.ofComponents hf.pullbackObjIso ⋯

@[simp]

theorem IsOpenMap.pullbackIso_inv_app_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (X✝ : TopCat.Presheaf C Y) (X✝¹ : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (hf.pullbackIso.inv.app X✝).app X✝¹ = (TopCat.Presheaf.pullbackObjObjOfImageOpen f X✝ (Opposite.unop X✝¹) ⋯).inv

@[simp]

theorem IsOpenMap.pullbackIso_hom_app_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (X✝ : TopCat.Presheaf C Y) (X✝¹ : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (hf.pullbackIso.hom.app X✝).app X✝¹ = (TopCat.Presheaf.pullbackObjObjOfImageOpen f X✝ (Opposite.unop X✝¹) ⋯).hom