General facts about the length of a module

Mathlib defines Module.length R M as the Krull dimension of the lattice of submodules and proves that it is additive in short exact sequences. This file adds the facts about it that a length-counting argument needs but Mathlib does not yet have: monotonicity in the submodule quotiented by, additivity along a filtration, the length of an image, the fact that finitely generated submodules already see the whole length, the ascent of finite length along a scalar tower, the length of I ⧸ aI for an ideal I, the length of R ⧸ 𝔪 for a local ring, the finite length of a quotient of a noetherian local ring by a maximal-primary ideal, and the infinite length of a ring of positive Krull dimension over itself.

The finite-generation reduction is the load-bearing one. Module.length is a supremum over strictly increasing chains, and any finite chain — in particular any one witnessing a finite lower bound on the length — is realised inside a finitely generated submodule, spanned by one element taken from each of its steps. So a uniform bound on finitely generated submodules is a bound on the module.

Multiplication by a ring element a on a module M is written throughout as LinearMap.range (LinearMap.lsmul A M a), which is the submodule aM. Mathlib spells the same submodule pointwise, as a • ⊤, and quotients by it in QuotSMulTop. TauCeti.map_lsmul_eq_smul is the single bridge between the two readings: TauCeti.range_lsmul_eq_smul_top and hence TauCeti.length_quotient_lsmul_congr are derived from it, so that Mathlib's QuotSMulTop API applies to the quotients appearing here without any further appeal to defeq.

Main results

• TauCeti.length_quotient_anti: M ⧸ Q is no longer than M ⧸ P when P ≤ Q.
• TauCeti.length_quotient_eq_length_map_add_length_quotient_sup: additivity along a filtration.
• TauCeti.length_map_mkQ: the length of the image of N in M ⧸ P.
• TauCeti.length_le_of_forall_fg: a bound on all finitely generated submodules bounds the length.
• TauCeti.isFiniteLength_of_tower: finite length over R gives finite length over any A acting compatibly.
• TauCeti.map_lsmul_eq_smul and TauCeti.range_lsmul_eq_smul_top: aN and aM as Mathlib's pointwise a • N and a • ⊤.
• TauCeti.comap_subtype_map_lsmul: aN computed inside N agrees with aN computed in the ambient module.
• TauCeti.length_quotient_lsmul_congr: the length of M ⧸ aM is a linear-equivalence invariant.
• TauCeti.length_quotient_lsmul_le_of_forall_fg: the finite-generation reduction for M ⧸ aM.
• TauCeti.isFiniteLength_quotient_of_nonZeroDivisor_mem: A ⧸ I has finite length when I contains a non-zero-divisor.
• TauCeti.length_quotient_lsmul_ideal_eq_ord: length (I ⧸ aI) = Ring.ord A a for an ideal I with A ⧸ I of finite length.
• TauCeti.length_quotient_maximalIdeal_eq_one: length (A ⧸ 𝔪) = 1 for a local ring A.
• TauCeti.length_self_eq_top_of_ringKrullDim_pos: a ring of positive Krull dimension has infinite length over itself.
• Ideal.isFiniteLength_quotient_of_radical_eq_maximalIdeal: A ⧸ I has finite length when the radical of I is the maximal ideal of a noetherian local ring. It is in the namespace of Ideal rather than that of TauCeti because its first explicit argument is an ideal, so that a consumer reads it as I.isFiniteLength_quotient_of_radical_eq_maximalIdeal.

theorem TauCeti.length_quotient_anti {A : Type u_1} {M : Type u_2} [Ring A] [AddCommGroup M] [Module A M] {P Q : Submodule A M} (h : P ≤ Q) : Module.length A (M ⧸ Q) ≤ Module.length A (M ⧸ P)

Quotienting by a larger submodule cannot increase length.

