smoothSheafCommRing.nonunits_stalk
theorem smoothSheafCommRing.nonunits_stalk :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {EM : Type u_1}
[inst_2 : NormedAddCommGroup EM] [inst_3 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_4 : TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM) {M : Type u} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace HM M] (x : M),
nonunits ↑((smoothSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜).presheaf.stalk x) =
↑(RingHom.ker (smoothSheafCommRing.eval IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x))
The theorem `smoothSheafCommRing.nonunits_stalk` states that for any non-trivially normed and complete space `𝕜`, a normed additive commutative group `EM`, a normed space `𝕜 EM`, a topological space `HM`, a model with corners `IM` from `EM` to `HM`, a topological space `M`, and a charted space `HM M` with a point `x` in `M`, the set of non-invertible elements (or non-units) of the stalk at `x` of the sheaf of smooth functions from `M` to `𝕜` (when considered as a sheaf of commutative rings) is precisely the set of functions whose values at `x` are zero. In other words, a function is a non-unit of this stalk if and only if it evaluates to zero at `x`. This is represented as the kernel of the evaluation map of the sheaf of smooth functions at `x`.
More concisely: The set of non-units in the stalk of the sheaf of smooth functions from a topological space to a non-trivially normed and complete ring at a point is equal to the kernel of the evaluation map at that point.
|
smoothSheafCommRing.isUnit_stalk_iff
theorem smoothSheafCommRing.isUnit_stalk_iff :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {EM : Type u_1}
[inst_2 : NormedAddCommGroup EM] [inst_3 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_4 : TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM) {M : Type u} [inst_5 : TopologicalSpace M] [inst_6 : 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 theorem `smoothSheafCommRing.isUnit_stalk_iff` states that for any point `x` in a manifold `M`, a function `f` in the stalk at `x` of the sheaf of smooth functions from `M` to a field `𝕜` (considered as a sheaf of commutative rings) is a unit (i.e., it has a two-sided inverse) if and only if the value of `f` at `x` is non-zero. This is expressed as `f` not lying in the kernel of the ring homomorphism given by the evaluation map at `x`, which sends each function to its value at `x`.
More concisely: A function in the stalk of a sheaf of smooth functions at a point is a unit if and only if its value at that point is non-zero.
|