# 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}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{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 (smoothSheafCommRing.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 𝕜]
[CompleteSpace 𝕜]
{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 (smoothSheafCommRing.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 𝕜]
[CompleteSpace 𝕜]
{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)
:

LocalRing ↑((smoothSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) 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}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{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-with-corners can be considered as a locally ringed space.

## Equations

- SmoothManifoldWithCorners.locallyRingedSpace IM M = { carrier := TopCat.of M, presheaf := smoothPresheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜, IsSheaf := ⋯, localRing := ⋯ }