Totally ramified extensions and Eisenstein polynomials

TheoremA generating uniformizer gives total ramification#✓fully proved

Let \(A \subseteq B\) be an extension of discrete valuation rings with \(B\) finite over \(A\) and the inclusion a local homomorphism, and let \(K \subseteq L\) be their fraction fields, with the maps \(A \to B \to L\) and \(A \to K \to L\) agreeing. If a uniformizer \(\pi\) of \(B\) satisfies \(B = A[\pi]\), then the ramification index of the maximal ideal of \(B\) over \(A\) equals \([L : K]\).

The proof shows that the inertia degree \(f\) of the maximal ideal of \(B\) over \(A\) is \(1\) and applies the identity \([L : K] = ef\), where \(e\) is the ramification index.

theorem ramificationIdx_eq_finrank_of_adjoin_uniformizer (π : B)
    (hπ : Irreducible π)
    (hadj : Algebra.adjoin A ({π} : Set B) = ⊤) :
    (IsLocalRing.maximalIdeal B).ramificationIdx A = Module.finrank K L

Uses 1 · Used by 2

Proof usesInertia degree one for a singly generated algebra

Used byEisenstein criterion for total ramification of discrete valuation rings · An Eisenstein generating uniformizer gives total ramification

TheoremAn Eisenstein generating uniformizer gives total ramification#✓fully proved

Let \(A \subseteq B\) be an extension of discrete valuation rings with \(B\) finite over \(A\) and the inclusion a local homomorphism, and let \(K \subseteq L\) be their fraction fields, with the maps \(A \to B \to L\) and \(A \to K \to L\) agreeing. If a uniformizer \(\pi\) of \(B\) satisfies \(B = A[\pi]\) and its minimal polynomial over \(A\) is Eisenstein at the maximal ideal of \(A\), then the ramification index of the maximal ideal of \(B\) over \(A\) equals \([L : K]\).

The Eisenstein hypothesis is not used: a generating uniformizer already suffices.

theorem ramificationIdx_eq_finrank_of_eisenstein_adjoin (π : B)
    (hπ : Irreducible π)
    (hadj : Algebra.adjoin A ({π} : Set B) = ⊤)
    (_heis : (minpoly A π).IsEisensteinAt (IsLocalRing.maximalIdeal A)) :
    (IsLocalRing.maximalIdeal B).ramificationIdx A = Module.finrank K L

Uses 1

Proof usesA generating uniformizer gives total ramification

TheoremTotally ramified extensions are generated by an Eisenstein uniformizer#✓fully proved

Let \(A \subseteq B\) be an extension of discrete valuation rings with \(B\) finite over \(A\) and the inclusion a local homomorphism, and let \(K \subseteq L\) be their fraction fields, with \(L\) finite over \(K\) and the maps \(A \to B \to L\) and \(A \to K \to L\) agreeing. If the ramification index of the maximal ideal of \(B\) over \(A\) equals \([L : K]\), then every uniformizer \(\pi\) of \(B\) satisfies \(B = A[\pi]\), and the minimal polynomial of \(\pi\) over \(A\) is Eisenstein at the maximal ideal of \(A\).

theorem eisenstein_adjoin_of_ramificationIdx_eq_finrank (π : B)
    (hπ : Irreducible π)
    (htotram : (IsLocalRing.maximalIdeal B).ramificationIdx A =
      Module.finrank K L) :
    Algebra.adjoin A ({π} : Set B) = ⊤ ∧
      (minpoly A π).IsEisensteinAt (IsLocalRing.maximalIdeal A)

Uses 1 · Used by 1

Proof usesThe extended maximal ideal is a power of the maximal ideal

Used byEisenstein criterion for total ramification of discrete valuation rings

TheoremEisenstein criterion for total ramification of discrete valuation rings#✓fully proved

Let \(A \subseteq B\) be an extension of discrete valuation rings with \(B\) finite over \(A\) and the inclusion a local homomorphism, and let \(K \subseteq L\) be their fraction fields, with \(L\) finite over \(K\) and the maps \(A \to B \to L\) and \(A \to K \to L\) agreeing. For a uniformizer \(\pi\) of \(B\), the ramification index of the maximal ideal of \(B\) over \(A\) equals \([L : K]\) if and only if \(B = A[\pi]\) and the minimal polynomial of \(\pi\) over \(A\) is Eisenstein at the maximal ideal of \(A\).

theorem ramificationIdx_eq_finrank_iff_eisenstein_adjoin (π : B)
    (hπ : Irreducible π) :
    (IsLocalRing.maximalIdeal B).ramificationIdx A = Module.finrank K L ↔
      Algebra.adjoin A ({π} : Set B) = ⊤ ∧
        (minpoly A π).IsEisensteinAt (IsLocalRing.maximalIdeal A)

