# 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) extends :
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 presheafed space which happens to be sheaf.

Instances For
theorem AlgebraicGeometry.SheafedSpace.IsSheaf {C : Type u} (self : ) :
self.presheaf.IsSheaf

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

Equations
• AlgebraicGeometry.SheafedSpace.coeCarrier = { coe := fun (X : ) => X.toPresheafedSpace }
Equations
• AlgebraicGeometry.SheafedSpace.coeSort = { coe := fun (X : ) => X.toPresheafedSpace }
def AlgebraicGeometry.SheafedSpace.sheaf {C : Type u} :
TopCat.Sheaf C X.toPresheafedSpace

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

Equations
• X.sheaf = { val := X.presheaf, cond := }
Instances For
theorem AlgebraicGeometry.SheafedSpace.mk_coe {C : Type u} (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier) (h : { carrier := carrier, presheaf := presheaf }.presheaf.IsSheaf) :
{ carrier := carrier, presheaf := presheaf, IsSheaf := h }.toPresheafedSpace = carrier
Equations
• X.instTopologicalSpaceαCarrier = (X.toPresheafedSpace).str

The trivial unit valued sheaf on any topological space.

Equations
• = let __src := ; { toPresheafedSpace := __src, IsSheaf := }
Instances For
Equations
• AlgebraicGeometry.SheafedSpace.instCategory = let_fun this := inferInstance; this
theorem AlgebraicGeometry.SheafedSpace.ext {C : Type u} {α : X Y} {β : X Y} (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.whiskerRight X.presheaf) = β.c) :
α = β
@[simp]
theorem AlgebraicGeometry.SheafedSpace.isoMk_inv {C : Type u} (e : X.toPresheafedSpace Y.toPresheafedSpace) :
= e.inv
@[simp]
theorem AlgebraicGeometry.SheafedSpace.isoMk_hom {C : Type u} (e : X.toPresheafedSpace Y.toPresheafedSpace) :
= e.hom
def AlgebraicGeometry.SheafedSpace.isoMk {C : Type u} (e : X.toPresheafedSpace Y.toPresheafedSpace) :
X Y

Constructor for isomorphisms in the category SheafedSpace C.

Equations
• = { hom := e.hom, inv := e.inv, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map {C : Type u} :
∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace} (f : X Y), AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.map f = f
@[simp]
theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_obj {C : Type u} (self : ) :
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.obj self = self.toPresheafedSpace

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

Equations
Instances For
instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full {C : Type u} :
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.Full
Equations
• =
instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful {C : Type u} :
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.Faithful
Equations
• =
Equations
• =
@[simp]
@[simp]
theorem AlgebraicGeometry.SheafedSpace.id_c_app {C : Type u} (U : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
.app U = CategoryTheory.CategoryStruct.id (X.presheaf.obj U)
@[simp]
theorem AlgebraicGeometry.SheafedSpace.comp_base {C : Type u} (f : X Y) (g : Y Z) :
@[simp]
theorem AlgebraicGeometry.SheafedSpace.comp_c_app {C : Type u} (α : X Y) (β : Y Z) (U : (TopologicalSpace.Opens Z.toPresheafedSpace)ᵒᵖ) :
.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (α.c.app (Opposite.op (().obj ())))
theorem AlgebraicGeometry.SheafedSpace.comp_c_app' {C : Type u} (α : X Y) (β : Y Z) (U : TopologicalSpace.Opens Z.toPresheafedSpace) :
.app () = CategoryTheory.CategoryStruct.comp (β.c.app ()) (α.c.app (Opposite.op (().obj U)))
theorem AlgebraicGeometry.SheafedSpace.congr_app {C : Type u} {α : X Y} {β : X Y} (h : α = β) (U : (TopologicalSpace.Opens Y.toPresheafedSpace)ᵒᵖ) :
α.c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (X.presheaf.map )

The forgetful functor from SheafedSpace to Top.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AlgebraicGeometry.SheafedSpace.restrict {C : Type u} {U : TopCat} {f : U X.toPresheafedSpace} (h : ) :

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

Equations
• X.restrict h = let __src := X.restrict h; { toPresheafedSpace := __src, IsSheaf := }
Instances For
@[simp]
theorem AlgebraicGeometry.SheafedSpace.ofRestrict_base {C : Type u} {U : TopCat} {f : U X.toPresheafedSpace} (h : ) :
(X.ofRestrict h).base = f
@[simp]
theorem AlgebraicGeometry.SheafedSpace.ofRestrict_c_app {C : Type u} {U : TopCat} {f : U X.toPresheafedSpace} (h : ) (V : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
(X.ofRestrict h).c.app V = X.presheaf.map (.adjunction.counit.app ()).op
def AlgebraicGeometry.SheafedSpace.ofRestrict {C : Type u} {U : TopCat} {f : U X.toPresheafedSpace} (h : ) :
X.restrict h X

The map from the restriction of a presheafed space.

Equations
• X.ofRestrict h = X.ofRestrict h
Instances For
@[simp]
theorem AlgebraicGeometry.SheafedSpace.restrictTopIso_inv {C : Type u} :
X.restrictTopIso.inv = X.toRestrictTop
@[simp]
theorem AlgebraicGeometry.SheafedSpace.restrictTopIso_hom {C : Type u} :
X.restrictTopIso.hom = X.ofRestrict

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

Equations
Instances For

The global sections, notated Gamma.

Equations
• AlgebraicGeometry.SheafedSpace.Γ = AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op.comp AlgebraicGeometry.PresheafedSpace.Γ
Instances For
theorem AlgebraicGeometry.SheafedSpace.Γ_def {C : Type u} :
AlgebraicGeometry.SheafedSpace.Γ = AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op.comp AlgebraicGeometry.PresheafedSpace.Γ
@[simp]
theorem AlgebraicGeometry.SheafedSpace.Γ_obj {C : Type u} (X : ) :
AlgebraicGeometry.SheafedSpace.Γ.obj X = ().presheaf.obj ()
theorem AlgebraicGeometry.SheafedSpace.Γ_obj_op {C : Type u} :
AlgebraicGeometry.SheafedSpace.Γ.obj () = X.presheaf.obj ()
@[simp]
theorem AlgebraicGeometry.SheafedSpace.Γ_map {C : Type u} {X : } {Y : } (f : X Y) :
AlgebraicGeometry.SheafedSpace.Γ.map f = f.unop.c.app ()
theorem AlgebraicGeometry.SheafedSpace.Γ_map_op {C : Type u} (f : X Y) :
AlgebraicGeometry.SheafedSpace.Γ.map f.op = f.c.app ()
noncomputable instance AlgebraicGeometry.SheafedSpace.instCreatesColimitsPresheafedSpaceForgetToPresheafedSpaceOfHasLimits {C : Type u} :
CategoryTheory.CreatesColimits AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
Equations
• One or more equations did not get rendered due to their size.
Equations
• =
Equations
• One or more equations did not get rendered due to their size.
theorem AlgebraicGeometry.SheafedSpace.hom_stalk_ext {C : Type u} [.ReflectsIsomorphisms] (f : X Y) (g : X Y) (h : f.base = g.base) (h' : ∀ (x : X.toPresheafedSpace), = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ).hom ) :
f = g
theorem AlgebraicGeometry.SheafedSpace.mono_of_base_injective_of_stalk_epi {C : Type u} [.ReflectsIsomorphisms] (f : X Y) (h₁ : Function.Injective f.base) (h₂ : ∀ (x : X.toPresheafedSpace), ) :