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_1) [CategoryTheory.Category.{u_2, u_1} C] extends AlgebraicGeometry.PresheafedSpace : Type (max (max u_1 u_2) (u_3 + 1))

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

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

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

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

Equations

• AlgebraicGeometry.SheafedSpace.coeCarrier = { coe := fun (X : AlgebraicGeometry.SheafedSpace C) => ↑X.toPresheafedSpace }

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

Equations

• AlgebraicGeometry.SheafedSpace.coeSort = { coe := fun (X : AlgebraicGeometry.SheafedSpace C) => ↑↑X.toPresheafedSpace }

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

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

Equations

• AlgebraicGeometry.SheafedSpace.sheaf X = { val := X.presheaf, cond := ⋯ }

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

instance AlgebraicGeometry.SheafedSpace.instTopologicalSpaceαCarrierToPresheafedSpace {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) : TopologicalSpace ↑↑X.toPresheafedSpace

Equations

• AlgebraicGeometry.SheafedSpace.instTopologicalSpaceαCarrierToPresheafedSpace X = (↑X.toPresheafedSpace).str

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

The trivial unit valued sheaf on any topological space.

Equations

• AlgebraicGeometry.SheafedSpace.unit X = let __src := AlgebraicGeometry.PresheafedSpace.const X { as := PUnit.unit }; { toPresheafedSpace := __src, IsSheaf := ⋯ }

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

Equations

• AlgebraicGeometry.SheafedSpace.instInhabitedSheafedSpaceDiscreteUnitDiscreteCategory = { default := AlgebraicGeometry.SheafedSpace.unit (TopCat.of PEmpty.{u_2 + 1} ) }

instance AlgebraicGeometry.SheafedSpace.instCategorySheafedSpace {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} (AlgebraicGeometry.SheafedSpace C)

Equations

• AlgebraicGeometry.SheafedSpace.instCategorySheafedSpace = let_fun this := inferInstance; this

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

@[simp]

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

@[simp]

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

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

Constructor for isomorphisms in the category SheafedSpace C.

Equations

• AlgebraicGeometry.SheafedSpace.isoMk e = { hom := e.hom, inv := e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : ∀ {X Y : CategoryTheory.InducedCategory (AlgebraicGeometry.PresheafedSpace C) AlgebraicGeometry.SheafedSpace.toPresheafedSpace} (f : X ⟶ Y), AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.map f = f

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

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

Equations

• AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace = CategoryTheory.inducedFunctor AlgebraicGeometry.SheafedSpace.toPresheafedSpace

instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Functor.Full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Functor.Faithful AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

The forgetful functor from SheafedSpace to Top.

Equations

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

def AlgebraicGeometry.SheafedSpace.restrict {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U ⟶ ↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) : AlgebraicGeometry.SheafedSpace C

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

Equations

• AlgebraicGeometry.SheafedSpace.restrict X h = let __src := AlgebraicGeometry.PresheafedSpace.restrict X.toPresheafedSpace h; { toPresheafedSpace := __src, IsSheaf := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• AlgebraicGeometry.SheafedSpace.restrictTopIso X = AlgebraicGeometry.SheafedSpace.isoMk (AlgebraicGeometry.PresheafedSpace.restrictTopIso X.toPresheafedSpace)

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

The global sections, notated Gamma.

Equations

• AlgebraicGeometry.SheafedSpace.Γ = CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op AlgebraicGeometry.PresheafedSpace.Γ

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

@[simp]

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

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

@[simp]

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

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

noncomputable instance AlgebraicGeometry.SheafedSpace.instCreatesColimitsSheafedSpaceInstCategorySheafedSpacePresheafedSpaceCategoryOfPresheafedSpacesForgetToPresheafedSpace {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.CreatesColimits AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace

Equations

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

instance AlgebraicGeometry.SheafedSpace.instHasColimitsSheafedSpaceInstCategorySheafedSpace {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasColimits (AlgebraicGeometry.SheafedSpace C)

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.SheafedSpace.instPreservesColimitsSheafedSpaceInstCategorySheafedSpaceTopCatInstTopCatLargeCategoryForget {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.PreservesColimits (AlgebraicGeometry.SheafedSpace.forget C)

Equations

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