Ramification of the dyadic eighth-root cyclotomic extension

The local field ℚ₂(ζ₈) is totally ramified of degree four, and ζ₈ - 1 generates its integer ring and is a uniformizer. The lower index of an automorphism is two when its cyclotomic exponent is three or seven, and four when that exponent is five. Thus the lower ramification groups are the whole group through index one, the subgroup generated by ζ₈ ↦ -ζ₈ at indices two and three, and trivial from index four.

Hilbert's formula then gives different and discriminant exponents equal to eight.

These computations supply the cyclotomic side of the comparison of lower numbering with the quadratic subextension ℚ₂(√2).

References

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

The local-field construction follows the other modules in TauCeti.NumberTheory.LocalField.WorkedExamples. The norm computations reuse Mathlib's IsPrimitiveRoot.norm_sub_one_two and norm_pow_sub_one_of_prime_pow_ne_two.

@[reducible, inline]

abbrev TauCeti.DyadicCyclotomicEight : Type

The dyadic cyclotomic field generated by a primitive eighth root of unity.

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

instance TauCeti.DyadicCyclotomicEight.instIsGaloisPadicOfNatNat : IsGalois ℚ_[2] DyadicCyclotomicEight

@[instance_reducible]

noncomputable instance TauCeti.DyadicCyclotomicEight.instValuativeRel : ValuativeRel DyadicCyclotomicEight

@[instance_reducible]

noncomputable instance TauCeti.DyadicCyclotomicEight.instTopologicalSpace : TopologicalSpace DyadicCyclotomicEight

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

instance TauCeti.DyadicCyclotomicEight.instIsNonarchimedeanLocalField : IsNonarchimedeanLocalField DyadicCyclotomicEight

noncomputable def TauCeti.DyadicCyclotomicEight.zetaEight : DyadicCyclotomicEight

A distinguished primitive eighth root of unity.

theorem TauCeti.DyadicCyclotomicEight.zetaEight_def : zetaEight = IsCyclotomicExtension.zeta 8 ℚ_[2] DyadicCyclotomicEight

Identify the distinguished root with Mathlib's cyclotomic generator.

theorem TauCeti.DyadicCyclotomicEight.isPrimitiveRoot_zetaEight : IsPrimitiveRoot zetaEight 8

The distinguished root has order eight.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.finrank_eq_four : Module.finrank ℚ_[2] DyadicCyclotomicEight = 4

The degree of the eighth-root cyclotomic extension is four.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.zetaEight_pow_four : zetaEight ^ 4 = -1

The fourth power of the distinguished root is minus one.

noncomputable def TauCeti.DyadicCyclotomicEight.integerZetaEight : ↥(ValuativeRel.valuation DyadicCyclotomicEight).integer

The distinguished root as an integer of the cyclotomic field.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.coe_integerZetaEight : ↑integerZetaEight = zetaEight

@[simp]

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

The residue degree of ℚ₂(ζ₈)/ℚ₂ is one.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.ramificationIndex_eq_four : ramificationIndex ℚ_[2] DyadicCyclotomicEight = 4

The ramification index of ℚ₂(ζ₈)/ℚ₂ is four.

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

The cyclotomic extension is totally ramified.

theorem TauCeti.DyadicCyclotomicEight.irreducible_integerZetaEight_sub_one : Irreducible (integerZetaEight - 1)

ζ₈ - 1 is a uniformizer in the cyclotomic integer ring.

theorem TauCeti.DyadicCyclotomicEight.adjoin_integerZetaEight_sub_one_eq_top : (↥(ValuativeRel.valuation ℚ_[2]).integer)[integerZetaEight - 1] = ⊤

The ring of integers is generated by ζ₈ - 1 over the integers of ℚ₂.

theorem TauCeti.DyadicCyclotomicEight.lowerIndex_eq (σ : Gal(DyadicCyclotomicEight/ℚ_[2])) : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation DyadicCyclotomicEight).integer) σ = if σ = 1 then ⊤ else if σ zetaEight = -zetaEight then 4 else 2

The lower index is infinite at the identity, four at ζ₈ ↦ -ζ₈, and two at each of ζ₈ ↦ ζ₈³ and ζ₈ ↦ ζ₈⁷.

noncomputable def TauCeti.DyadicCyclotomicEight.sigmaFive : Gal(DyadicCyclotomicEight/ℚ_[2])

The automorphism with cyclotomic exponent five, sending ζ₈ to -ζ₈.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.sigmaFive_zetaEight : sigmaFive zetaEight = -zetaEight

The exponent-five automorphism negates the distinguished root.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.orderOf_sigmaFive : orderOf sigmaFive = 2

The exponent-five automorphism has order two.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.lowerRamificationGroup_eq (i : ℤ) : LocalFieldsRamification.lowerRamificationGroup ℚ_[2] DyadicCyclotomicEight i = if i ≤ 1 then ⊤ else if i ≤ 3 then Subgroup.zpowers sigmaFive else ⊥

The complete lower filtration: the whole group through index one, the exponent-five subgroup at indices two and three, and the trivial group from index four.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.lowerRamificationGroupReal_eq (u : ℝ) : LocalFieldsRamification.lowerRamificationGroupReal ℚ_[2] DyadicCyclotomicEight u = if u ≤ 1 then ⊤ else if u ≤ 3 then Subgroup.zpowers sigmaFive else ⊥

The real lower filtration is constant on (-∞, 1], (1, 3], and (3, ∞).

@[simp]

theorem TauCeti.DyadicCyclotomicEight.differentExponent_eq_eight : differentExponent ℚ_[2] DyadicCyclotomicEight = 8

The different exponent of ℚ₂(ζ₈)/ℚ₂ is eight.

@[simp]

theorem TauCeti.DyadicCyclotomicEight.discriminantExponent_eq_eight : discriminantExponent ℚ_[2] DyadicCyclotomicEight = 8

The local discriminant exponent of ℚ₂(ζ₈)/ℚ₂ is eight.