Ramification of ℚ₂(√2)

Adjoining a root of X² - 2 gives a totally ramified quadratic extension of ℚ₂. Its root is a uniformizer, its residue field has two elements, and its different and discriminant exponents are both three. The nonidentity automorphism sends √2 to -√2, so its displacement at the integral generator has valuation three. Consequently the lower ramification groups are the whole Galois group through index two and trivial from index three.

This explicit filtration is useful for comparing lower numbering in the dyadic cyclotomic extension with its quadratic subextension: the third lower group of ℚ₂(√2)/ℚ₂ is trivial.

Main definitions

• TauCeti.DyadicSqrtTwo: the local field ℚ₂(√2).
• TauCeti.DyadicSqrtTwo.sqrtTwo: its distinguished square root of two.
• TauCeti.DyadicSqrtTwo.integerSqrtTwo: the same generator in its ring of integers.

Main results

• TauCeti.DyadicSqrtTwo.sqrtTwo_sq and TauCeti.DyadicSqrtTwo.minpoly_sqrtTwo: the generator equation and minimal polynomial.
• TauCeti.DyadicSqrtTwo.adjoin_sqrtTwo_eq_top and TauCeti.DyadicSqrtTwo.adjoin_integerSqrtTwo_eq_top: field and integral generation.
• TauCeti.DyadicSqrtTwo.irreducible_integerSqrtTwo: the generator is a uniformizer.
• TauCeti.DyadicSqrtTwo.isEisensteinAt_X_sq_sub_two and TauCeti.DyadicSqrtTwo.isRoot_integerSqrtTwo: the Eisenstein polynomial and its integral root.
• TauCeti.DyadicSqrtTwo.finrank_eq_two, TauCeti.DyadicSqrtTwo.ramificationIndex_eq_two, TauCeti.DyadicSqrtTwo.absoluteRamificationIndex_eq_two, TauCeti.DyadicSqrtTwo.dyadicLevel_eq_two, TauCeti.DyadicSqrtTwo.inertiaDegree_eq_one, and TauCeti.DyadicSqrtTwo.natCard_residueField: the degree, ramification, and residue invariants.
• TauCeti.DyadicSqrtTwo.isTotallyRamified and TauCeti.DyadicSqrtTwo.not_isUnramified: the ramification predicates.
• TauCeti.DyadicSqrtTwo.apply_sqrtTwo_of_ne_one, TauCeti.DyadicSqrtTwo.addVal_smul_sub_integerSqrtTwo_of_ne_one, and TauCeti.DyadicSqrtTwo.lowerIndex_of_ne_one: the nonidentity automorphism and its lower index.
• TauCeti.DyadicSqrtTwo.lowerRamificationGroup_eq: the complete lower filtration.
• TauCeti.DyadicSqrtTwo.differentExponent_eq_three and TauCeti.DyadicSqrtTwo.discriminantExponent_eq_three: both exponents are three.

References

• J.-P. Serre, Local Fields, Chapter III, §6 and Chapter IV, §1.

Formal sources

The construction is adapted from TauCeti.NumberTheory.LocalField.WorkedExamples.DyadicSqrt.Five.Basic and TauCeti.NumberTheory.LocalField.WorkedExamples.NonGaloisCubic.

def TauCeti.DyadicSqrtTwo : Type

The local field ℚ₂(√2), obtained by adjoining a root of X² - 2 to ℚ₂.

theorem TauCeti.DyadicSqrtTwo.instFactIrreduciblePolynomialPadicOfNatNatHSubHPowXCoeRingHomC : Fact (Irreducible (Polynomial.X ^ 2 - Polynomial.C 2))

@[instance_reducible]

noncomputable instance TauCeti.DyadicSqrtTwo.instField : Field DyadicSqrtTwo

@[instance_reducible]

noncomputable instance TauCeti.DyadicSqrtTwo.instAlgebraPadicOfNatNat : Algebra ℚ_[2] DyadicSqrtTwo

instance TauCeti.DyadicSqrtTwo.instFiniteDimensionalPadicOfNatNat : FiniteDimensional ℚ_[2] DyadicSqrtTwo

instance TauCeti.DyadicSqrtTwo.instCharZero : CharZero DyadicSqrtTwo

@[instance_reducible]

noncomputable instance TauCeti.DyadicSqrtTwo.instValuativeRel : ValuativeRel DyadicSqrtTwo

@[instance_reducible]

noncomputable instance TauCeti.DyadicSqrtTwo.instTopologicalSpace : TopologicalSpace DyadicSqrtTwo

instance TauCeti.DyadicSqrtTwo.instValuativeExtensionPadicOfNatNat : ValuativeExtension ℚ_[2] DyadicSqrtTwo

instance TauCeti.DyadicSqrtTwo.instIsNonarchimedeanLocalField : IsNonarchimedeanLocalField DyadicSqrtTwo

noncomputable def TauCeti.DyadicSqrtTwo.sqrtTwo : DyadicSqrtTwo

The square root √2 generating ℚ₂(√2), the class of X.

@[simp]

theorem TauCeti.DyadicSqrtTwo.sqrtTwo_sq : sqrtTwo ^ 2 = 2

The defining equation of the generator √2.

@[simp]

theorem TauCeti.DyadicSqrtTwo.minpoly_sqrtTwo : minpoly ℚ_[2] sqrtTwo = Polynomial.X ^ 2 - Polynomial.C 2

The minimal polynomial of √2 over ℚ₂ is X² - 2.

theorem TauCeti.DyadicSqrtTwo.adjoin_sqrtTwo_eq_top : ℚ_[2]⟮sqrtTwo⟯ = ⊤

√2 generates ℚ₂(√2) as a field extension of ℚ₂.

@[simp]