Sources

• ATLAS NumberTheoryI, Theorem 11.5 (Sutherland, MIT 18.785, Lecture 11).

Uses 2

Proof usesTotally ramified extensions are generated by an Eisenstein uniformizer · A generating uniformizer gives total ramification

LemmaThe constant coefficient lies in the ideal generated by the adjoined root#✓fully proved

Let \(A\) be a commutative ring, let \(f \in A[X]\) be a polynomial, and let \(\alpha\) be the image of \(X\) in \(A[X]/(f)\). Then the image in \(A[X]/(f)\) of the constant coefficient \(f(0)\) of \(f\) lies in the principal ideal \((\alpha)\).

lemma algebraMap_coeff_zero_mem_span_root (f : A[X]) :
    algebraMap A (AdjoinRoot f) (f.coeff 0) ∈ Ideal.span {root f}

Used by 1

Used byThe maximal ideal of a DVR maps into the ideal of an Eisenstein root

LemmaThe constant term of an Eisenstein polynomial generates the maximal ideal of a DVR#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak m\), and let \(f \in A[X]\) be a polynomial of positive degree that is Eisenstein with respect to \(\mathfrak m\). Then \(\mathfrak m\) is the principal ideal generated by the constant coefficient \(f(0)\) of \(f\).

lemma maximalIdeal_eq_span_coeff_zero (f : A[X])
    (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hdeg : 0 < f.natDegree) :
    IsLocalRing.maximalIdeal A = Ideal.span {f.coeff 0}

Used by 1

Used byThe maximal ideal of a DVR maps into the ideal of an Eisenstein root

LemmaThe maximal ideal of a DVR maps into the ideal of an Eisenstein root#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak m\), let \(f \in A[X]\) be a polynomial of positive degree that is Eisenstein with respect to \(\mathfrak m\), and let \(\alpha\) be the image of \(X\) in \(A[X]/(f)\). Then the ideal of \(A[X]/(f)\) generated by the image of \(\mathfrak m\) is contained in the principal ideal \((\alpha)\).

lemma map_maximalIdeal_le_span_root {A : Type*} [CommRing A] [IsDomain A]
    [IsDiscreteValuationRing A] (f : A[X])
    (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hdeg : 0 < f.natDegree) :
    Ideal.map (algebraMap A (AdjoinRoot f)) (IsLocalRing.maximalIdeal A) ≤
      Ideal.span {root f}

Uses 2 · Used by 1

Proof usesThe constant coefficient lies in the ideal generated by the adjoined root · The constant term of an Eisenstein polynomial generates the maximal ideal of a DVR

Used byThe adjoined root of an Eisenstein polynomial generates a maximal ideal

LemmaThe adjoined root of an Eisenstein polynomial is nonzero#✓fully proved

Let \(A\) be a local integral domain with maximal ideal \(\mathfrak m\), let \(f \in A[X]\) be a monic polynomial of positive degree that is Eisenstein with respect to \(\mathfrak m\), and let \(\alpha\) be the image of \(X\) in \(A[X]/(f)\). Then \(\alpha \neq 0\).

lemma root_ne_zero {A : Type*} [CommRing A] [IsDomain A] [IsLocalRing A] (f : A[X])
    (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hf : f.Monic) (hdeg : 0 < f.natDegree) :
    root f ≠ 0

Used by 1

Used byAdjoining a root of an Eisenstein polynomial to a DVR gives a DVR

TheoremThe adjoined root of an Eisenstein polynomial generates a maximal ideal#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak m\), let \(f \in A[X]\) be a monic polynomial of positive degree that is Eisenstein with respect to \(\mathfrak m\), and let \(\alpha\) be the image of \(X\) in \(A[X]/(f)\). Then the principal ideal \((\alpha)\) of \(A[X]/(f)\) is a maximal ideal.

theorem isMaximal_span_root {A : Type*} [CommRing A] [IsDomain A]
    [IsDiscreteValuationRing A] (f : A[X])
    (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hf : f.Monic) (hdeg : 0 < f.natDegree) :
    (Ideal.span {root f}).IsMaximal

Uses 2 · Used by 2

Proof usesResidual irreducible factors give maximal ideals of a monogenic algebra · The maximal ideal of a DVR maps into the ideal of an Eisenstein root

Used byThe maximal ideal of an Eisenstein extension of a DVR is generated by the root · An Eisenstein extension of a DVR is local