theorem TauCeti.length_quotient_eq_length_map_add_length_quotient_sup {A : Type u_1} {M : Type u_2} [Ring A] [AddCommGroup M] [Module A M] (N P : Submodule A M) : Module.length A (M ⧸ P) = Module.length A ↥(Submodule.map P.mkQ N) + Module.length A (M ⧸ P ⊔ N)

Filtration additivity. The image of N in M ⧸ P and the further quotient M ⧸ (P ⊔ N) account between them for the whole of M ⧸ P.

theorem TauCeti.length_map_mkQ {A : Type u_1} {M : Type u_2} [Ring A] [AddCommGroup M] [Module A M] (N P : Submodule A M) : Module.length A ↥(Submodule.map P.mkQ N) = Module.length A (↥N ⧸ Submodule.comap N.subtype P)

The image of N in M ⧸ P has the length of N ⧸ (N ⊓ P), for any P; in particular no P ≤ N is needed.

theorem TauCeti.length_le_of_forall_fg {A : Type u_1} {M : Type u_2} [Ring A] [AddCommGroup M] [Module A M] {c : ℕ∞} (h : ∀ (N : Submodule A M), N.FG → Module.length A ↥N ≤ c) : Module.length A M ≤ c

Length is detected by finitely generated submodules.

theorem TauCeti.isFiniteLength_of_tower {A : Type u_1} {M : Type u_2} [Ring A] [AddCommGroup M] [Module A M] (R : Type u_3) [Ring R] [SMul R A] [Module R M] [IsScalarTower R A M] (h : IsFiniteLength R M) : IsFiniteLength A M

Finite length ascends along a scalar tower. A module of finite length over R has finite length over any S acting compatibly, since its S-submodules are among its R-submodules.

theorem TauCeti.map_lsmul_eq_smul {A : Type u_1} {M : Type u_2} [CommSemiring A] [AddCommMonoid M] [Module A M] (N : Submodule A M) (a : A) : Submodule.map ((LinearMap.lsmul A M) a) N = a • N

aN, written as the image of the submodule N under multiplication by a, is the pointwise scalar multiple a • N. This is the only bridge between the two readings of aN; the rest of this file meets Mathlib's pointwise API through it.

theorem TauCeti.range_lsmul_eq_smul_top {A : Type u_1} {M : Type u_2} [CommSemiring A] [AddCommMonoid M] [Module A M] (a : A) : ((LinearMap.lsmul A M) a).range = a • ⊤

aM, written as the range of multiplication by a, is the pointwise scalar multiple a • ⊤ that Mathlib's QuotSMulTop quotients by.

@[simp]

theorem TauCeti.comap_subtype_map_lsmul {A : Type u_1} {M : Type u_2} [CommSemiring A] [AddCommMonoid M] [Module A M] (N : Submodule A M) (a : A) : Submodule.comap N.subtype (Submodule.map ((LinearMap.lsmul A M) a) N) = ((LinearMap.lsmul A ↥N) a).range

For a submodule N, the elements of N lying in aN computed in the ambient module are exactly the elements of aN computed in N.

theorem TauCeti.length_quotient_lsmul_congr {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] {N : Type u_3} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) (a : A) : Module.length A (M ⧸ ((LinearMap.lsmul A M) a).range) = Module.length A (N ⧸ ((LinearMap.lsmul A N) a).range)

The length of M ⧸ aM depends on M only through its linear equivalence class.

This proves nothing that Mathlib does not: it is QuotSMulTop.congr read through range_lsmul_eq_smul_top, and exists only so that the change of spelling is not repeated at each call site. It is stated forward-only, because rewriting back out of a QuotSMulTop-shaped goal is not type-correct — the AddCommGroup instance on the quotient depends on the submodule being rewritten.

theorem TauCeti.length_quotient_lsmul_le_of_forall_fg {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] {a : A} {c : ℕ∞} (h : ∀ (N : Submodule A M), N.FG → Module.length A (↥N ⧸ ((LinearMap.lsmul A ↥N) a).range) ≤ c) : Module.length A (M ⧸ ((LinearMap.lsmul A M) a).range) ≤ c

