The marked pro-2 Galois group of ℚ₂(√-2)

The field ℚ₂(√-2) has degree 2 over ℚ₂ and exactly two 2-power roots of unity, and the image of its cyclotomic character is the twisted subgroup U^[2] = closure⟨3⟩ of ℤ₂ˣ, which does not contain -1. So it lies in the even-degree principal branch of the dyadic marked classification, with k = 2, and

G_{ℚ₂(√-2)}(2) ≃ ⟨x₁, x₂, x₃, x₄ ∣ x₁⁶ (x₁, x₂) x₃⁸ (x₃, x₄)⟩,

under which the cyclotomic orientation satisfies χ(x₂) · (1 + 4) = -1 and χ(x₄) · (1 - 8) = 1 and is trivial on x₁ and x₃. This is TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_principal at N = 2, k = 2, α = 4, f = 3. In this branch the level f is not an invariant: the general theorem applies to every f > k, and f = 3 is the least choice.

This example separates the two even-degree branches: q = 2 and the rank 4 are those of the plus-minus branch as well, and only the image of the orientation, through -1 ∉ Im χ and the generator 3 = -1 + 2², selects the principal branch and its index k = 2.

The image is computed by Galois theory, without reciprocity. Every value of the character is 1 or 3 modulo 8, because √-2 = ξ + ξ³ for a primitive eighth root of unity ξ (TauCeti.toZModPow_three_localCyclotomicCharacter_eq_one_or_eq_three). This excludes -1 and every generator -1 + 2^k with k ≥ 3 from the image, so the classification of the closed subgroups of ℤ₂ˣ (TauCeti.exists_range_localCyclotomicCharacter_eq_topologicalClosure_zpowers) leaves closure⟨-1 + 2²⟩. The same congruence excludes a primitive fourth root of unity: it would put the image in 1 + 8ℤ₂, of index 4 in ℤ₂ˣ, while the image has index dividing the degree 2 (TauCeti.relIndex_range_localCyclotomicCharacter_dvd_finrank).

Main definitions

• TauCeti.RatPadicSqrtNegTwo: the local field ℚ₂(√-2), adjoining a root of X² + 2 to ℚ₂.
• TauCeti.RatPadicSqrtNegTwo.sqrtNegTwo: its distinguished square root of -2.

Main results

• TauCeti.finrank_ratPadicSqrtNegTwo: the degree is 2.
• TauCeti.localRootOfUnityOrder_two_ratPadicSqrtNegTwo: q(ℚ₂(√-2)) = 2.
• TauCeti.range_localCyclotomicCharacter_ratPadicSqrtNegTwo: the cyclotomic image is closure⟨-negThreeUnit⟩ = closure⟨3⟩.
• TauCeti.isDyadicEvenPrincipalCase_ratPadicSqrtNegTwo: ℚ₂(√-2) is in the even principal branch.
• TauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo_marked: the marked presentation of G_{ℚ₂(√-2)}(2), and its unmarked corollary TauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, Theorems 8 and 9.
• J.-P. Serre, Local Fields, Chapter IV, §4.

def TauCeti.RatPadicSqrtNegTwo : Type

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

theorem TauCeti.RatPadicSqrtNegTwo.instFactIrreduciblePolynomialPadicOfNatNatHAddHPowXCoeRingHomC : Fact (Irreducible (Polynomial.X ^ 2 + Polynomial.C 2))

X² + 2 is irreducible over ℚ₂: it is X² - (-2), and -2 is a uniformizer of ℤ₂.

@[instance_reducible]

noncomputable instance TauCeti.RatPadicSqrtNegTwo.instField : Field RatPadicSqrtNegTwo

@[instance_reducible]

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

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

theorem TauCeti.RatPadicSqrtNegTwo.instIsAlgebraicPadicOfNatNat : Algebra.IsAlgebraic ℚ_[2] RatPadicSqrtNegTwo

instance TauCeti.RatPadicSqrtNegTwo.instIsSeparablePadicOfNatNat : Algebra.IsSeparable ℚ_[2] RatPadicSqrtNegTwo

instance TauCeti.RatPadicSqrtNegTwo.instCharZero : CharZero RatPadicSqrtNegTwo

@[instance_reducible]

noncomputable instance TauCeti.RatPadicSqrtNegTwo.instValuativeRel : ValuativeRel RatPadicSqrtNegTwo

@[instance_reducible]

noncomputable instance TauCeti.RatPadicSqrtNegTwo.instTopologicalSpace : TopologicalSpace RatPadicSqrtNegTwo

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

instance TauCeti.RatPadicSqrtNegTwo.instIsNonarchimedeanLocalField : IsNonarchimedeanLocalField RatPadicSqrtNegTwo

noncomputable def TauCeti.RatPadicSqrtNegTwo.sqrtNegTwo : RatPadicSqrtNegTwo

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

@[simp]

theorem TauCeti.RatPadicSqrtNegTwo.sqrtNegTwo_sq : sqrtNegTwo ^ 2 = -2

The defining equation of the generator √-2.

@[simp]

theorem TauCeti.finrank_ratPadicSqrtNegTwo : Module.finrank ℚ_[2] RatPadicSqrtNegTwo = 2

The degree of ℚ₂(√-2)/ℚ₂ is 2, so N + 2 = 4.

