The dyadic cyclotomic character in odd degree

This file shows that the local cyclotomic character of a finite odd-degree extension of ℚ₂ has full image in ℤ₂ˣ. The base case Φ₁ is linear, while for positive exponents the translated 2-power cyclotomic polynomial over ℤ₂ is Eisenstein.

The predicate IsDyadicOddCase packages the two numerical invariants used by the odd dyadic case of the local Galois-group classification. See Serre, Local Fields, Chapter IV, §4, for the cyclotomic extensions of local fields.

theorem TauCeti.range_localCyclotomicCharacter_of_odd_finrank (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (hodd : Odd (Module.finrank ℚ_[2] K)) : (localCyclotomicCharacter 2 K).range = ⊤

The local dyadic cyclotomic character of an odd-degree extension of ℚ₂ has full image.

def TauCeti.IsDyadicOddCase (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Prop

The numerical conditions defining the odd dyadic case: exactly two 2-power roots of unity, and odd degree over ℚ₂.

Equations

• TauCeti.IsDyadicOddCase K = (TauCeti.localRootOfUnityOrder 2 K ⋯ = 2 ∧ Odd (Module.finrank ℚ_[2] K))

theorem TauCeti.isDyadicOddCase_iff (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsDyadicOddCase K ↔ have x := ⋯; localRootOfUnityOrder 2 K ⋯ = 2 ∧ Odd (Module.finrank ℚ_[2] K)

Characterization of the numerical conditions in IsDyadicOddCase.

theorem TauCeti.IsDyadicOddCase.mk (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hroots : have x := ⋯; localRootOfUnityOrder 2 K ⋯ = 2) (hodd : Odd (Module.finrank ℚ_[2] K)) : IsDyadicOddCase K

Construct the odd dyadic case from its two numerical conditions.

theorem TauCeti.IsDyadicOddCase.localRootOfUnityOrder_eq_two (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hcase : IsDyadicOddCase K) : have x := ⋯; localRootOfUnityOrder 2 K ⋯ = 2

The odd dyadic case has exactly two 2-power roots of unity.

theorem TauCeti.IsDyadicOddCase.odd_finrank (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hcase : IsDyadicOddCase K) : Odd (Module.finrank ℚ_[2] K)

The degree over ℚ₂ in the odd dyadic case is odd.

theorem TauCeti.range_localCyclotomicCharacter_of_degree_odd (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [FiniteDimensional ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hcase : IsDyadicOddCase K) : (localCyclotomicCharacter 2 K).range = ⊤

In the odd dyadic case, the image of the local cyclotomic character is all of ℤ₂ˣ.