Reduction of the length of M ⧸ aM to finitely generated submodules.

theorem TauCeti.isFiniteLength_quotient_of_nonZeroDivisor_mem {A : Type u_1} [CommRing A] [IsNoetherianRing A] [Ring.KrullDimLE 1 A] (I : Ideal A) {x : A} (hxI : x ∈ I) (hx : x ∈ nonZeroDivisors A) : IsFiniteLength A (A ⧸ I)

In a Noetherian ring of Krull dimension at most one, the quotient by an ideal containing a non-zero-divisor has finite length.

theorem TauCeti.length_quotient_lsmul_ideal_eq_ord {A : Type u_1} [CommRing A] (I : Ideal A) (hI : IsFiniteLength A (A ⧸ I)) (a : A) (ha : a ∈ nonZeroDivisors A) : Module.length A (↥I ⧸ ((LinearMap.lsmul A ↥I) a).range) = Ring.ord A a

The length of I ⧸ aI for an ideal I. For an ideal I with A ⧸ I of finite length and a non-zero-divisor a, length (I ⧸ aI) is the order of vanishing Ring.ord A a, which is by definition length (A ⧸ aA).

Both sides are read off length (A ⧸ aI), which splits in two ways. Mathlib's exact sequence A ⧸ I ↪ A ⧸ aI ↠ A ⧸ aA — multiplication by a, then quotienting further, from Ideal.exact_mulQuot_quotOfMul — splits it as length (A ⧸ I) + length (A ⧸ aA), while the filtration aI ≤ I ≤ A splits it as length (I ⧸ aI) + length (A ⧸ I). Cancelling the common term, finite by hypothesis, leaves the claim.

@[simp]

theorem TauCeti.length_quotient_maximalIdeal_eq_one {A : Type u_1} [CommRing A] [IsLocalRing A] : Module.length A (A ⧸ IsLocalRing.maximalIdeal A) = 1

The length of a quotient by the maximal ideal of a local ring is one, the quotient being the residue field.

theorem Ideal.isFiniteLength_quotient_of_radical_eq_maximalIdeal {A : Type u_1} [CommRing A] [IsNoetherianRing A] [IsLocalRing A] (I : Ideal A) (hI : I.radical = IsLocalRing.maximalIdeal A) : IsFiniteLength A (A ⧸ I)

A quotient by a maximal-primary ideal has finite length. Let (A, 𝔪) be a noetherian local ring and let I be an ideal whose radical is 𝔪, so that I is maximal-primary. Then A ⧸ I is a noetherian local ring, its maximal ideal is the image of 𝔪, and 𝔪 ⁿ ≤ I for some power 𝔪 ⁿ of 𝔪, so that maximal ideal is nilpotent. A noetherian local ring with nilpotent maximal ideal is Artinian, and A ⧸ I is then both noetherian and Artinian as an A-module, which is finite length.

@[simp]

theorem TauCeti.length_self_eq_top_of_ringKrullDim_pos {A : Type u_1} [CommRing A] (hpos : 0 < ringKrullDim A) : Module.length A A = ⊤

A ring of positive Krull dimension has infinite length over itself. A ring of finite length over itself is both noetherian and Artinian, by Module.length_ne_top_iff and isFiniteLength_iff_isNoetherian_isArtinian, and a commutative Artinian ring is of Krull dimension zero, by isArtinianRing_iff_isNoetherianRing_krullDimLE_zero. So a ring of positive Krull dimension is of infinite length over itself, and the hypothesis is what rules out the zero-dimensional case, the trivial ring among it, whose ringKrullDim is ⊥ rather than 0 and which is of length zero over itself.

In particular the length of a one-dimensional local domain over itself is infinite, which is what a length read along such a domain, the order of vanishing of an element of it, has to be measured against.