Auxiliary file: Eisenstein monogenicity—integers L is generated by x #
For a root x of an Eisenstein polynomial over 𝒪[K] in SeparableClosure K, the integral closure
of 𝒪[K] in K⟮x⟯ is generated by x itself ([Serre 1979, Chap. I, §6, Prop. 17][Serre1979]). The
proof is the classical two-step denominator chase, powered by two Mathlib lemmas:
Algebra.discr_mul_isIntegral_mem_adjoin clears an integral element into the adjoin after
multiplication by the discriminant of the power basis—nonzero by separability, which is free inside
SeparableClosure K—and mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt strips prime
powers, the discriminant being a unit times a power of the uniformizer in the discrete valuation
ring 𝒪[K]. This file sits below First.lean and Discriminant.lean in the import graph: the
total-ramifiedness of K⟮x⟯ (isTotallyRamified_adjoin, below) and the discriminant bound
n - 1 ≤ d L (sub_one_le_d_adjoin) are computations inside 𝒪[K][x] made possible by this
identification.
References #
- [Serre1979] J-P. Serre, Local fields, Graduate Texts in Mathematics 67, Springer, 1979. (The English translation of Corps locaux, whose numbering it keeps.)
Instances Mathlib does not reach #
Two links of the tower 𝒪[K] → L → SeparableClosure K that instance search no longer finds on its
own: IntermediateField.isScalarTower wants the base to act on K, and FaithfulSMul over
SeparableClosure K is only reachable through IsFractionRing 𝒪[K] K, which is not a global
instance. Both are needed by minpoly and isIntegral_algebraMap_iff throughout this file.
The constant coefficient of the Eisenstein minimal polynomial is an associate of the uniformizer.
A root of an Eisenstein polynomial is monogenic: the integral closure of 𝒪[K] in
K⟮x⟯ is generated by x itself.
Total ramifiedness of the adjoined root field #
Three abstract commutative-algebra lemmas—kept over opaque rings so that unification stays
structural—followed by the concrete theorem. The route avoids constructing any valuation on
L = K⟮x⟯: from the Eisenstein relation, the constant coefficient satisfies a₀ * u = -ξ ^ n for a
unit u = 1 + ξ * t, so the extended maximal ideal is exactly the n-th power of (ξ); the ideal
(ξ) is maximal as the kernel of the constant-coefficient-then-residue map through the monogenic
presentation of integers L as 𝒪[K][X] modulo (g) from integers_eq_adjoin; and
Ideal.ramificationIdx'_spec turns the two power bounds into e = n, which is the degree.
If evaluation at z is a surjection R[X] → A with kernel (g), where the maximal
ideal of the local ring R is generated by the constant coefficient of g, whose image lies in
(z), then (z) is maximal: it is the kernel of the induced map onto the residue field of R.
(Not private: RootLifting.lean reuses it to make the integral closure local.)
Total ramifiedness of the adjoined root field #
The unit relation behind total ramifiedness, exposed for the discriminant bound of
sub_one_le_d_adjoin: the constant coefficient of the minimal polynomial becomes a unit multiple of
-ξ ^ n inside the integral closure.