Elements of 𝔪 \ 𝔪² in a local ring #
For a local ring R with maximal ideal 𝔪, elements of 𝔪 \ 𝔪² are the ones that can be part
of a minimal system of generators of 𝔪.
Main declarations #
TauCeti.IsLocalRing.spanFinrank_map_maximalIdeal_quotient_add_one_le: forx ∈ 𝔪 \ 𝔪², the maximal ideal ofR ⧸ (x)needs at least one generator fewer than𝔪;TauCeti.IsLocalRing.spanFinrank_map_maximalIdeal_quotient_of_le_sq: dividing out an ideal contained in𝔪²does not change the number of generators of the maximal ideal;TauCeti.IsLocalRing.exists_mem_maximalIdeal_notMem_sq_notMem_minimalPrimes: in a Noetherian local ring of positive dimension there isx ∈ 𝔪 \ 𝔪²outside every minimal prime.
theorem
TauCeti.IsLocalRing.spanFinrank_map_maximalIdeal_quotient_add_one_le
{R : Type u_1}
[CommRing R]
[IsLocalRing R]
(hfg : (IsLocalRing.maximalIdeal R).FG)
{x : R}
(hxm : x ∈ IsLocalRing.maximalIdeal R)
(hx : x ∉ IsLocalRing.maximalIdeal R ^ 2)
:
If x ∈ 𝔪 \ 𝔪², then the image of 𝔪 in R ⧸ (x), which is the maximal ideal of R ⧸ (x),
needs at least one generator fewer than 𝔪.
theorem
TauCeti.IsLocalRing.spanFinrank_map_maximalIdeal_quotient_of_le_sq
{R : Type u_1}
[CommRing R]
[IsLocalRing R]
(hfg : (IsLocalRing.maximalIdeal R).FG)
{I : Ideal R}
(hI : I ≤ IsLocalRing.maximalIdeal R ^ 2)
:
Dividing out an ideal contained in 𝔪² does not change the number of generators needed for
the maximal ideal: the image of 𝔪 in R ⧸ I needs exactly as many generators as 𝔪.
theorem
TauCeti.IsLocalRing.exists_mem_maximalIdeal_notMem_sq_notMem_minimalPrimes
{R : Type u_1}
[CommRing R]
[IsLocalRing R]
[IsNoetherianRing R]
(h : 0 < ringKrullDim R)
:
∃ x ∈ IsLocalRing.maximalIdeal R, x ∉ IsLocalRing.maximalIdeal R ^ 2 ∧ ∀ p ∈ minimalPrimes R, x ∉ p
In a Noetherian local ring of positive dimension there is an element of the maximal ideal which lies neither in its square nor in any minimal prime.