Presheafed spaces

Introduces the category of topological spaces equipped with a presheaf (taking values in an arbitrary target category C.)

We further describe how to apply functors and natural transformations to the values of the presheaves.

structure AlgebraicGeometry.PresheafedSpace (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Type (max (max u_1 u_2) (u_3 + 1))

A PresheafedSpace C is a topological space equipped with a presheaf of Cs.

• carrier : TopCat
• presheaf : TopCat.Presheaf C ↑self

instance AlgebraicGeometry.PresheafedSpace.coeCarrier {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : CoeOut (PresheafedSpace C) TopCat

instance AlgebraicGeometry.PresheafedSpace.instCoeSortType {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] : CoeSort (PresheafedSpace C) (Type u_2)

instance AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : TopologicalSpace ↑↑X

def AlgebraicGeometry.PresheafedSpace.const {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : TopCat) (Z : C) : PresheafedSpace C

The constant presheaf on X with value Z.

instance AlgebraicGeometry.PresheafedSpace.instInhabited {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [Inhabited C] : Inhabited (PresheafedSpace C)

structure AlgebraicGeometry.PresheafedSpace.Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X Y : PresheafedSpace C) : Type (max u_2 u_3)

A morphism between presheafed spaces X and Y consists of a continuous map f between the underlying topological spaces, and a (notice contravariant!) map from the presheaf on Y to the pushforward of the presheaf on X via f.

• base : ↑X ⟶ ↑Y
• c : Y.presheaf ⟶ (TopCat.Presheaf.pushforward C self.base).obj X.presheaf

theorem AlgebraicGeometry.PresheafedSpace.Hom.ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (α β : X.Hom Y) (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.Functor.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf) = β.c) : α = β

theorem AlgebraicGeometry.PresheafedSpace.hext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (α β : X.Hom Y) (w : α.base = β.base) (h : α.c ≍ β.c) : α = β

def AlgebraicGeometry.PresheafedSpace.id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : X.Hom X

The identity morphism of a PresheafedSpace.

instance AlgebraicGeometry.PresheafedSpace.homInhabited {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : Inhabited (X.Hom X)

def AlgebraicGeometry.PresheafedSpace.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : PresheafedSpace C} (α : X.Hom Y) (β : Y.Hom Z) : X.Hom Z

Composition of morphisms of PresheafedSpaces.

theorem AlgebraicGeometry.PresheafedSpace.comp_c {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : PresheafedSpace C} (α : X.Hom Y) (β : Y.Hom Z) : (comp α β).c = CategoryTheory.CategoryStruct.comp β.c ((TopCat.Presheaf.pushforward C β.base).map α.c)

instance AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Category.{max u_2 u_3, max (max (u_3 + 1) u_2) u_1} (PresheafedSpace C)

The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map from the presheaf on the target to the pushforward of the presheaf on the source.

@[reducible, inline]

abbrev AlgebraicGeometry.PresheafedSpace.Hom.toPshHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (f : X.Hom Y) : X ⟶ Y

Cast Hom X Y as an arrow X ⟶ Y of presheaves.

theorem AlgebraicGeometry.PresheafedSpace.ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.Functor.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf) = β.c) : α = β

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.id_base {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id ↑X

theorem AlgebraicGeometry.PresheafedSpace.id_c {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : (CategoryTheory.CategoryStruct.id X).c = CategoryTheory.CategoryStruct.id X.presheaf

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.id_c_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) (U : (TopologicalSpace.Opens ↑↑X)ᵒᵖ) : (CategoryTheory.CategoryStruct.id X).c.app U = X.presheaf.map (CategoryTheory.CategoryStruct.id U)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.comp_base {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

instance AlgebraicGeometry.PresheafedSpace.instCoeFunHomForallCarrierCarrier {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X Y : PresheafedSpace C) : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ↑↑X → ↑↑Y

Note that we don't include a ConcreteCategory instance, since equality of morphisms X ⟶ Y does not follow from equality of their coercions X → Y.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.comp_c_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z)ᵒᵖ) : (CategoryTheory.CategoryStruct.comp α β).c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj (Opposite.unop U))))

Sometimes rewriting with comp_c_app doesn't work because of dependent type issues. In that case, erw comp_c_app_assoc might make progress. The lemma comp_c_app_assoc is also better suited for rewrites in the opposite direction.

theorem AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z)ᵒᵖ) {Z✝ : C} (h : ((TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.comp α β).base).obj X.presheaf).obj U ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp α β).c.app U) h = CategoryTheory.CategoryStruct.comp (β.c.app U) (CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj (Opposite.unop U)))) h)

theorem AlgebraicGeometry.PresheafedSpace.congr_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U : (TopologicalSpace.Opens ↑↑Y)ᵒᵖ) : α.c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (X.presheaf.map (CategoryTheory.eqToHom ⋯))

def AlgebraicGeometry.PresheafedSpace.forget (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Functor (PresheafedSpace C) TopCat

The forgetful functor from PresheafedSpace to TopCat.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.forget_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : PresheafedSpace C} (f : X✝ ⟶ Y✝) : (forget C).map f = f.base

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.forget_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : (forget C).obj X = ↑X

