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 at x of the sheaf of smooth functions from a smooth manifold M to its scalar field 𝕜, considered as a sheaf of commutative rings, are the functions whose values at x are nonzero.

Main definitions

• IsManifold.locallyRingedSpace: A smooth manifold can be considered as a locally ringed space.

TODO

Characterize morphisms-of-locally-ringed-spaces (AlgebraicGeometry.LocallyRingedSpace.Hom) between smooth manifolds.

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)) : IsUnit f ↔ f ∉ RingHom.ker (eval IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 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.

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] : AlgebraicGeometry.LocallyRingedSpace

A smooth manifold can be considered as a locally ringed space.

Equations

• IsManifold.locallyRingedSpace IM M = { carrier := { carrier := M, str := inst✝¹ }, presheaf := smoothPresheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜, IsSheaf := ⋯, isLocalRing := ⋯ }