Local rings whose maximal ideal is generated by one or two elements

Let R be a local ring whose maximal ideal is generated by ϖ, for instance a valuation ring with a uniformizer. Then divisibility by ϖ describes the maximal ideal and the units, and if R is Noetherian, it has dimension at most one.

Consequently, if the maximal ideal of R is generated by x, y but is not principal, as when R is Noetherian of dimension two, then neither element generates it alone, and by Nakayama's lemma each lies outside the square of the maximal ideal.

Main results

• TauCeti.IsLocalRing.mem_maximalIdeal_iff_dvd: the maximal ideal consists of the multiples of ϖ.
• TauCeti.IsLocalRing.isUnit_iff_not_dvd: the units are the elements not divisible by ϖ.
• TauCeti.IsLocalRing.isUnit_add_of_dvd: a unit plus a multiple of ϖ is a unit.
• IsLocalRing.ringKrullDim_le_one_of_isPrincipal_maximalIdeal: a Noetherian local ring with principal maximal ideal has dimension at most one.
• IsLocalRing.not_isPrincipal_maximalIdeal_of_one_lt_ringKrullDim: so the maximal ideal of a Noetherian local ring of dimension greater than one is not principal.
• TauCeti.IsLocalRing.notMem_sq_of_span_pair_eq_maximalIdeal: in a local ring with non-principal maximal ideal, each element of a pair generating the maximal ideal lies outside its square.

theorem TauCeti.IsLocalRing.mem_maximalIdeal_iff_dvd {R : Type u_1} [CommSemiring R] [IsLocalRing R] {ϖ : R} (hϖ : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}) {z : R} : z ∈ IsLocalRing.maximalIdeal R ↔ ϖ ∣ z

In a local ring whose maximal ideal is generated by ϖ, membership in the maximal ideal is divisibility by ϖ.

theorem TauCeti.IsLocalRing.isUnit_iff_not_dvd {R : Type u_1} [CommSemiring R] [IsLocalRing R] {ϖ : R} (hϖ : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}) {z : R} : IsUnit z ↔ ¬ϖ ∣ z

In a local ring whose maximal ideal is generated by ϖ, an element is a unit exactly when it is not divisible by ϖ.

theorem TauCeti.IsLocalRing.isUnit_add_of_dvd {R : Type u_1} [CommRing R] [IsLocalRing R] {ϖ : R} (hϖ : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}) {a b : R} (ha : IsUnit a) (hb : ϖ ∣ b) : IsUnit (a + b)

In a local ring whose maximal ideal is generated by ϖ, a unit plus a multiple of ϖ is a unit.

theorem IsLocalRing.ringKrullDim_le_one_of_isPrincipal_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (h : Submodule.IsPrincipal (maximalIdeal R)) : ringKrullDim R ≤ 1

A Noetherian local ring whose maximal ideal is principal has dimension at most one.

theorem IsLocalRing.not_isPrincipal_maximalIdeal_of_one_lt_ringKrullDim {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hdim : 1 < ringKrullDim R) : ¬Submodule.IsPrincipal (maximalIdeal R)

The maximal ideal of a Noetherian local ring of dimension greater than one is not principal.

theorem TauCeti.IsLocalRing.mem_maximalIdeal_of_span_pair_eq_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] {x y : R} (hxy : Ideal.span {x, y} = IsLocalRing.maximalIdeal R) : x ∈ IsLocalRing.maximalIdeal R

The first element of a pair generating the maximal ideal lies in the maximal ideal.

theorem TauCeti.IsLocalRing.notMem_span_singleton_of_span_pair_eq_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] (hprin : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)) {x y : R} (hxy : Ideal.span {x, y} = IsLocalRing.maximalIdeal R) : y ∉ Ideal.span {x}

If the maximal ideal is not principal, neither element of a pair generating it generates it alone.

theorem TauCeti.IsLocalRing.ne_zero_of_span_pair_eq_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] (hprin : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)) {x y : R} (hxy : Ideal.span {x, y} = IsLocalRing.maximalIdeal R) : x ≠ 0

If the maximal ideal is not principal, each element of a pair generating it is nonzero.

theorem TauCeti.IsLocalRing.notMem_sq_of_span_pair_eq_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] (hprin : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)) {x y : R} (hxy : Ideal.span {x, y} = IsLocalRing.maximalIdeal R) : x ∉ IsLocalRing.maximalIdeal R ^ 2

In a local ring whose maximal ideal is not principal, each element of a pair generating the maximal ideal is a regular parameter: it does not lie in the square of the maximal ideal.