The maximal ideal has order one

[Kol07, Definition 47]: the order of an ideal I of a local ring is the largest r with I ⊆ 𝔪^r. For the maximal ideal itself of a Noetherian local ring that is not a field the order is exactly 1: 𝔪 ⊆ 𝔪 and, by Nakayama, 𝔪 ⊆ 𝔪² would force 𝔪 = 0. On a locally Noetherian scheme, an ideal sheaf whose stalk at x is the maximal ideal has order 1 at x: the order of the ideal of a reduced component at its generic point, as in the Claim in the proof of [Wlo05, Theorem 4.7.1], "the order of the controlled transform σ^c(I) of I is 1 along the strict transform of Y₁".

Used for the embedded resolution (Hironaka/Resolution/Algebraic/Wlo05/EmbeddedClaimTools.lean, Hironaka/Resolution/Algebraic/Wlo05/EmbeddedGenericOrder.lean).

theorem AlgebraicGeometry.ord_maximalIdeal_eq_one {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (h : IsLocalRing.maximalIdeal R ≠ ⊥) : IsLocalRing.ord (IsLocalRing.maximalIdeal R) = 1

The order ([Kol07, Definition 47]) of the maximal ideal of a Noetherian local ring that is not a field is 1 (Nakayama: 𝔪 ⊆ 𝔪² forces 𝔪 = 0).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_eq_one_of_stalkIdeal_eq_maximalIdeal {X : Scheme} [IsLocallyNoetherian X] (I : X.IdealSheafData) {x : ↥X} (h : I.stalkIdeal x = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x)) (hne : IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ≠ ⊥) : I.ord x = 1

An ideal sheaf whose stalk at x is the maximal ideal of a stalk that is not a field has order 1 at x.