AdjoinRoot.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

11 declarations, 0 contain sorry, 0 declared as axioms

`R[X]/(P)` as an unramified discrete valuation ring

Proposed new Mathlib file Mathlib.RingTheory.DiscreteValuationRing.AdjoinRoot: for a monic P over a discrete valuation ring R with irreducible reduction, S = R[X]/(P) is a discrete valuation ring, unramified over R, with fraction field K[X]/(P) and residue field k[X]/(P̄); separability of simple extensions; auxiliary local-ring lemmas.

Imports (9)

Imported by 2 files

theorem IsDiscreteValuationRing.injective_of_not_maximalIdeal_le_ker Documented declaration: injective_of_not_maximalIdeal_le_ker line 37 source
Source documentation
A ring homomorphism from a discrete valuation ring to a domain is injective as soon as its kernel does not contain the maximal ideal: the kernel is a prime ideal, so it is either ⊥ or the maximal ideal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDomain, IsDiscreteValuationRing, RingHom, Not, LE.le, Ideal, IsLocalRing.maximalIdeal, RingHom.ker, Function.Injective
Proof uses: Eq.mpr, Eq, Bot.bot, id, congrArg, propext, RingHom.injective_iff_ker_eq_bot, Decidable.byContradiction, Eq.ge, IsLocalRing.eq_maximalIdeal, Ideal.IsPrime.isMaximal, RingHom.ker_isPrime
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem IsDiscreteValuationRing.injective_of_not_maximalIdeal_le_ker {S L : Type*} [CommRing S]
    [IsDomain S] [IsDiscreteValuationRing S] [CommRing L] [IsDomain L] (φ : S →+* L)
    (h : ¬maximalIdeal S ≤ RingHom.ker φ) : Function.Injective φ := by
…
```
theorem Field.exists_monic_irreducible_adjoinRoot_algEquiv Documented declaration: exists_monic_irreducible_adjoinRoot_algEquiv line 46 source
Source documentation
A finite separable field extension k'/k is k[X]/(p) for a monic separable irreducible polynomial p of degree [k' : k] (the primitive element theorem, packaged via AdjoinRoot).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, FiniteDimensional, Algebra.IsSeparable, Exists, Polynomial, And, Polynomial.Monic, Polynomial.Separable, Irreducible, Eq, Nat, Polynomial.natDegree, Module.finrank, Nonempty, AlgEquiv, AdjoinRoot
Proof uses: PowerBasis, Field.powerBasisOfFiniteOfSeparable, rfl, IsIntegral, PowerBasis.gen, Algebra.IsIntegral.isIntegral, Exists.intro, minpoly, And.intro, minpoly.monic, Algebra.IsSeparable.isSeparable, minpoly.irreducible, Eq.mpr, PowerBasis.dim, id, congrArg, PowerBasis.natDegree_minpoly, PowerBasis.finrank, Eq.refl, Nonempty.intro and 10 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem Field.exists_monic_irreducible_adjoinRoot_algEquiv (k k' : Type*) [Field k] [Field k']
    [Algebra k k'] [FiniteDimensional k k'] [Algebra.IsSeparable k k'] :
    ∃ p : k[X], p.Monic ∧ p.Separable ∧ Irreducible p ∧ p.natDegree = Module.finrank k k' ∧
      Nonempty (AdjoinRoot p ≃ₐ[k] k') := by
…
```
theorem IsLocalRing.exists_monic_map_residue_eq A monic polynomial over the residue field of a local ring lifts to a monic polynomial of the same degree over the ring line 58 source
Source documentation
A monic polynomial over the residue field of a local ring lifts to a monic polynomial of the same degree over the ring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Polynomial, IsLocalRing.ResidueField, Polynomial.Monic, Exists, And, Eq, Polynomial.map, IsLocalRing.residue, Nat, Polynomial.natDegree
Proof uses: Polynomial.map_surjective, Ideal.Quotient.mk_surjective, IsLocalRing.maximalIdeal, Polynomial.lifts_and_natDegree_eq_and_monic, Exists.intro, RingHom, Polynomial.mapRingHom, And.intro
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem IsLocalRing.exists_monic_map_residue_eq {A : Type u} [CommRing A] [IsLocalRing A]
    {pbar : (ResidueField A)[X]} (h : pbar.Monic) :
    ∃ P : A[X], P.Monic ∧ P.map (residue A) = pbar ∧ P.natDegree = pbar.natDegree := by
