Sheafed spaces

Introduces the category of topological spaces equipped with a sheaf (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.SheafedSpace (C : Type u) [CategoryTheory.Category.{v, u} C] extends AlgebraicGeometry.PresheafedSpace C : Type (max (max u (u_1 + 1)) v)

A SheafedSpace C is a topological space equipped with a sheaf of Cs.

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

  A sheafed space is a presheafed space which happens to be a sheaf.

@[implicit_reducible]

instance AlgebraicGeometry.SheafedSpace.coeCarrier {C : Type u} [CategoryTheory.Category.{v, u} C] : CoeOut (SheafedSpace C) TopCat

@[implicit_reducible]

instance AlgebraicGeometry.SheafedSpace.coeSort {C : Type u} [CategoryTheory.Category.{v, u} C] : CoeSort (SheafedSpace C) (Type u_1)

def AlgebraicGeometry.SheafedSpace.sheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : TopCat.Sheaf C ↑X.toPresheafedSpace

Extract the sheaf C (X : Top) from a SheafedSpace C.

theorem AlgebraicGeometry.SheafedSpace.mk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier) (h : presheaf.IsSheaf) : ↑{ carrier := carrier, presheaf := presheaf, IsSheaf := h }.toPresheafedSpace = carrier

Not @[simp] since it already reduces to carrier = carrier.

@[implicit_reducible]

instance AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : TopologicalSpace ↑↑X.toPresheafedSpace

def AlgebraicGeometry.SheafedSpace.unit (X : TopCat) : SheafedSpace (CategoryTheory.Discrete Unit)

The trivial unit-valued sheaf on any topological space.

@[implicit_reducible]

instance AlgebraicGeometry.SheafedSpace.instInhabitedDiscreteUnit : Inhabited (SheafedSpace (CategoryTheory.Discrete Unit))

@[implicit_reducible]

instance AlgebraicGeometry.SheafedSpace.instCategory {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{max v u_1, max (max (u_1 + 1) v) u} (SheafedSpace C)

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

def AlgebraicGeometry.SheafedSpace.isoMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (e : X.toPresheafedSpace ≅ Y.toPresheafedSpace) : X ≅ Y

Constructor for isomorphisms in the category SheafedSpace C.

@[simp]

theorem AlgebraicGeometry.SheafedSpace.isoMk_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (e : X.toPresheafedSpace ≅ Y.toPresheafedSpace) : (isoMk e).inv = CategoryTheory.InducedCategory.homMk e.inv

@[simp]

theorem AlgebraicGeometry.SheafedSpace.isoMk_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (e : X.toPresheafedSpace ≅ Y.toPresheafedSpace) : (isoMk e).hom = CategoryTheory.InducedCategory.homMk e.hom

def AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (SheafedSpace C) (PresheafedSpace C)

Forgetting the sheaf condition is a functor from SheafedSpace C to PresheafedSpace C.

@[simp]

theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (self : SheafedSpace C) : forgetToPresheafedSpace.obj self = self.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.InducedCategory (PresheafedSpace C) toPresheafedSpace} (f : X✝ ⟶ Y✝) : forgetToPresheafedSpace.map f = f.hom

def AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace {C : Type u} [CategoryTheory.Category.{v, u} C] : forgetToPresheafedSpace.FullyFaithful

The functor forgetToPresheafedSpace : SheafedSpace C ⥤ PresheafedSpace C is fully faithful.

@[simp]

theorem AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace_preimage_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : forgetToPresheafedSpace.obj X ⟶ forgetToPresheafedSpace.obj Y) : (fullyFaithfulForgetToPresheafedSpace.preimage f).hom = f

instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full {C : Type u} [CategoryTheory.Category.{v, u} C] : forgetToPresheafedSpace.Full

instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] : forgetToPresheafedSpace.Faithful

instance AlgebraicGeometry.SheafedSpace.is_presheafedSpace_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom

@[simp]

