# Documentation

Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

# 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 : ()) :
fRingHom.ker (smoothSheafCommRing.eval IM () 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} [] {EM : Type u_1} [] [NormedSpace 𝕜 EM] {HM : Type u_2} [] (IM : ModelWithCorners 𝕜 EM HM) {M : Type u} [] [ChartedSpace HM M] (x : M) :
nonunits () = (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 ()

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

Equations
• One or more equations did not get rendered due to their size.
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
• One or more equations did not get rendered due to their size.
Instances For