…
```
theorem IsLocalRing.of_isMaximal_map_maximalIdeal Documented declaration: of_isMaximal_map_maximalIdeal line 69 source
Source documentation
An integral algebra S over a local ring R such that 𝔪_R · S is a maximal ideal is itself local, with maximal ideal 𝔪_R · S: any maximal ideal of S contracts to 𝔪_R by integrality, hence contains 𝔪_R · S, hence equals it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Algebra, Algebra.IsIntegral, Ideal.IsMaximal, Ideal.map, RingHom, Algebra.algebraMap, IsLocalRing.maximalIdeal
Proof uses: IsLocalRing.of_unique_max_ideal, Exists.intro, Ideal, And, Eq, And.intro, Ideal.comap, Ideal.isMaximal_under_of_isIntegral_of_isMaximal, LE.le, Eq.mpr, id, congrArg, Eq.symm, IsLocalRing.eq_maximalIdeal, Ideal.map_comap_le, Ideal.IsMaximal.eq_of_le, Ideal.IsMaximal.ne_top
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem IsLocalRing.of_isMaximal_map_maximalIdeal {R S : Type*} [CommRing R] [IsLocalRing R]
    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S]
    (hmax : ((maximalIdeal R).map (algebraMap R S)).IsMaximal) : IsLocalRing S :=
…
```
def AdjoinRoot.residueFieldEquiv If S = A[X]/(P) is local with maximal ideal 𝔪_A · S, then its residue field is (A/𝔪_A)[X]/(P mod 𝔪_A) line 81 source
Source documentation
If S = A[X]/(P) is local with maximal ideal 𝔪_A · S, then its residue field is (A/𝔪_A)[X]/(P mod 𝔪_A).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Polynomial, AdjoinRoot, Eq, Ideal, IsLocalRing.maximalIdeal, Ideal.map, RingHom, Algebra.algebraMap, AlgEquiv, IsLocalRing.ResidueField, Polynomial.map, IsLocalRing.residue
Proof uses: AlgEquiv.trans, HasQuotient.Quotient, Ideal.quotientEquivAlgOfEq, AdjoinRoot.quotEquivQuotMap
28 instances, coercions and auxiliary constants left out.
```
noncomputable def AdjoinRoot.residueFieldEquiv {A : Type*} [CommRing A] [IsLocalRing A]
    {P : A[X]} [IsLocalRing (AdjoinRoot P)]
    (hmax : maximalIdeal (AdjoinRoot P) = (maximalIdeal A).map (algebraMap A (AdjoinRoot P))) :
    ResidueField (AdjoinRoot P) ≃ₐ[A] AdjoinRoot (P.map (residue A)) :=
…
```
theorem AdjoinRoot.isSeparable_root The root of an irreducible separable polynomial q is a separable element of F[X]/(q): its minimal polynomial is q up to a unit line 89 source
Source documentation
The root of an irreducible separable polynomial q is a separable element of F[X]/(q): its minimal polynomial is q up to a unit.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Polynomial, Fact, Irreducible, Polynomial.Separable, IsSeparable, AdjoinRoot, AdjoinRoot.root
Proof uses: Ne, OfNat.ofNat, Irreducible.ne_zero, Fact.out, Eq.mpr, HMul.hMul, RingHom, Polynomial.C, Inv.inv, Polynomial.leadingCoeff, id, Eq, congrArg, minpoly, AdjoinRoot.minpoly_root, Polynomial.Separable.mul_unit, Iff.mpr, IsUnit, Polynomial.isUnit_C, isUnit_iff_ne_zero and 2 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem AdjoinRoot.isSeparable_root {F : Type*} [Field F] {q : F[X]} [Fact (Irreducible q)]
    (hq : q.Separable) : IsSeparable F (root q) := by
…
```
theorem AdjoinRoot.isSeparable_of_separable The simple extension F[X]/(q) by a root of an irreducible separable polynomial is separable line 98 source
Source documentation
The simple extension F[X]/(q) by a root of an irreducible separable polynomial is separable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Polynomial, Fact, Irreducible, Polynomial.Separable, Algebra.IsSeparable, AdjoinRoot
Proof uses: Algebra.IsSeparable.of_isSeparable_of_adjoin_eq_top, AdjoinRoot.root, AdjoinRoot.isSeparable_root, IntermediateField.adjoin_eq_top_of_algebra, Singleton.singleton, Set, AdjoinRoot.adjoinRoot_eq_top
23 instances, coercions and auxiliary constants left out.
```
theorem AdjoinRoot.isSeparable_of_separable {F : Type*} [Field F] {q : F[X]} [Fact (Irreducible q)]
    (hq : q.Separable) : Algebra.IsSeparable F (AdjoinRoot q) :=