theorem AlgebraicGeometry.SheafedSpace.id_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.SheafedSpace.id_hom_base {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : (CategoryTheory.CategoryStruct.id X).hom.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

theorem AlgebraicGeometry.SheafedSpace.id_hom_c {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : (CategoryTheory.CategoryStruct.id X).hom.c = CategoryTheory.eqToHom ⋯

theorem AlgebraicGeometry.SheafedSpace.id_hom_c_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) (U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) : (CategoryTheory.CategoryStruct.id X).hom.c.app U = CategoryTheory.CategoryStruct.id (X.presheaf.obj U)

@[simp]

theorem AlgebraicGeometry.SheafedSpace.comp_hom_base {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom.base = CategoryTheory.CategoryStruct.comp f.hom.base g.hom.base

@[simp]

theorem AlgebraicGeometry.SheafedSpace.comp_hom_c_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z.toPresheafedSpace)ᵒᵖ) : (CategoryTheory.CategoryStruct.comp α β).hom.c.app U = CategoryTheory.CategoryStruct.comp (β.hom.c.app U) (α.hom.c.app (Opposite.op ((TopologicalSpace.Opens.map β.hom.base).obj (Opposite.unop U))))

theorem AlgebraicGeometry.SheafedSpace.comp_hom_c_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) : (CategoryTheory.CategoryStruct.comp α β).hom.c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp (β.hom.c.app (Opposite.op U)) (α.hom.c.app (Opposite.op ((TopologicalSpace.Opens.map β.hom.base).obj U)))

theorem AlgebraicGeometry.SheafedSpace.congr_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U : (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)ᵒᵖ) : α.hom.c.app U = CategoryTheory.CategoryStruct.comp (β.hom.c.app U) (X.presheaf.map (CategoryTheory.eqToHom ⋯))

@[deprecated AlgebraicGeometry.SheafedSpace.id_hom_base (since := "2025-12-18")]

