Documentation

Mathlib.AlgebraicGeometry.PresheafedSpace

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
theorem AlgebraicGeometry.PresheafedSpace.mk_coe {C : Type u_1} [] (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier) :
{ carrier := carrier, presheaf := presheaf } = carrier
def AlgebraicGeometry.PresheafedSpace.const {C : Type u_1} [] (X : TopCat) (Z : C) :

The constant presheaf on X with value Z.

Instances For
structure AlgebraicGeometry.PresheafedSpace.Hom {C : Type u_1} [] :
Type (max u_2 u_3)
• base : X Y
• c : Y.presheaf s.base _* X.presheaf

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} [] (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.whiskerRight (CategoryTheory.eqToHom (_ : ().op = ().op)) X.presheaf) = β.c) :
α = β
theorem AlgebraicGeometry.PresheafedSpace.hext {C : Type u_1} [] (w : α.base = β.base) (h : HEq α.c β.c) :
α = β

The identity morphism of a PresheafedSpace.

Instances For

Composition of morphisms of PresheafedSpaces.

Instances For

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.

theorem AlgebraicGeometry.PresheafedSpace.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.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) :
theorem AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc {C : Type u_1} [] (α : X Y) (β : Y Z) (U : ()ᵒᵖ) {Z : C} (h : (().base _* 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 (().obj U.unop)))

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 (CategoryTheory.eqToHom (_ : ().op.obj U = ().op.obj U)))
@[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.

Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.isoOfComponents_hom {C : Type u_1} [] (H : X Y) (α : H.hom _* X.presheaf Y.presheaf) :
= { base := H.hom, c := α.inv }
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv {C : Type u_1} [] (H : X Y) (α : H.hom _* X.presheaf Y.presheaf) :
= { base := H.inv, c := }
def AlgebraicGeometry.PresheafedSpace.isoOfComponents {C : Type u_1} [] (H : X Y) (α : H.hom _* X.presheaf Y.presheaf) :
X Y

An isomorphism of PresheafedSpaces is a homeomorphism of the underlying space, and a natural transformation between the sheaves.

Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv {C : Type u_1} [] (H : X Y) :
= TopCat.Presheaf.pushforwardToOfIso (().mapIso H).symm H.inv.c
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom {C : Type u_1} [] (H : X Y) :
= H.hom.c
def AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso {C : Type u_1} [] (H : X Y) :
Y.presheaf H.hom.base _* X.presheaf

Isomorphic PresheafedSpaces have naturally isomorphic presheaves.

Instances For

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

@[simp]
theorem AlgebraicGeometry.PresheafedSpace.restrict_carrier {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.restrict_presheaf {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :
().presheaf = CategoryTheory.Functor.comp (IsOpenMap.functor (_ : )).op X.presheaf
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.

Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) (V : ()ᵒᵖ) :
.app V = X.presheaf.map ((IsOpenMap.adjunction (_ : )).counit.app V.unop).op
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_base {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :
().base = f
def AlgebraicGeometry.PresheafedSpace.ofRestrict {C : Type u_1} [] {U : TopCat} {f : U X} (h : ) :

The map from the restriction of a presheafed space.

Instances For
instance AlgebraicGeometry.PresheafedSpace.ofRestrict_mono {C : Type u_1} [] {U : TopCat} (f : U X) (hf : ) :
theorem AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf {C : Type u_1} [] :
().presheaf = _* X.presheaf
theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c {C : Type u_1} [] :
= CategoryTheory.eqToHom (_ : X.presheaf = ().base _* ().presheaf)
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.toRestrictTop_c {C : Type u_1} [] :
= CategoryTheory.eqToHom (_ : ().presheaf = _* X.presheaf)

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

Instances For
@[simp]
@[simp]

The isomorphism from the restriction to the top subspace.

Instances For
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.Γ_obj {C : Type u_1} [] (X : ) :
AlgebraicGeometry.PresheafedSpace.Γ.obj X = X.unop.presheaf.obj ()
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.Γ_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), AlgebraicGeometry.PresheafedSpace.Γ.map f = f.unop.c.app ()

The global sections, notated Gamma.

Instances For
theorem AlgebraicGeometry.PresheafedSpace.Γ_obj_op {C : Type u_1} [] :
AlgebraicGeometry.PresheafedSpace.Γ.obj () = 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

Instances For
@[simp]
theorem CategoryTheory.Functor.mapPresheaf_obj_X {C : Type u_1} [] {D : Type u_2} [] (F : ) :
↑(().obj X) = X
@[simp]
theorem CategoryTheory.Functor.mapPresheaf_obj_presheaf {C : Type u_1} [] {D : Type u_2} [] (F : ) :
(().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) :
(().map f).base = f.base
@[simp]
theorem CategoryTheory.Functor.mapPresheaf_map_c {C : Type u_1} [] {D : Type u_2} [] (F : ) (f : X Y) :
(().map f).c =
def CategoryTheory.NatTrans.onPresheaf {C : Type u_1} [] {D : Type u_2} [] {F : } {G : } (α : F G) :

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

Instances For