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

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

Instances For
Equations
• AlgebraicGeometry.PresheafedSpace.coeCarrier = { coe := fun (X : ) => X }
Equations
• AlgebraicGeometry.PresheafedSpace.instCoeSortType = { coe := fun (X : ) => X }
theorem AlgebraicGeometry.PresheafedSpace.mk_coe {C : Type u_1} [] (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier) :
{ carrier := carrier, presheaf := presheaf } = carrier
Equations
• X.instTopologicalSpaceαCarrier = (↑X).str
def AlgebraicGeometry.PresheafedSpace.const {C : Type u_1} [] (X : TopCat) (Z : C) :

The constant presheaf on X with value Z.

Equations
• = { carrier := X, presheaf := Z }
Instances For
Equations
• AlgebraicGeometry.PresheafedSpace.instInhabited = { default := }
structure AlgebraicGeometry.PresheafedSpace.Hom {C : Type u_1} [] :
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.

Instances For
theorem AlgebraicGeometry.PresheafedSpace.Hom.ext {C : Type u_1} [] (α : X.Hom Y) (β : X.Hom Y) (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.whiskerRight X.presheaf) = β.c) :
α = β
theorem AlgebraicGeometry.PresheafedSpace.hext {C : Type u_1} [] (α : X.Hom Y) (β : X.Hom Y) (w : α.base = β.base) (h : HEq α.c β.c) :
α = β
def AlgebraicGeometry.PresheafedSpace.id {C : Type u_1} [] :
X.Hom X

The identity morphism of a PresheafedSpace.

Equations
Instances For
Equations
• X.homInhabited = { default := X.id }
def AlgebraicGeometry.PresheafedSpace.comp {C : Type u_1} [] (α : X.Hom Y) (β : Y.Hom Z) :
X.Hom Z

Composition of morphisms of PresheafedSpaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicGeometry.PresheafedSpace.comp_c {C : Type u_1} [] (α : X.Hom Y) (β : Y.Hom Z) :

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.

Equations
theorem AlgebraicGeometry.PresheafedSpace.ext {C : Type u_1} [] (α : X Y) (β : X Y) (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.whiskerRight X.presheaf) = β.c) :
α = β
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.id_c_app {C : Type u_1} [] (U : ᵒᵖ) :
.app U = X.presheaf.map
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.comp_base {C : Type u_1} [] (f : X Y) (g : Y Z) :
instance AlgebraicGeometry.PresheafedSpace.instCoeFunHomForallαTopologicalSpaceCarrier {C : Type u_1} [] :
CoeFun (X Y) fun (x : X Y) => XY
Equations
• X.instCoeFunHomForallαTopologicalSpaceCarrier Y = { coe := fun (f : X Y) => f.base }
theorem AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc {C : Type u_1} [] (α : X Y) (β : Y Z✝) (U : (TopologicalSpace.Opens Z✝)ᵒᵖ) {Z : C} (h : (.obj X.presheaf).obj U Z) :
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.comp_c_app {C : Type u_1} [] (α : X Y) (β : Y Z) (U : ᵒᵖ) :
.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj )))

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.congr_app {C : Type u_1} [] {α : X Y} {β : X Y} (h : α = β) (U : ᵒᵖ) :
α.c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (X.presheaf.map )
@[simp]
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.forget_map (C : Type u_1) [] :
∀ {X Y : } (f : X Y), = f.base

