The dyadic cyclotomic image in the even-degree cases

For a finite extension K of ℚ₂ with exactly two 2-power roots of unity and even degree, the marked classification of G_K(2) has two branches, separated by whether -1 lies in the image of the cyclotomic character χ. This file computes that image in each branch, as one of Labute's closed subgroups of ℤ₂ˣ (closedSubgroup_units_two_classification):

• if -1 ∈ Im χ, then Im χ = V^(f) = {±1} × U^(f) for some f ≥ 2;
• if -1 ∉ Im χ and K contains no primitive fourth root of unity, then Im χ is the twisted subgroup U^[f] topologically generated by a unit u with u = -1 + 2 ^ f, f ≥ 2.

The image is closed since the absolute Galois group is compact. In the first branch it is not {±1} because it is infinite (infinite_range_localCyclotomicCharacter). In the second it is not contained in U^(2) = 1 + 4ℤ₂, since otherwise K would contain a primitive fourth root of unity (range_localCyclotomicCharacter_le_unitsPrincipal_iff). The exponent f is the parameter that the even marked normal forms take from the image.

Main results

• TauCeti.exists_range_localCyclotomicCharacter_eq_unitsPlusMinus: Im χ = V^(f) when -1 ∈ Im χ.
• TauCeti.exists_range_localCyclotomicCharacter_eq_topologicalClosure_zpowers: Im χ = U^[f] when -1 ∉ Im χ and μ₄ ⊄ K.
• TauCeti.range_localCyclotomicCharacter_of_degree_even_plusMinus, TauCeti.range_localCyclotomicCharacter_of_degree_even_principal: the same computations under the branch predicates IsDyadicEvenPlusMinusCase and IsDyadicEvenPrincipalCase.

References

• J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), §5.
• J.-P. Serre, Local Fields, Chapter IV, §4.

theorem TauCeti.exists_range_localCyclotomicCharacter_eq_unitsPlusMinus (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (hneg : -1 ∈ (localCyclotomicCharacter 2 K).range) : ∃ (f : ℕ), 2 ≤ f ∧ (localCyclotomicCharacter 2 K).range = unitsPlusMinus f

If -1 is a value of the cyclotomic character of a finite extension K of ℚ₂, its image is V^(f) = {±1} × U^(f) for some f ≥ 2.

theorem TauCeti.exists_range_localCyclotomicCharacter_eq_topologicalClosure_zpowers (K : Type u_1) [Field K] [NeZero 2] (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ 4) (hneg : -1 ∉ (localCyclotomicCharacter 2 K).range) : ∃ (f : ℕ) (u : ℤ_[2]ˣ), 2 ≤ f ∧ ↑u = -1 + 2 ^ f ∧ (localCyclotomicCharacter 2 K).range = (Subgroup.zpowers u).topologicalClosure

If K contains no primitive fourth root of unity and -1 is not a value of its cyclotomic character, the image of the character is the twisted subgroup U^[f], topologically generated by a unit u = -1 + 2 ^ f with f ≥ 2.

theorem TauCeti.range_localCyclotomicCharacter_of_degree_even_plusMinus (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [FiniteDimensional ℚ_[2] K] (hcase : IsDyadicEvenPlusMinusCase K) : ∃ (f : ℕ), 2 ≤ f ∧ (localCyclotomicCharacter 2 K).range = unitsPlusMinus f

The cyclotomic image in the even plus-minus branch is V^(f) = {±1} × U^(f) for some f ≥ 2.

theorem TauCeti.range_localCyclotomicCharacter_of_degree_even_principal (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hcase : IsDyadicEvenPrincipalCase K) : ∃ (f : ℕ) (u : ℤ_[2]ˣ), 2 ≤ f ∧ ↑u = -1 + 2 ^ f ∧ (localCyclotomicCharacter 2 K).range = (Subgroup.zpowers u).topologicalClosure

The cyclotomic image in the even principal branch is the twisted subgroup U^[f], topologically generated by a unit u = -1 + 2 ^ f with f ≥ 2.