…
```
theorem AdjoinRoot.isMaximal_map_maximalIdeal If the reduction of P modulo the maximal ideal of a local ring A is irreducible, then 𝔪_A · A[X]/(P) is a maximal ideal: the quotient by it is the field (A/𝔪_A)[X]/(P̄) line 105 source
Source documentation
If the reduction of P modulo the maximal ideal of a local ring A is irreducible, then 𝔪_A · A[X]/(P) is a maximal ideal: the quotient by it is the field (A/𝔪_A)[X]/(P̄).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Polynomial, Irreducible, IsLocalRing.ResidueField, Polynomial.map, IsLocalRing.residue, Ideal.IsMaximal, AdjoinRoot, Ideal.map, RingHom, Algebra.algebraMap, IsLocalRing.maximalIdeal
Proof uses: Fact, Fact.mk, Eq.mpr, AdjoinRoot.of, id, Eq, congrArg, AdjoinRoot.algebraMap_eq, Ideal.Quotient.maximal_of_isField, MulEquiv.isField, HasQuotient.Quotient, Ideal, Field.toIsField, RingEquiv.toMulEquiv, Ideal.span, Singleton.singleton, Set, Ideal.Quotient.mk, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot
38 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem AdjoinRoot.isMaximal_map_maximalIdeal {A : Type*} [CommRing A] [IsLocalRing A] {P : A[X]}
    (hirr : Irreducible (P.map (residue A))) :
    ((maximalIdeal A).map (algebraMap A (AdjoinRoot P))).IsMaximal := by
…
```
theorem AdjoinRoot.isDiscreteValuationRing_of_irreducible_map_residue Documented declaration: isDiscreteValuationRing_of_irreducible_map_residue line 121 source
Source documentation
For a monic P over a discrete valuation ring R whose reduction is irreducible over the residue field, S = R[X]/(P) is again a discrete valuation ring, unramified over R: its maximal ideal is 𝔪_R · S (residue field (ResidueField R)[X]/(P̄)), so R → S is a local homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDomain, IsDiscreteValuationRing, Polynomial, AdjoinRoot, Polynomial.Monic, Ne, WithBot, Nat, Polynomial.degree, OfNat.ofNat, Irreducible, IsLocalRing.ResidueField, Polynomial.map, IsLocalRing.residue, And, Ideal.IsMaximal, Ideal.map, RingHom, Algebra.algebraMap and 2 more
Proof uses: Module.Finite, Polynomial.Monic.finite_adjoinRoot, Algebra.IsIntegral, AdjoinRoot.isMaximal_map_maximalIdeal, IsLocalRing, IsLocalRing.of_isMaximal_map_maximalIdeal, Eq, Ideal, Eq.symm, IsLocalRing.eq_maximalIdeal, Function.Injective, Eq.mpr, AdjoinRoot.of, id, congrArg, AdjoinRoot.algebraMap_eq, AdjoinRoot.of.injective_of_degree_ne_zero, Not, IsField, IsDiscreteValuationRing.not_a_field and 35 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem AdjoinRoot.isDiscreteValuationRing_of_irreducible_map_residue
    {P : R[X]} [IsDomain (AdjoinRoot P)] (hPm : P.Monic) (hP0 : P.degree ≠ 0)
    (hirr : Irreducible (P.map (residue R))) :
    ((maximalIdeal R).map (algebraMap R (AdjoinRoot P))).IsMaximal ∧
      IsDiscreteValuationRing (AdjoinRoot P) ∧ IsLocalHom (algebraMap R (AdjoinRoot P)) := by