The forgetful functor from PresheafedSpace to TopCat.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv {C : Type u_1} [] (H : X Y) (α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf Y.presheaf) :
= { base := H.inv, c := }
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.isoOfComponents_hom {C : Type u_1} [] (H : X Y) (α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf Y.presheaf) :
= { base := H.hom, c := α.inv }
def AlgebraicGeometry.PresheafedSpace.isoOfComponents {C : Type u_1} [] (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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom {C : Type u_1} [] (H : X Y) :
= H.hom.c
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv {C : Type u_1} [] (H : X Y) :
= TopCat.Presheaf.pushforwardToOfIso (.mapIso H).symm H.inv.c
def AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso {C : Type u_1} [] (H : X Y) :
Y.presheaf (TopCat.Presheaf.pushforward C H.hom.base).obj X.presheaf

Isomorphic PresheafedSpaces have naturally isomorphic presheaves.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
Equations
• =

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

@[simp]
theorem AlgebraicGeometry.PresheafedSpace.restrict_presheaf {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :
(X.restrict h).presheaf = .functor.op.comp X.presheaf
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.restrict_carrier {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :
(X.restrict h) = U
def AlgebraicGeometry.PresheafedSpace.restrict {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :

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

Equations
• X.restrict h = { carrier := U, presheaf := .functor.op.comp X.presheaf }
Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_base {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :
(X.ofRestrict h).base = f
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) (V : ᵒᵖ) :
(X.ofRestrict h).c.app V = X.presheaf.map (.adjunction.counit.app ).op
def AlgebraicGeometry.PresheafedSpace.ofRestrict {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :
X.restrict h X

The map from the restriction of a presheafed space.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance AlgebraicGeometry.PresheafedSpace.ofRestrict_mono {C : Type u_1} [] {U : TopCat} (f : U X) (hf : ) :
CategoryTheory.Mono (X.ofRestrict hf)
Equations
• =
theorem AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf {C : Type u_1} [] :
(X.restrict ).presheaf = .obj X.presheaf
theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c {C : Type u_1} [] :
(X.ofRestrict ).c =
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.toRestrictTop_c {C : Type u_1} [] :
X.toRestrictTop.c =
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.toRestrictTop_base {C : Type u_1} [] :
X.toRestrictTop.base =
def AlgebraicGeometry.PresheafedSpace.toRestrictTop {C : Type u_1} [] :
X X.restrict

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

Equations
• X.toRestrictTop = { base := , c := }
Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv {C : Type u_1} [] :
X.restrictTopIso.inv = X.toRestrictTop
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom {C : Type u_1} [] :
X.restrictTopIso.hom = X.ofRestrict
def AlgebraicGeometry.PresheafedSpace.restrictTopIso {C : Type u_1} [] :
X.restrict X

The isomorphism from the restriction to the top subspace.

Equations
• X.restrictTopIso = { hom := X.ofRestrict , inv := X.toRestrictTop, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.Γ_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), AlgebraicGeometry.PresheafedSpace.Γ.map f = f.unop.c.app
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.Γ_obj {C : Type u_1} [] (X : ) :
AlgebraicGeometry.PresheafedSpace.Γ.obj X = .presheaf.obj

The global sections, notated Gamma.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicGeometry.PresheafedSpace.Γ_obj_op {C : Type u_1} [] :
AlgebraicGeometry.PresheafedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj
theorem AlgebraicGeometry.PresheafedSpace.Γ_map_op {C : Type u_1} [] (f : X Y) :
AlgebraicGeometry.PresheafedSpace.Γ.map f.op = f.c.app
def CategoryTheory.Functor.mapPresheaf {C : Type u_1} [] {D : Type u_2} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.mapPresheaf_obj_X {C : Type u_1} [] {D : Type u_2} [] (F : ) :
(F.mapPresheaf.obj X) = X
@[simp]
theorem CategoryTheory.Functor.mapPresheaf_obj_presheaf {C : Type u_1} [] {D : Type u_2} [] (F : ) :
(F.mapPresheaf.obj X).presheaf = CategoryTheory.Functor.comp X.presheaf F
@[simp]
theorem CategoryTheory.Functor.mapPresheaf_map_f {C : Type u_1} [] {D : Type u_2} [] (F : ) (f : X Y) :
(F.mapPresheaf.map f).base = f.base
@[simp]
theorem CategoryTheory.Functor.mapPresheaf_map_c {C : Type u_1} [] {D : Type u_2} [] (F : ) (f : X Y) :
(F.mapPresheaf.map f).c =
def CategoryTheory.NatTrans.onPresheaf {C : Type u_1} [] {D : Type u_2} [] {F : } {G : } (α : F G) :
G.mapPresheaf F.mapPresheaf

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

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