# Documentation

Mathlib.AlgebraicGeometry.SheafedSpace

# 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) [] extends :
Type (max (max u_1 u_2) (u_3 + 1))

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

Instances For
def AlgebraicGeometry.SheafedSpace.sheaf {C : Type u_1} [] :
TopCat.Sheaf C X.toPresheafedSpace

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

Instances For
theorem AlgebraicGeometry.SheafedSpace.mk_coe {C : Type u_1} [] (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

The trivial unit valued sheaf on any topological space.

Instances For
theorem AlgebraicGeometry.SheafedSpace.ext {C : Type u_1} [] (α : X Y) (β : X Y) (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.whiskerRight (CategoryTheory.eqToHom (_ : ().op = ().op)) X.presheaf) = β.c) :
α = β
@[simp]
theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map {C : Type u_1} [] :
∀ {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_1} [] (self : ) :
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.obj self = self.toPresheafedSpace

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

Instances For
instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full {C : Type u_1} [] :
CategoryTheory.Full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful {C : Type u_1} [] :
CategoryTheory.Faithful AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
@[simp]
theorem AlgebraicGeometry.SheafedSpace.id_base {C : Type u_1} [] :
().base = CategoryTheory.CategoryStruct.id X.toPresheafedSpace
theorem AlgebraicGeometry.SheafedSpace.id_c {C : Type u_1} [] :
= CategoryTheory.eqToHom (_ : X.presheaf = CategoryTheory.CategoryStruct.id X.toPresheafedSpace _* X.presheaf)
@[simp]
theorem AlgebraicGeometry.SheafedSpace.id_c_app {C : Type u_1} [] (U : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
.app U = CategoryTheory.eqToHom (_ : X.presheaf.obj U = X.presheaf.obj ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X.toPresheafedSpace)).op.obj U))
@[simp]
theorem AlgebraicGeometry.SheafedSpace.comp_base {C : Type u_1} [] (f : X Y) (g : Y Z) :
@[simp]
theorem AlgebraicGeometry.SheafedSpace.comp_c_app {C : Type u_1} [] (α : X Y) (β : Y Z) (U : (TopologicalSpace.Opens Z.toPresheafedSpace)ᵒᵖ) :
.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (α.c.app (Opposite.op (().obj U.unop)))
theorem AlgebraicGeometry.SheafedSpace.comp_c_app' {C : Type u_1} [] (α : 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_1} [] {α : X Y} {β : X Y} (h : α = β) (U : (TopologicalSpace.Opens Y.toPresheafedSpace)ᵒᵖ) :
α.c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (X.presheaf.map (CategoryTheory.eqToHom (_ : ().op.obj U = ().op.obj U)))

The forgetful functor from SheafedSpace to Top.

Instances For
def AlgebraicGeometry.SheafedSpace.restrict {C : Type u_1} [] {U : TopCat} {f : U X.toPresheafedSpace} (h : ) :

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

Instances For

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

Instances For

The global sections, notated Gamma.

Instances For
theorem AlgebraicGeometry.SheafedSpace.Γ_def {C : Type u_1} [] :
AlgebraicGeometry.SheafedSpace.Γ = CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op AlgebraicGeometry.PresheafedSpace.Γ
@[simp]
theorem AlgebraicGeometry.SheafedSpace.Γ_obj {C : Type u_1} [] (X : ) :
AlgebraicGeometry.SheafedSpace.Γ.obj X = X.unop.presheaf.obj ()
theorem AlgebraicGeometry.SheafedSpace.Γ_obj_op {C : Type u_1} [] :
AlgebraicGeometry.SheafedSpace.Γ.obj () = X.presheaf.obj ()
@[simp]
theorem AlgebraicGeometry.SheafedSpace.Γ_map {C : Type u_1} [] {X : } {Y : } (f : X Y) :
AlgebraicGeometry.SheafedSpace.Γ.map f = f.unop.c.app ()
theorem AlgebraicGeometry.SheafedSpace.Γ_map_op {C : Type u_1} [] (f : X Y) :
AlgebraicGeometry.SheafedSpace.Γ.map f.op = f.c.app ()