…
```
theorem AdjoinRoot.exists_nonZeroDivisor_mul_eq_algebraMap Documented declaration: exists_nonZeroDivisor_mul_eq_algebraMap line 148 source
Source documentation
Clearing denominators in L = K[X]/(P·K) over S = R[X]/(P): any element of L, multiplied by (the image of) a suitable nonzero element of R, lies in the image of S (IsLocalization.integerNormalization for the polynomial g representing the element). The hypothesis hmap records that algebraMap S L reduces mk P to mk (P·K) ∘ map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, Algebra, IsFractionRing, Polynomial, AdjoinRoot, Polynomial.map, Algebra.algebraMap, Eq, RingHom, RingHom.comp, AdjoinRoot.mk, Polynomial.mapRingHom, Exists, And, Membership.mem, Submonoid, nonZeroDivisors, HMul.hMul
Proof uses: AdjoinRoot.mk_surjective, IsLocalization.integerNormalization, HSMul.hSMul, IsLocalization.integerNormalization_spec, Exists.intro, And.intro, RingHom.congr_fun, Polynomial.C, Eq.mpr, id, congrArg, IsScalarTower.algebraMap_apply, AdjoinRoot.of, AdjoinRoot.algebraMap_eq, Eq.symm, AdjoinRoot.mk_C, Eq.refl, Algebra.smul_def, Polynomial.algebraMap_eq, Eq.mp and 4 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem AdjoinRoot.exists_nonZeroDivisor_mul_eq_algebraMap {R : Type*} [CommRing R] {K : Type*}
    [Field K] [Algebra R K] [IsFractionRing R K] {P : R[X]}
    [Algebra (AdjoinRoot P) (AdjoinRoot (P.map (algebraMap R K)))]
    (hmap : (algebraMap (AdjoinRoot P) (AdjoinRoot (P.map (algebraMap R K)))).comp (mk P)
      = (mk (P.map (algebraMap R K))).comp (Polynomial.mapRingHom (algebraMap R K)))
    (z : AdjoinRoot (P.map (algebraMap R K))) :
    ∃ b ∈ nonZeroDivisors R, ∃ x : AdjoinRoot P,
      z * algebraMap R (AdjoinRoot (P.map (algebraMap R K))) b
        = algebraMap (AdjoinRoot P) (AdjoinRoot (P.map (algebraMap R K))) x := by
…
```
theorem AdjoinRoot.isFractionRing_map Documented declaration: isFractionRing_map line 177 source
Source documentation
L = K[X]/(P·K) = Frac(S) for S = R[X]/(P) a discrete valuation ring: algebraMap S L is injective (its kernel is a prime of the DVR S, and it does not kill a uniformizer), and every element of L clears its K-denominators (exists_nonZeroDivisor_mul_eq_algebraMap) to a multiple in the image of S. The hypothesis hmap records that algebraMap S L reduces mk P to mk (P·K) ∘ map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDomain, IsDiscreteValuationRing, Field, Algebra, IsFractionRing, Polynomial, Ne, WithBot, Nat, Polynomial.degree, OfNat.ofNat, AdjoinRoot, Fact, Irreducible, Polynomial.map, Algebra.algebraMap, IsScalarTower, Eq, Ideal and 6 more
Proof uses: Function.Injective, Eq.mpr, AdjoinRoot.of, id, congrArg, AdjoinRoot.algebraMap_eq, AdjoinRoot.of.injective_of_degree_ne_zero, Eq.mp, rfl, IsScalarTower.algebraMap_eq, Function.Injective.comp, RingHom.injective, IsFractionRing.injective, IsDiscreteValuationRing.injective_of_not_maximalIdeal_le_ker, LE.le, RingHom.ker, And, Membership.mem, Submodule, Exists and 31 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem AdjoinRoot.isFractionRing_map {P : R[X]} (hP0 : P.degree ≠ 0)
    [IsDomain (AdjoinRoot P)] [IsDiscreteValuationRing (AdjoinRoot P)]
    [Fact (Irreducible (P.map (algebraMap R K)))]
    [Algebra (AdjoinRoot P) (AdjoinRoot (P.map (algebraMap R K)))]
    [IsScalarTower R (AdjoinRoot P) (AdjoinRoot (P.map (algebraMap R K)))]
    (hmaxS : maximalIdeal (AdjoinRoot P) = (maximalIdeal R).map (algebraMap R (AdjoinRoot P)))
    (hmap : (algebraMap (AdjoinRoot P) (AdjoinRoot (P.map (algebraMap R K)))).comp (mk P)
      = (mk (P.map (algebraMap R K))).comp (Polynomial.mapRingHom (algebraMap R K))) :
    IsFractionRing (AdjoinRoot P) (AdjoinRoot (P.map (algebraMap R K))) := by
…
```

FLT/Mathlib/RingTheory/DiscreteValuationRing/AdjoinRoot.lean

R[X]/(P) as an unramified discrete valuation ring

`FLT/Mathlib/RingTheory/DiscreteValuationRing/AdjoinRoot.lean`

`R[X]/(P)` as an unramified discrete valuation ring