Smooth manifolds as locally ringed spaces #
This file equips a smooth manifold with the structure of a locally ringed space.
Main results #
smoothSheafCommRing.isUnit_stalk_iff: The units of the stalk atxof the sheaf of smooth functions from a smooth manifoldMto its scalar field𝕜, considered as a sheaf of commutative rings, are the functions whose values atxare nonzero.
Main definitions #
ChartedSpace.locallyRingedSpace: A smooth manifold can be considered as a locally ringed space.ChartedSpace.locallyRingedSpaceMap: A smooth map between smooth manifolds induces a morphism of locally ringed spaces.
TODO #
- Show that every morphism of locally ringed spaces between two smooth manifolds is induced
by a smooth map via
ChartedSpace.locallyRingedSpaceMap.
theorem
smoothSheafCommRing.isUnit_stalk_iff
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{x : M}
(f : ↑((smoothSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜).presheaf.stalk x))
:
The units of the stalk at x of the sheaf of smooth functions from M to 𝕜, considered as a
sheaf of commutative rings, are the functions whose values at x are nonzero.
theorem
smoothSheafCommRing.nonunits_stalk
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(x : M)
:
nonunits ↑((smoothSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜).presheaf.stalk x) = ↑(RingHom.ker (eval IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x))
The non-units of the stalk at x of the sheaf of smooth functions from M to 𝕜, considered
as a sheaf of commutative rings, are the functions whose values at x are zero.
instance
smoothSheafCommRing.instLocalRing_stalk
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(x : M)
:
IsLocalRing ↑((smoothSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜).presheaf.stalk x)
The stalks of the structure sheaf of a smooth manifold are local rings.
noncomputable def
ChartedSpace.locallyRingedSpace
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
:
A smooth manifold can be considered as a locally ringed space.
Equations
- ChartedSpace.locallyRingedSpace IM M = { carrier := TopCat.of M, presheaf := smoothPresheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜, IsSheaf := ⋯, isLocalRing := ⋯ }
Instances For
@[deprecated ChartedSpace.locallyRingedSpace (since := "2026-04-01")]
def
IsManifold.locallyRingedSpace
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
:
Alias of ChartedSpace.locallyRingedSpace.
A smooth manifold can be considered as a locally ringed space.
Instances For
noncomputable def
ChartedSpace.locallyRingedSpaceMapAux
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{EN : Type u_3}
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HN : Type u_4}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
{N : Type u}
[TopologicalSpace N]
[ChartedSpace HN N]
(f : M → N)
(hf : ContMDiff IM IN (↑⊤) f)
:
(Implementation): Use ChartedSpace.locallyRingedSpaceMap.
Equations
- ChartedSpace.locallyRingedSpaceMapAux f hf = { base := TopCat.ofHom { toFun := f, continuous_toFun := ⋯ }, c := (ContMDiff.smoothSheafCommRingHom IN N f hf).hom }
Instances For
theorem
ChartedSpace.stalkMap_locallyRingedSpaceMapAux
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{EN : Type u_3}
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HN : Type u_4}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
{N : Type u}
[TopologicalSpace N]
[ChartedSpace HN N]
(f : M → N)
(hf : ContMDiff IM IN (↑⊤) f)
(x : M)
:
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x)
(smoothSheafCommRing.evalHom IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x) = smoothSheafCommRing.evalHom IN (modelWithCornersSelf 𝕜 𝕜) N 𝕜 (f x)
(Implementation): Use ChartedSpace.stalkMap_locallyRingedSpaceMap_evalHom.
noncomputable def
ChartedSpace.locallyRingedSpaceMap
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{EN : Type u_3}
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HN : Type u_4}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
{N : Type u}
[TopologicalSpace N]
[ChartedSpace HN N]
(f : M → N)
(hf : ContMDiff IM IN (↑⊤) f)
:
A smooth function of manifolds f : M → N induces a morphism of locally ringed spaces.
Equations
- ChartedSpace.locallyRingedSpaceMap f hf = { toHom := ChartedSpace.locallyRingedSpaceMapAux f hf, prop := ⋯ }
Instances For
@[simp]
theorem
ChartedSpace.locallyRingedSpaceMap_base
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{EN : Type u_3}
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HN : Type u_4}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
{N : Type u}
[TopologicalSpace N]
[ChartedSpace HN N]
(f : M → N)
(hf : ContMDiff IM IN (↑⊤) f)
:
@[simp]
theorem
ChartedSpace.stalkMap_locallyRingedSpaceMap_evalHom
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{EN : Type u_3}
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HN : Type u_4}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
{N : Type u}
[TopologicalSpace N]
[ChartedSpace HN N]
(f : M → N)
(hf : ContMDiff IM IN (↑⊤) f)
(x : M)
:
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (locallyRingedSpaceMap f hf) x)
(smoothSheafCommRing.evalHom IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x) = smoothSheafCommRing.evalHom IN (modelWithCornersSelf 𝕜 𝕜) N 𝕜 (f x)
@[simp]
theorem
ChartedSpace.stalkMap_locallyRingedSpaceMap_evalHom_assoc
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{EN : Type u_3}
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HN : Type u_4}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
{N : Type u}
[TopologicalSpace N]
[ChartedSpace HN N]
(f : M → N)
(hf : ContMDiff IM IN (↑⊤) f)
(x : M)
{Z : CommRingCat}
(h : CommRingCat.of 𝕜 ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (locallyRingedSpaceMap f hf) x)
(CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.evalHom IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x) h) = CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.evalHom IN (modelWithCornersSelf 𝕜 𝕜) N 𝕜 (f x)) h
theorem
ChartedSpace.locallyRingedSpace_id
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
:
theorem
ChartedSpace.locallyRingedSpace_comp
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{EN : Type u_3}
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HN : Type u_4}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
{N : Type u}
[TopologicalSpace N]
[ChartedSpace HN N]
{EP : Type u_5}
[NormedAddCommGroup EP]
[NormedSpace 𝕜 EP]
{HP : Type u_6}
[TopologicalSpace HP]
(IP : ModelWithCorners 𝕜 EP HP)
{P : Type u}
[TopologicalSpace P]
[ChartedSpace HP P]
{f : M → N}
(hf : ContMDiff IM IN (↑⊤) f)
{g : N → P}
(hg : ContMDiff IN IP (↑⊤) g)
:
locallyRingedSpaceMap (g ∘ f) ⋯ = CategoryTheory.CategoryStruct.comp (locallyRingedSpaceMap f hf) (locallyRingedSpaceMap g hg)
instance
instIsOpenImmersionLocallyRingedSpaceMapSubtypeMemOpensVal
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(U : TopologicalSpace.Opens M)
:
noncomputable def
ChartedSpace.restrictLocallyRingedSpaceIso
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(U : TopologicalSpace.Opens M)
:
Viewing a manifold as a locally ringed space commutes with restriction to open subsets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ChartedSpace.restrictLocallyRingedSpaceIso_inv
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(U : TopologicalSpace.Opens M)
:
@[simp]
theorem
ChartedSpace.restrictLocallyRingedSpaceIso_hom
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(U : TopologicalSpace.Opens M)
: