Defs.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

12 declarations, 0 contain sorry, 0 declared as axioms

The Hilbert–Samuel function, `d(R)`, and `δ(R)`

Definitions of the quantities compared by the dimension theorem for a Noetherian local ring (R, 𝔪) (the third, the Krull dimension, is Mathlib's ringKrullDim), together with basic finiteness and monotonicity lemmas.

Main definitions

DimensionTheorem.colength R I — the length ℓ_R(R ⧸ I) as a natural number (Module.length truncated at ⊤; by colength_coe nothing is lost when I is an ideal of definition).
DimensionTheorem.hilbertSamuel R — the Hilbert–Samuel function n ↦ ℓ_R(R ⧸ 𝔪ⁿ).
DimensionTheorem.growthDeg R — d(R), the least d such that ℓ(R ⧸ 𝔪ⁿ) = O(nᵈ).
DimensionTheorem.minGenPrimary R — δ(R), the least number of generators (Submodule.spanFinrank) of an ideal of definition of R, i.e. an ideal with radical 𝔪.

Main results

length_quotient_ne_top_of_radical_eq — quotients by ideals of definition have finite length; the Artinian input is Hopkins–Levitzki via Mathlib's IsNoetherianRing.isArtinianRing_of_krullDimLE_zero.
colength_le_colength, hilbertSamuel_monotone — comparison lemmas.
length_quotient_eq_add — additivity ℓ(R/I) = ℓ(J/I) + ℓ(R/J) for I ≤ J, from the exact sequence 0 → J/I → R/I → R/J → 0.

Design note

Classically (Atiyah–Macdonald Ch. 11; Stacks Project, tag 00KQ) d(R) is defined as the degree of the Hilbert–Samuel polynomial, whose existence is the Hilbert–Serre theorem. This development instead takes the growth-order formulation above, which requires no graded machinery; the two definitions agree once eventual polynomiality is known. Upgrading growthDeg to the polynomial degree (i.e. formalizing Hilbert–Serre) is the natural next step.

Imports (3)

Imported by 4 files

def DimensionTheorem.colength The length of R ⧸ I as a natural number (junk value 0 when the length is infinite; see colength_coe for the case of an ideal of definition) line 61 source
Source documentation
The length of R ⧸ I as a natural number (junk value 0 when the length is infinite; see colength_coe for the case of an ideal of definition).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Nat
Proof uses: ENat.toNat, Module.length, HasQuotient.Quotient
10 instances, coercions and auxiliary constants left out.
```
noncomputable def colength (I : Ideal R) : ℕ :=
…
```
def DimensionTheorem.hilbertSamuel The Hilbert–Samuel function of a local ring: n ↦ ℓ(R ⧸ 𝔪ⁿ) line 65 source
Source documentation
The Hilbert–Samuel function of a local ring: n ↦ ℓ(R ⧸ 𝔪ⁿ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Nat
Proof uses: DimensionTheorem.colength, HPow.hPow, Ideal, IsLocalRing.maximalIdeal
8 instances, coercions and auxiliary constants left out.
```
noncomputable def hilbertSamuel (n : ℕ) : ℕ :=
…
```
def DimensionTheorem.growthDeg The growth degree d(R) of the Hilbert–Samuel function: the least d such that ℓ(R ⧸ 𝔪ⁿ) = O(nᵈ) line 74 source
Source documentation
The growth degree d(R) of the Hilbert–Samuel function: the least d such that ℓ(R ⧸ 𝔪ⁿ) = O(nᵈ).
Classically, for a Noetherian local ring, this is the degree of the Hilbert–Samuel polynomial. The present development does not construct that eventual polynomial; it uses this Big-O formulation as the formal invariant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Nat
Proof uses: InfSet.sInf, Set.ofPred, DimensionTheorem.GrowthLE, DimensionTheorem.hilbertSamuel
5 instances, coercions and auxiliary constants left out.
```
noncomputable def growthDeg : ℕ :=
…
```
def DimensionTheorem.minGenPrimary δ(R): the minimal number of generators of an ideal of definition of R, i.e. of an 𝔪-primary ideal (an ideal with radical 𝔪) line 79 source
Source documentation
δ(R): the minimal number of generators of an ideal of definition of R, i.e. of an 𝔪-primary ideal (an ideal with radical 𝔪).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Ideal, And, Eq, Ideal.radical, IsLocalRing.maximalIdeal, Submodule.spanFinrank
7 instances, coercions and auxiliary constants left out.
```
noncomputable def minGenPrimary : ℕ :=
…
```
instance DimensionTheorem.(instance at line 84) line 84 source
Source documentation
A nontrivial quotient of a local ring is local. (Instance so that hilbertSamuel (R ⧸ I) elaborates.)
```
instance (I : Ideal R) [Nontrivial (R ⧸ I)] : IsLocalRing (R ⧸ I) :=
…
```
lemma DimensionTheorem.isArtinianRing_quotient_of_radical_eq A quotient by an ideal of definition is an Artinian ring line 94 source
Source documentation
A quotient by an ideal of definition is an Artinian ring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Ideal, Eq, Ideal.radical, IsLocalRing.maximalIdeal, IsArtinianRing, HasQuotient.Quotient
Proof uses: IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing, And.intro, And, Ideal.IsPrime, LE.le, Ideal.IsMaximal.isPrime, Eq.rec, Ideal.le_radical, Eq.mpr, id, congrArg, Eq.symm, Iff.mpr, Ideal.IsPrime.radical_le_iff, And.left, And.right
12 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma isArtinianRing_quotient_of_radical_eq {I : Ideal R}
    (h : I.radical = maximalIdeal R) : IsArtinianRing (R ⧸ I) := by
…
```
lemma DimensionTheorem.length_quotient_ne_top_of_radical_eq A quotient by an ideal of definition has finite length over R line 103 source
Source documentation
A quotient by an ideal of definition has finite length over R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Ideal, Eq, Ideal.radical, IsLocalRing.maximalIdeal, Ne, ENat, Module.length, HasQuotient.Quotient, Top.top
Proof uses: IsArtinian, DimensionTheorem.isArtinianRing_quotient_of_radical_eq, IsNoetherian, Eq.mpr, id, congrArg, Eq.symm, propext, isNoetherianRing_iff, inferInstance, Module.length_eq_of_surjective, Function.Surjective, RingHom, Algebra.algebraMap, Ideal.Quotient.mk, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.mk_surjective, Module.length_ne_top
31 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma length_quotient_ne_top_of_radical_eq {I : Ideal R}
    (h : I.radical = maximalIdeal R) : Module.length R (R ⧸ I) ≠ ⊤ := by
…
```
lemma DimensionTheorem.colength_coe For an ideal of definition, colength really is the length line 113 source
Source documentation
For an ideal of definition, colength really is the length.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Ideal, Eq, Ideal.radical, IsLocalRing.maximalIdeal, ENat, DimensionTheorem.colength, Module.length, HasQuotient.Quotient
Proof uses: Eq.mpr, ENat.toNat, id, congrArg, Nat, DimensionTheorem.colength.eq_1, ENat.natCast_toNat, DimensionTheorem.length_quotient_ne_top_of_radical_eq, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma colength_coe {I : Ideal R} (h : I.radical = maximalIdeal R) :
    (colength R I : ℕ∞) = Module.length R (R ⧸ I) := by
…
```
Mentions: DimensionTheorem.colength
lemma DimensionTheorem.radical_pow_eq_of_radical_eq Powers of an ideal of definition are ideals of definition line 120 source
Source documentation
Powers of an ideal of definition are ideals of definition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Ideal, Eq, Ideal.radical, IsLocalRing.maximalIdeal, Nat, Ne, OfNat.ofNat, HPow.hPow
Proof uses: Eq.mpr, id, congrArg, Ideal.radical_pow, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma radical_pow_eq_of_radical_eq {I : Ideal R} (h : I.radical = maximalIdeal R)
    {n : ℕ} (hn : n ≠ 0) : (I ^ n).radical = maximalIdeal R := by
…
```
lemma DimensionTheorem.colength_le_colength colength is antitone: a larger ideal has a smaller quotient line 132 source
Source documentation
colength is antitone: a larger ideal has a smaller quotient. The hypothesis that I is an ideal of definition guarantees finiteness.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Ideal, LE.le, Eq, Ideal.radical, IsLocalRing.maximalIdeal, Nat, DimensionTheorem.colength
Proof uses: Submodule.comap, RingHom.id, LinearMap.id, Eq.mpr, id, congrArg, Submodule, Submodule.comap_id, Function.Surjective, HasQuotient.Quotient, LinearMap, Submodule.mapQ, Submodule.Quotient.mk, Exists, Submodule.Quotient.mk_surjective, Exists.intro, rfl, ENat.toNat_le_toNat, Module.length, Module.length_le_of_surjective and 1 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma colength_le_colength {I J : Ideal R} (hIJ : I ≤ J)
    (h : I.radical = maximalIdeal R) : colength R J ≤ colength R I := by
…
```
Mentions: DimensionTheorem.colength
lemma DimensionTheorem.hilbertSamuel_monotone The Hilbert–Samuel function is monotone line 146 source
Source documentation
The Hilbert–Samuel function is monotone.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Monotone, Nat, DimensionTheorem.hilbertSamuel
Proof uses: monotone_nat_of_le_succ, DimensionTheorem.colength_le_colength, HPow.hPow, Ideal, IsLocalRing.maximalIdeal, HAdd.hAdd, OfNat.ofNat, Ideal.pow_le_pow_right, Nat.le_succ, DimensionTheorem.radical_pow_eq_of_radical_eq, Ideal.IsPrime.radical, Ideal.IsMaximal.isPrime, Nat.succ_ne_zero
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma hilbertSamuel_monotone : Monotone (hilbertSamuel R) := by
…
```
Mentions: DimensionTheorem.hilbertSamuel
lemma DimensionTheorem.length_quotient_eq_add Additivity of length along a pair of nested ideals I ≤ J, from the exact sequence 0 → J/I → R/I → R/J → 0 (valid in ℕ∞, no finiteness needed) line 156 source
Source documentation
Additivity of length along a pair of nested ideals I ≤ J, from the exact sequence 0 → J/I → R/I → R/J → 0 (valid in ℕ∞, no finiteness needed).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Ideal, LE.le, Eq, ENat, Module.length, HasQuotient.Quotient, HAdd.hAdd, Subtype, Submodule, Membership.mem, Submodule.map, RingHom.id, Submodule.mkQ
Proof uses: Submodule.comap, LinearMap.id, Eq.mpr, id, congrArg, Submodule.comap_id, Function.Surjective, LinearMap, Submodule.mapQ, Submodule.Quotient.mk, Exists, Submodule.Quotient.mk_surjective, Exists.intro, rfl, Module.length_eq_add_of_exact, Submodule.subtype, Submodule.subtype_injective, Function.Exact, LinearMap.ker, LinearMap.range and 5 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma length_quotient_eq_add (I J : Ideal R) (hIJ : I ≤ J) :
    Module.length R (R ⧸ I) =
      Module.length R (Submodule.map (Submodule.mkQ (I : Submodule R R)) (J : Submodule R R)) +
      Module.length R (R ⧸ J) := by
…
```

FLT/Slop/DimensionTheorem/Defs.lean

The Hilbert–Samuel function, d(R), and δ(R)

Main definitions

Main results

Design note

`FLT/Slop/DimensionTheorem/Defs.lean`

The Hilbert–Samuel function, `d(R)`, and `δ(R)`