theorem TauCeti.DyadicSqrtTwo.finrank_eq_two : Module.finrank ℚ_[2] DyadicSqrtTwo = 2

The degree of ℚ₂(√2)/ℚ₂ is two.

instance TauCeti.DyadicSqrtTwo.instIsQuadraticExtensionPadicOfNatNat : Algebra.IsQuadraticExtension ℚ_[2] DyadicSqrtTwo

noncomputable def TauCeti.DyadicSqrtTwo.integerSqrtTwo : ↥(ValuativeRel.valuation DyadicSqrtTwo).integer

√2, viewed as an element of the ring of integers.

@[simp]

theorem TauCeti.DyadicSqrtTwo.coe_integerSqrtTwo : ↑integerSqrtTwo = sqrtTwo

@[simp]

theorem TauCeti.DyadicSqrtTwo.coe_ofNat_two : ↑2 = 2

The integer-ring inclusion sends 2 to 2 in ℚ₂(√2).

theorem TauCeti.DyadicSqrtTwo.isRoot_integerSqrtTwo : (Polynomial.map (algebraMap ↥(ValuativeRel.valuation ℚ_[2]).integer ↥(ValuativeRel.valuation DyadicSqrtTwo).integer) (Polynomial.X ^ 2 - Polynomial.C 2)).IsRoot integerSqrtTwo

The integer generator √2 is a root of X² - 2 over 𝒪[ℚ₂].

theorem TauCeti.DyadicSqrtTwo.isEisensteinAt_X_sq_sub_two : (Polynomial.X ^ 2 - Polynomial.C 2).IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation ℚ_[2]).integer)

The polynomial X² - 2 is Eisenstein over the integer ring of ℚ₂.

theorem TauCeti.DyadicSqrtTwo.irreducible_integerSqrtTwo : Irreducible integerSqrtTwo

√2 is a uniformizer of the integer ring of ℚ₂(√2).

@[simp]

theorem TauCeti.DyadicSqrtTwo.ramificationIndex_eq_two : ramificationIndex ℚ_[2] DyadicSqrtTwo = 2

The ramification index of ℚ₂(√2)/ℚ₂ is two.

@[simp]

theorem TauCeti.DyadicSqrtTwo.absoluteRamificationIndex_eq_two : absoluteRamificationIndex DyadicSqrtTwo 2 = 2

The absolute ramification index of ℚ₂(√2) is two.

theorem TauCeti.DyadicSqrtTwo.dyadicLevel_eq_two (h2 : 2 ≠ 0) : dyadicLevel DyadicSqrtTwo h2 = 2

The normalized valuation v_K(2) of 2 in K = ℚ₂(√2) is the absolute ramification index 2.

@[simp]

theorem TauCeti.DyadicSqrtTwo.inertiaDegree_eq_one : inertiaDegree ℚ_[2] DyadicSqrtTwo = 1

The residue degree of ℚ₂(√2)/ℚ₂ is one.

theorem TauCeti.DyadicSqrtTwo.isTotallyRamified : IsTotallyRamified ℚ_[2] DyadicSqrtTwo

ℚ₂(√2)/ℚ₂ is totally ramified.

@[simp]

theorem TauCeti.DyadicSqrtTwo.natCard_residueField : Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation DyadicSqrtTwo).integer) = 2

The residue field of ℚ₂(√2) has two elements.

theorem TauCeti.DyadicSqrtTwo.not_isUnramified : ¬IsUnramified ℚ_[2] DyadicSqrtTwo

The extension ℚ₂(√2)/ℚ₂ is ramified.

theorem TauCeti.DyadicSqrtTwo.adjoin_integerSqrtTwo_eq_top : (↥(ValuativeRel.valuation ℚ_[2]).integer)[integerSqrtTwo] = ⊤

The ring of integers is 𝒪[ℚ₂][√2].

@[simp]

theorem TauCeti.DyadicSqrtTwo.apply_sqrtTwo_of_ne_one {σ : Gal(DyadicSqrtTwo/ℚ_[2])} (hσ : σ ≠ 1) : σ sqrtTwo = -sqrtTwo

Every nonidentity automorphism sends √2 to -√2.

@[simp]

theorem TauCeti.DyadicSqrtTwo.addVal_smul_sub_integerSqrtTwo_of_ne_one {σ : Gal(DyadicSqrtTwo/ℚ_[2])} (hσ : σ ≠ 1) : (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation DyadicSqrtTwo).integer) (σ • integerSqrtTwo - integerSqrtTwo) = 3

The displacement of any nonidentity automorphism at the integral generator has valuation three: v(-√2 - √2) = v(2) + v(√2) = 2 + 1.

@[simp]

theorem TauCeti.DyadicSqrtTwo.lowerIndex_of_ne_one {σ : Gal(DyadicSqrtTwo/ℚ_[2])} (hσ : σ ≠ 1) : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation DyadicSqrtTwo).integer) σ = 3

Every nonidentity automorphism has lower index three.

@[simp]

theorem TauCeti.DyadicSqrtTwo.lowerRamificationGroup_eq (i : ℤ) : LocalFieldsRamification.lowerRamificationGroup ℚ_[2] DyadicSqrtTwo i = if i ≤ 2 then ⊤ else ⊥

The lower ramification groups are the whole Galois group through index two and trivial from index three, including the negative-index convention.

@[simp]

theorem TauCeti.DyadicSqrtTwo.differentExponent_eq_three : differentExponent ℚ_[2] DyadicSqrtTwo = 3

The different exponent of ℚ₂(√2)/ℚ₂ is three.

@[simp]

theorem TauCeti.DyadicSqrtTwo.discriminantExponent_eq_three : discriminantExponent ℚ_[2] DyadicSqrtTwo = 3

The local discriminant exponent of ℚ₂(√2)/ℚ₂ is three.