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.
A PresheafedSpace C
is a topological space equipped with a presheaf of C
s.
- carrier : TopCat
- presheaf : TopCat.Presheaf C ↑self
Instances For
Equations
- AlgebraicGeometry.PresheafedSpace.coeCarrier = { coe := fun (X : AlgebraicGeometry.PresheafedSpace C) => ↑X }
Equations
- AlgebraicGeometry.PresheafedSpace.instCoeSortType = { coe := fun (X : AlgebraicGeometry.PresheafedSpace C) => ↑↑X }
Equations
- X.instTopologicalSpaceαCarrier = (↑X).str
The constant presheaf on X
with value Z
.
Equations
- AlgebraicGeometry.PresheafedSpace.const X Z = { carrier := X, presheaf := (CategoryTheory.Functor.const (TopologicalSpace.Opens ↑X)ᵒᵖ).obj Z }
Instances For
Equations
- AlgebraicGeometry.PresheafedSpace.instInhabited = { default := AlgebraicGeometry.PresheafedSpace.const (TopCat.of PEmpty.{?u.22 + 1} ) default }
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
.
- base : ↑X ⟶ ↑Y
- c : Y.presheaf ⟶ (TopCat.Presheaf.pushforward C self.base).obj X.presheaf
Instances For
The identity morphism of a PresheafedSpace
.
Equations
- X.id = { base := CategoryTheory.CategoryStruct.id ↑X, c := CategoryTheory.CategoryStruct.id X.presheaf }
Instances For
Equations
- X.homInhabited = { default := X.id }
Composition of morphisms of PresheafedSpace
s.
Equations
- One or more equations did not get rendered due to their size.
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.
Cast Hom X Y
as an arrow X ⟶ Y
of presheaves.
Equations
- f.toPshHom = f
Instances For
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.
The forgetful functor from PresheafedSpace
to TopCat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An isomorphism of PresheafedSpace
s 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
Isomorphic PresheafedSpace
s have naturally isomorphic presheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This could be used in conjunction with CategoryTheory.NatIso.isIso_of_isIso_app
.
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
The map from the restriction of a presheafed space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map to the restriction of a presheafed space along the canonical inclusion from the top subspace.
Equations
- X.toRestrictTop = { base := (TopologicalSpace.Opens.inclusionTopIso ↑X).inv, c := CategoryTheory.eqToHom ⋯ }
Instances For
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
The global sections, notated Gamma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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.