def AlgebraicGeometry.PresheafedSpace.isoOfComponents {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (H : ↑X ≅ ↑Y) (α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf) : X ≅ Y

An isomorphism of PresheafedSpaces is a homeomorphism of the underlying space, and a natural transformation between the sheaves.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (H : ↑X ≅ ↑Y) (α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf) : (isoOfComponents H α).inv = { base := H.inv, c := TopCat.Presheaf.toPushforwardOfIso H α.hom }

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.isoOfComponents_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (H : ↑X ≅ ↑Y) (α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf) : (isoOfComponents H α).hom = { base := H.hom, c := α.inv }

def AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (H : X ≅ Y) : Y.presheaf ≅ (TopCat.Presheaf.pushforward C H.hom.base).obj X.presheaf

Isomorphic PresheafedSpaces have naturally isomorphic presheaves.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (H : X ≅ Y) : (sheafIsoOfIso H).hom = H.hom.c

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (H : X ≅ Y) : (sheafIsoOfIso H).inv = TopCat.Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c

instance AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.base

instance AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.c

theorem AlgebraicGeometry.PresheafedSpace.isIso_of_components {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f.base] [CategoryTheory.IsIso f.c] : CategoryTheory.IsIso f

This could be used in conjunction with CategoryTheory.NatIso.isIso_of_isIso_app.

def AlgebraicGeometry.PresheafedSpace.restrict {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : PresheafedSpace C

The restriction of a presheafed space along an open embedding into the space.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrict_presheaf {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.restrict h).presheaf = ⋯.functor.op.comp X.presheaf

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrict_carrier {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ↑(X.restrict h) = U

def AlgebraicGeometry.PresheafedSpace.ofRestrict {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : X.restrict h ⟶ X

The map from the restriction of a presheafed space.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_base {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.ofRestrict h).base = f

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ) : (X.ofRestrict h).c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op

instance AlgebraicGeometry.PresheafedSpace.ofRestrict_mono {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {U : TopCat} (X : PresheafedSpace C) (f : U ⟶ ↑X) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Mono (X.ofRestrict hf)

theorem AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : (X.restrict ⋯).presheaf = (TopCat.Presheaf.pushforward C (TopologicalSpace.Opens.inclusionTopIso ↑X).inv).obj X.presheaf

theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : (X.ofRestrict ⋯).c = CategoryTheory.eqToHom ⋯

def AlgebraicGeometry.PresheafedSpace.toRestrictTop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : X ⟶ X.restrict ⋯

The map to the restriction of a presheafed space along the canonical inclusion from the top subspace.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.toRestrictTop_base {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : X.toRestrictTop.base = (TopologicalSpace.Opens.inclusionTopIso ↑X).inv

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.toRestrictTop_c {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : X.toRestrictTop.c = CategoryTheory.eqToHom ⋯

def AlgebraicGeometry.PresheafedSpace.restrictTopIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : X.restrict ⋯ ≅ X

The isomorphism from the restriction to the top subspace.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : X.restrictTopIso.hom = X.ofRestrict ⋯

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : X.restrictTopIso.inv = X.toRestrictTop

def AlgebraicGeometry.PresheafedSpace.Γ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Functor (PresheafedSpace C)ᵒᵖ C

The global sections, notated Gamma.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.Γ_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : (PresheafedSpace C)ᵒᵖ} (f : X✝ ⟶ Y✝) : Γ.map f = f.unop.c.app (Opposite.op ⊤)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.Γ_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : (PresheafedSpace C)ᵒᵖ) : Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)

theorem AlgebraicGeometry.PresheafedSpace.Γ_obj_op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : PresheafedSpace C) : Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)

theorem AlgebraicGeometry.PresheafedSpace.Γ_map_op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) : Γ.map f.op = f.c.app (Opposite.op ⊤)

def CategoryTheory.Functor.mapPresheaf {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (F : Functor C D) : Functor (AlgebraicGeometry.PresheafedSpace C) (AlgebraicGeometry.PresheafedSpace D)

We can apply a functor F : C ⥤ D to the values of the presheaf in any PresheafedSpace C, giving a functor PresheafedSpace C ⥤ PresheafedSpace D

@[simp]

theorem CategoryTheory.Functor.mapPresheaf_obj_X {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (F : Functor C D) (X : AlgebraicGeometry.PresheafedSpace C) : ↑(F.mapPresheaf.obj X) = ↑X

@[simp]

theorem CategoryTheory.Functor.mapPresheaf_obj_presheaf {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (F : Functor C D) (X : AlgebraicGeometry.PresheafedSpace C) : (F.mapPresheaf.obj X).presheaf = comp X.presheaf F

@[simp]

theorem CategoryTheory.Functor.mapPresheaf_map_f {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (F : Functor C D) {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) : (F.mapPresheaf.map f).base = f.base

@[simp]

theorem CategoryTheory.Functor.mapPresheaf_map_c {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (F : Functor C D) {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) : (F.mapPresheaf.map f).c = whiskerRight f.c F

def CategoryTheory.NatTrans.onPresheaf {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] {F G : Functor C D} (α : F ⟶ G) : G.mapPresheaf ⟶ F.mapPresheaf

A natural transformation induces a natural transformation between the map_presheaf functors.