Smooth manifolds as locally ringed spaces #

This file equips a smooth manifold-with-corners 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 #

• SmoothManifoldWithCorners.locallyRingedSpace: A smooth manifold-with-corners 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} [] {EM : Type u_1} [] [NormedSpace 𝕜 EM] {HM : Type u_2} [] (IM : ModelWithCorners 𝕜 EM HM) {M : Type u} [] [ChartedSpace HM M] {x : M} (f : ((smoothSheafCommRing IM 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} [] {EM : Type u_1} [] [NormedSpace 𝕜 EM] {HM : Type u_2} [] (IM : ModelWithCorners 𝕜 EM HM) {M : Type u} [] [ChartedSpace HM M] (x : M) :
nonunits ((smoothSheafCommRing IM M 𝕜).presheaf.stalk x) = (RingHom.ker (smoothSheafCommRing.eval IM 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} [] {EM : Type u_1} [] [NormedSpace 𝕜 EM] {HM : Type u_2} [] (IM : ModelWithCorners 𝕜 EM HM) {M : Type u} [] [ChartedSpace HM M] (x : M) :
LocalRing ((smoothSheafCommRing IM M 𝕜).presheaf.stalk x)

The stalks of the structure sheaf of a smooth manifold-with-corners are local rings.

Equations
• =
def SmoothManifoldWithCorners.locallyRingedSpace {𝕜 : Type u} [] {EM : Type u_1} [] [NormedSpace 𝕜 EM] {HM : Type u_2} [] (IM : ModelWithCorners 𝕜 EM HM) (M : Type u) [] [ChartedSpace HM M] :

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

Equations
• = { carrier := , presheaf := , IsSheaf := , localRing := }
Instances For