TheoremEvery maximal ideal of an Eisenstein extension of a DVR contains the root#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak m\), let \(f \in A[X]\) be a monic polynomial that is Eisenstein with respect to \(\mathfrak m\), and let \(\alpha\) be the image of \(X\) in \(A[X]/(f)\). Then \(\alpha\) lies in every maximal ideal of \(A[X]/(f)\).

theorem root_mem_of_isMaximal {A : Type*} [CommRing A] [IsDomain A]
    [IsDiscreteValuationRing A] (f : A[X])
    (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hf : f.Monic)
    (m : Ideal (AdjoinRoot f)) (hm : m.IsMaximal) :
    root f ∈ m

Used by 1

Used byAn Eisenstein extension of a DVR is local

TheoremAn Eisenstein extension of a DVR is local#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak m\), and let \(f \in A[X]\) be a monic polynomial of positive degree that is Eisenstein with respect to \(\mathfrak m\). Then \(A[X]/(f)\) is a local ring.

theorem isLocalRing_of_isEisensteinAt {A : Type*} [CommRing A] [IsDomain A]
    [IsDiscreteValuationRing A] (f : A[X])
    (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hf : f.Monic) (hdeg : 0 < f.natDegree) :
    IsLocalRing (AdjoinRoot f)

Uses 2 · Used by 2

Proof usesThe adjoined root of an Eisenstein polynomial generates a maximal ideal · Every maximal ideal of an Eisenstein extension of a DVR contains the root

Used byThe adjoined root of an Eisenstein polynomial over a DVR is irreducible · Adjoining a root of an Eisenstein polynomial to a DVR gives a DVR

TheoremThe maximal ideal of an Eisenstein extension of a DVR is generated by the root#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak m\), let \(f \in A[X]\) be a monic polynomial of positive degree that is Eisenstein with respect to \(\mathfrak m\), and let \(\alpha\) be the image of \(X\) in \(A[X]/(f)\). If \(A[X]/(f)\) is a local ring, then its maximal ideal is the principal ideal \((\alpha)\).

theorem isLocalRing_maximalIdeal_eq_span_root {A : Type*} [CommRing A] [IsDomain A]
    [IsDiscreteValuationRing A] (f : A[X])
    (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hf : f.Monic) (hdeg : 0 < f.natDegree) [IsLocalRing (AdjoinRoot f)] :
    IsLocalRing.maximalIdeal (AdjoinRoot f) = Ideal.span {root f}

Uses 1 · Used by 2

Proof usesThe adjoined root of an Eisenstein polynomial generates a maximal ideal

Used byThe adjoined root of an Eisenstein polynomial over a DVR is irreducible · Adjoining a root of an Eisenstein polynomial to a DVR gives a DVR

TheoremAdjoining a root of an Eisenstein polynomial to a DVR gives a DVR#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak m\), and let \(f \in A[X]\) be a monic polynomial of positive degree that is Eisenstein with respect to \(\mathfrak m\). Then \(A[X]/(f)\) is a discrete valuation ring.

theorem isDiscreteValuationRing_of_isEisensteinAt
    {A : Type*} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    (f : A[X]) (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hf : f.Monic) (hdeg : 0 < f.natDegree) :
    @IsDiscreteValuationRing (AdjoinRoot f) _
      (AdjoinRoot.isDomain_of_prime
        (UniqueFactorizationMonoid.irreducible_iff_prime.mp
          (heis.irreducible (IsLocalRing.maximalIdeal.isMaximal A).isPrime
            hf.isPrimitive hdeg)))

Uses 3 · Used by 1

Proof usesThe maximal ideal of an Eisenstein extension of a DVR is generated by the root · An Eisenstein extension of a DVR is local · The adjoined root of an Eisenstein polynomial is nonzero

Used byThe adjoined root of an Eisenstein polynomial over a DVR is irreducible

TheoremThe adjoined root of an Eisenstein polynomial over a DVR is irreducible#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak m\), let \(f \in A[X]\) be a monic polynomial of positive degree that is Eisenstein with respect to \(\mathfrak m\), and let \(\alpha\) be the image of \(X\) in \(A[X]/(f)\). Then \(\alpha\) is an irreducible element of \(A[X]/(f)\).

theorem irreducible_root_of_isEisensteinAt
    {A : Type*} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    (f : A[X]) (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A))
    (hf : f.Monic) (hdeg : 0 < f.natDegree) :
    Irreducible (root f)

Uses 3

Proof usesAdjoining a root of an Eisenstein polynomial to a DVR gives a DVR · The maximal ideal of an Eisenstein extension of a DVR is generated by the root · An Eisenstein extension of a DVR is local

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.