theorem TauCeti.ratPadicSqrtNegTwo_hasPrimitiveRoot : ∃ (ζ : RatPadicSqrtNegTwo), IsPrimitiveRoot ζ 2

ℚ₂(√-2) contains the primitive square root of unity -1.

theorem TauCeti.not_exists_isPrimitiveRoot_four_ratPadicSqrtNegTwo : ¬∃ (ζ : RatPadicSqrtNegTwo), IsPrimitiveRoot ζ 4

ℚ₂(√-2) contains no primitive fourth root of unity. Otherwise every value of its cyclotomic character would be 1 modulo 4, hence 1 modulo 8, and the image would have index at least [ℤ₂ˣ : 1 + 8ℤ₂] = 4, while its index divides [ℚ₂(√-2) : ℚ₂] = 2.

theorem TauCeti.localRootOfUnityOrder_two_ratPadicSqrtNegTwo : localRootOfUnityOrder 2 RatPadicSqrtNegTwo ⋯ = 2

q(ℚ₂(√-2)) = 2: the only 2-power roots of unity of ℚ₂(√-2) are ±1.

theorem TauCeti.neg_one_notMem_range_localCyclotomicCharacter_ratPadicSqrtNegTwo : -1 ∉ (localCyclotomicCharacter 2 RatPadicSqrtNegTwo).range

-1 is not a value of the cyclotomic character of ℚ₂(√-2), since -1 ≡ 7 mod 8.

theorem TauCeti.range_localCyclotomicCharacter_ratPadicSqrtNegTwo : (localCyclotomicCharacter 2 RatPadicSqrtNegTwo).range = (Subgroup.zpowers (-negThreeUnit)).topologicalClosure

The cyclotomic image of ℚ₂(√-2) is U^[2] = closure⟨3⟩, the closed subgroup of ℤ₂ˣ topologically generated by -negThreeUnit = 3 = -1 + 2² (negThreeUnit_neg_coe). By the classification of closed subgroups it is closure⟨-1 + 2^k⟩ for some k ≥ 2, and k = 2 because -1 + 2^k ≡ 7 mod 8 for k ≥ 3, while every value of the character is 1 or 3 modulo 8.

theorem TauCeti.isDyadicEvenPrincipalCase_ratPadicSqrtNegTwo : IsDyadicEvenPrincipalCase RatPadicSqrtNegTwo

ℚ₂(√-2) lies in the even-degree principal branch: q = 2, the degree 2 is even, and -1 is not a value of the cyclotomic character.

theorem TauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo_marked : ∃ (e : absoluteGaloisGroupProP 2 RatPadicSqrtNegTwo ≃ₜ* presentedProP 2 (Fin 4) {demushkinWordTwoEven 4 3 4 (freeProPGen 2 4)}), ↑((cyclotomicOrientation 2 RatPadicSqrtNegTwo ratPadicSqrtNegTwo_hasPrimitiveRoot) (e.symm (presentedProPGen 2 4 {demushkinWordTwoEven 4 3 4 (freeProPGen 2 4)} 1))) * (1 + 4) = -1 ∧ ↑((cyclotomicOrientation 2 RatPadicSqrtNegTwo ratPadicSqrtNegTwo_hasPrimitiveRoot) (e.symm (presentedProPGen 2 4 {demushkinWordTwoEven 4 3 4 (freeProPGen 2 4)} 3))) * (1 - 8) = 1 ∧ (cyclotomicOrientation 2 RatPadicSqrtNegTwo ratPadicSqrtNegTwo_hasPrimitiveRoot) (e.symm (presentedProPGen 2 4 {demushkinWordTwoEven 4 3 4 (freeProPGen 2 4)} 0)) = 1 ∧ (cyclotomicOrientation 2 RatPadicSqrtNegTwo ratPadicSqrtNegTwo_hasPrimitiveRoot) (e.symm (presentedProPGen 2 4 {demushkinWordTwoEven 4 3 4 (freeProPGen 2 4)} 2)) = 1

The marked presentation of G_{ℚ₂(√-2)}(2). The maximal pro-2 Galois group of ℚ₂(√-2) is isomorphic to ⟨x₁, x₂, x₃, x₄ ∣ x₁⁶ (x₁, x₂) x₃⁸ (x₃, x₄)⟩, the even dyadic Demushkin group with α = 4 and f = 3, and under this isomorphism the cyclotomic orientation satisfies χ(x₂) · (1 + 4) = -1 and χ(x₄) · (1 - 8) = 1 and is trivial on x₁ and x₃.

This is absoluteGaloisGroupProP_two_marked_of_degree_even_principal at N = 2, with k = 2 read off the cyclotomic image closure⟨-1 + 2²⟩ (range_localCyclotomicCharacter_ratPadicSqrtNegTwo).

theorem TauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo : Nonempty (absoluteGaloisGroupProP 2 RatPadicSqrtNegTwo ≃ₜ* presentedProP 2 (Fin 4) {demushkinWordTwoEven 4 3 4 (freeProPGen 2 4)})

G_{ℚ₂(√-2)}(2) ≃ ⟨x₁, x₂, x₃, x₄ ∣ x₁⁶ (x₁, x₂) x₃⁸ (x₃, x₄)⟩, the unmarked form of absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo_marked.