theorem AlgebraicGeometry.SheafedSpace.id_base {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : (CategoryTheory.CategoryStruct.id X).hom.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

Alias of AlgebraicGeometry.SheafedSpace.id_hom_base.

@[deprecated AlgebraicGeometry.SheafedSpace.id_hom_c (since := "2025-12-18")]

theorem AlgebraicGeometry.SheafedSpace.id_c {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : (CategoryTheory.CategoryStruct.id X).hom.c = CategoryTheory.eqToHom ⋯

Alias of AlgebraicGeometry.SheafedSpace.id_hom_c.

@[deprecated AlgebraicGeometry.SheafedSpace.id_hom_c_app (since := "2025-12-18")]

theorem AlgebraicGeometry.SheafedSpace.id_c_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) (U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) : (CategoryTheory.CategoryStruct.id X).hom.c.app U = CategoryTheory.CategoryStruct.id (X.presheaf.obj U)

Alias of AlgebraicGeometry.SheafedSpace.id_hom_c_app.

@[deprecated AlgebraicGeometry.SheafedSpace.comp_hom_base (since := "2025-12-18")]

theorem AlgebraicGeometry.SheafedSpace.comp_base {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom.base = CategoryTheory.CategoryStruct.comp f.hom.base g.hom.base

Alias of AlgebraicGeometry.SheafedSpace.comp_hom_base.

@[deprecated AlgebraicGeometry.SheafedSpace.comp_hom_c_app (since := "2025-12-18")]

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

Alias of AlgebraicGeometry.SheafedSpace.comp_hom_c_app.

@[deprecated AlgebraicGeometry.SheafedSpace.comp_hom_c_app' (since := "2025-12-18")]

theorem AlgebraicGeometry.SheafedSpace.comp_c_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) : (CategoryTheory.CategoryStruct.comp α β).hom.c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp (β.hom.c.app (Opposite.op U)) (α.hom.c.app (Opposite.op ((TopologicalSpace.Opens.map β.hom.base).obj U)))

Alias of AlgebraicGeometry.SheafedSpace.comp_hom_c_app'.

@[deprecated AlgebraicGeometry.SheafedSpace.congr_hom_app (since := "2025-12-18")]

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

Alias of AlgebraicGeometry.SheafedSpace.congr_hom_app.

def AlgebraicGeometry.SheafedSpace.forget (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (SheafedSpace C) TopCat

The forgetful functor from SheafedSpace to Top.

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

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

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

The map from the restriction of a presheafed space.

@[simp]

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

@[simp]

theorem AlgebraicGeometry.SheafedSpace.ofRestrict_hom_base {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : SheafedSpace C) {f : U ⟶ ↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.ofRestrict h).hom.base = f

def AlgebraicGeometry.SheafedSpace.restrictTopIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : X.restrict ⋯ ≅ X

The restriction of a sheafed space X to the top subspace is isomorphic to X itself.

@[simp]

theorem AlgebraicGeometry.SheafedSpace.restrictTopIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : X.restrictTopIso.hom = CategoryTheory.InducedCategory.homMk (X.ofRestrict ⋯)

@[simp]

theorem AlgebraicGeometry.SheafedSpace.restrictTopIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (X : SheafedSpace C) : X.restrictTopIso.inv = CategoryTheory.InducedCategory.homMk X.toRestrictTop

def AlgebraicGeometry.SheafedSpace.Γ {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (SheafedSpace C)ᵒᵖ C

The global sections, notated Gamma.

theorem AlgebraicGeometry.SheafedSpace.Γ_def {C : Type u} [CategoryTheory.Category.{v, u} C] : Γ = forgetToPresheafedSpace.op.comp PresheafedSpace.Γ

@[simp]

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

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

@[simp]

theorem AlgebraicGeometry.SheafedSpace.Γ_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : (SheafedSpace C)ᵒᵖ} (f : X ⟶ Y) : Γ.map f = f.unop.hom.c.app (Opposite.op ⊤)

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

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.SheafedSpace.instCreatesColimitsOfShapePresheafedSpaceForgetToPresheafedSpaceOfSmallOfHasLimitsOfShapeOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.Category.{w', w} J] [Small.{v, w} J] [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] : CategoryTheory.CreatesColimitsOfShape J forgetToPresheafedSpace

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.SheafedSpace.instCreatesColimitsPresheafedSpaceForgetToPresheafedSpaceOfHasLimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.CreatesColimits forgetToPresheafedSpace

instance AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.Category.{w', w} J] [Small.{v, w} J] [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] : CategoryTheory.Limits.HasColimitsOfShape J (SheafedSpace C)

instance AlgebraicGeometry.SheafedSpace.instHasColimitsOfHasLimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasColimits (SheafedSpace C)

instance AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.Category.{w', w} J] [Small.{v, w} J] [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] : CategoryTheory.Limits.PreservesColimitsOfShape J (forget C)

instance AlgebraicGeometry.SheafedSpace.instPreservesColimitsTopCatForgetOfHasLimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.PreservesColimits (forget C)

theorem AlgebraicGeometry.SheafedSpace.hom_stalk_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {X Y : SheafedSpace C} (f g : X ⟶ Y) (h : f.hom.base = g.hom.base) (h' : ∀ (x : ↑↑X.toPresheafedSpace), PresheafedSpace.Hom.stalkMap f.hom x = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (PresheafedSpace.Hom.stalkMap g.hom x)) : f = g

theorem AlgebraicGeometry.SheafedSpace.mono_of_base_injective_of_stalk_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {X Y : SheafedSpace C} (f : X ⟶ Y) (h₁ : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)) (h₂ : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.Epi (PresheafedSpace.Hom.stalkMap f.hom x)) : CategoryTheory.Mono f

theorem AlgebraicGeometry.SheafedSpace.epi_of_base_surjective_of_stalk_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {X Y : SheafedSpace C} (f : X ⟶ Y) (h₁ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)) (h₂ : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.Mono (PresheafedSpace.Hom.stalkMap f.hom x)) : CategoryTheory.Epi f