Documentation

TauCeti.FieldTheory.FunctionField.Place.Extension.Eisenstein

Totally ramified places, and the Eisenstein criterion #

Let F' / k' be a finite extension of the field extension F / k. A place P' of F' / k' is totally ramified over F when its ramification index is as large as the fundamental inequality allows, e(P' ∣ P) = [F' : F]. The inequality then forces the rest of the picture: the relative degree is 1 and P' is the only place of F' lying over P, which is Stichtenoth's Definition 3.1.13 read at P.

The criterion that produces totally ramified places is Eisenstein's. Call φ ∈ F[X] Eisenstein at a place P of F / k when its leading coefficient is a unit of 𝒪_P, every coefficient below the leading one vanishes at P, and the constant coefficient vanishes to order exactly one — the three conditions of Mathlib's Polynomial.IsEisensteinAt at the maximal ideal of 𝒪_P, read off the order function so that a polynomial over F may be tested. If y generates F' over F and its minimal polynomial is Eisenstein at P, then every place P' of F' over P is totally ramified and y is a prime element at P'.

The proof is the Newton-polygon computation, run with the strict triangle inequality. Write n = deg φ, e = e(P' ∣ P) and m = ord_{P'} y, and expand 0 = φ(y) as the sum of its n + 1 terms. The term of index i < n has order at least e + i·m because its coefficient vanishes at P, the term of index 0 has order exactly e, and the leading term has order n·m. If any one of the terms had order strictly smaller than all the others, the strict triangle inequality would make the sum nonzero; so neither the leading term nor the constant term can dominate, and comparing the two possibilities gives n·m = e — first for m ≤ 0, where the leading term would dominate, and then for the two ways n·m and e could differ. Since e ≤ [F' : F] = n and m ≥ 1, this forces e = n and m = 1.

Main definitions #

Main results #

References #

source
def TauCeti.Place.IsTotallyRamified {k' : Type u'} (F : Type v) {F' : Type v'} [Field k'] [Field F] [Field F'] [Algebra k' F'] [Algebra F F'] (P' : Place k' F') :
Prop

A place P' of F' / k' is totally ramified over F when its ramification index is the full degree [F' : F]. By the fundamental inequality this is the largest value the ramification index can take, and it forces the relative degree to be 1 (TauCeti.Place.relativeDegree_eq_one_of_isTotallyRamified) and P' to be the only place of F' over the place of F below it (TauCeti.Place.eq_of_isTotallyRamified): the situation Stichtenoth's Definition 3.1.13 calls total ramification of that place of F.

Equations
Instances For
    source
    theorem TauCeti.Place.isTotallyRamified_iff {k' : Type u'} (F : Type v) {F' : Type v'} [Field k'] [Field F] [Field F'] [Algebra k' F'] [Algebra F F'] {P' : Place k' F'} :
    IsTotallyRamified F P' ↔ ramificationIdx F P' = Module.finrank F F'

    Total ramification unfolds to its defining equality of the ramification index with the degree.

    source
    @[simp]
    theorem TauCeti.Place.relativeDegree_eq_one_of_isTotallyRamified (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] {P' : Place k' F'} (h : IsTotallyRamified F P') :
    relativeDegree k F P' = 1

    A totally ramified place has relative degree one: the fundamental inequality has no room left for a residue field extension.

    source
    theorem TauCeti.Place.eq_of_isTotallyRamified (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] {P' Q' : Place k' F'} (h : IsTotallyRamified F P') (hQ : restrict k F Q' = restrict k F P') :
    Q' = P'

    A totally ramified place is the only place over the place below it: a second place in the fibre would contribute at least 1 more to the fundamental inequality.

    source
    @[simp]
    theorem TauCeti.Place.setOf_restrict_eq_eq_singleton_of_isTotallyRamified (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] {P' : Place k' F'} (h : IsTotallyRamified F P') :
    {Q' : Place k' F' | restrict k F Q' = restrict k F P'} = {P'}

    The fibre of TauCeti.Place.restrict over the place below a totally ramified place is a single point.

    source
    theorem TauCeti.Place.adjoin_eq_top_of_isTotallyRamified_of_ord_eq_one {k' : Type u'} (F : Type v) {F' : Type v'} [Field k'] [Field F] [Field F'] [Algebra k' F'] [Algebra F F'] [FiniteDimensional F F'] {P' : Place k' F'} {t : F'} (h : IsTotallyRamified F P') (ht : P'.ord t = 1) :
    F⟮t⟯ = ⊤

    A uniformizer at a totally ramified place generates the field extension. Its first e(P' | P) = [F' : F] powers are linearly independent, hence form a basis.

    source
    structure TauCeti.Place.IsEisensteinAt {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (φ : Polynomial F) :
    Prop

    A polynomial over F is Eisenstein at a place P of F / k when its leading coefficient is a unit of 𝒪_P, every coefficient below the leading one vanishes at P, and the constant coefficient vanishes to order exactly one. For a polynomial with coefficients in 𝒪_P these are the three conditions of Mathlib's Polynomial.IsEisensteinAt at the maximal ideal of 𝒪_P; see TauCeti.Place.isEisensteinAt_map. The conditions are stated through the valuation and the order function rather than through membership in the maximal ideal, so that a polynomial over F — for instance a minimal polynomial — may be tested directly; the junk value ord_P 0 = 0 is avoided by using the valuation in the condition that admits zero coefficients.

    • ord_leadingCoeff : P.ord φ.leadingCoeff = 0

      The leading coefficient is a unit of 𝒪_P; monic polynomials qualify.

    • valuation_coeff_lt_one (i : ℕ) : i < φ.natDegree → P.valuation (φ.coeff i) < 1

      Every coefficient below the leading one lies in the maximal ideal of 𝒪_P.

    • ord_coeff_zero : P.ord (φ.coeff 0) = 1

      The constant coefficient vanishes to order exactly one.

    Instances For
      source
      theorem TauCeti.Place.IsEisensteinAt.natDegree_pos {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {P : Place k F} {φ : Polynomial F} (h : P.IsEisensteinAt φ) :
      0 < φ.natDegree

      An Eisenstein polynomial has positive degree: in degree zero the leading coefficient is the constant coefficient, and the two order conditions contradict each other.

      source
      theorem TauCeti.Place.isEisensteinAt_map {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {ψ : Polynomial ↥P.integers} (hdeg : 0 < ψ.natDegree) (h : ψ.IsEisensteinAt (IsLocalRing.maximalIdeal ↥P.integers)) :
      P.IsEisensteinAt (Polynomial.map (algebraMap (↥P.integers) F) ψ)

      Mathlib's Eisenstein condition is this one: a polynomial over 𝒪_P of positive degree which is Eisenstein at the maximal ideal of 𝒪_P in the sense of Polynomial.IsEisensteinAt becomes, read in F[X], a polynomial Eisenstein at P. No monicity is needed: the Polynomial.IsEisensteinAt.leading field already puts the leading coefficient outside the maximal ideal, hence makes it a unit of 𝒪_P. The Polynomial.IsEisensteinAt.notMem field is what pins the order of the constant coefficient down to exactly one.

      source
      theorem TauCeti.Place.natDegree_mul_ord_eq_ramificationIdx (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] {P' : Place k' F'} [Algebra.IsIntegral F F'] {φ : Polynomial F} (hφ : (restrict k F P').IsEisensteinAt φ) {y : F'} (hy : (Polynomial.aeval y) φ = 0) :
      ↑φ.natDegree * P'.ord y = ↑(ramificationIdx F P')

      The order of a root of an Eisenstein polynomial (Stichtenoth, Proposition 3.1.15): if φ ∈ F[X] of degree n is Eisenstein at the place of F / k below P', then a root y ∈ F' of φ satisfies n · ord_{P'} y = e(P' ∣ P). In particular n divides the ramification index, which is the whole content of the criterion.

      source
      theorem TauCeti.Place.isTotallyRamified_of_isEisensteinAt (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] {P' : Place k' F'} [Algebra.IsIntegral F F'] [FiniteDimensional F F'] {y : F'} (htop : F⟮y⟯ = ⊤) (hφ : (restrict k F P').IsEisensteinAt (minpoly F y)) :
      IsTotallyRamified F P'

      The Eisenstein criterion (Stichtenoth, Proposition 3.1.15): if F' = F(y) and the minimal polynomial of y over F is Eisenstein at the place of F / k below P', then P' is totally ramified over F. Together with TauCeti.Place.setOf_restrict_eq_eq_singleton_of_isTotallyRamified this says that the place below P' is totally ramified in F' / F: it has exactly one extension, of ramification index [F' : F] and relative degree 1.

      source
      theorem TauCeti.Place.ord_eq_one_of_isEisensteinAt (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] {P' : Place k' F'} [Algebra.IsIntegral F F'] [FiniteDimensional F F'] {y : F'} (htop : F⟮y⟯ = ⊤) (hφ : (restrict k F P').IsEisensteinAt (minpoly F y)) :
      P'.ord y = 1

      A generator with an Eisenstein minimal polynomial is a prime element (Stichtenoth, Proposition 3.1.15).