Arithmetic cases for marked local Galois presentations

The marked classification of maximal pro-p local Galois groups separates the dyadic fields with exactly two 2-power roots of unity according to the parity of their degree and, in even degree, according to whether -1 belongs to the cyclotomic image. This file defines those arithmetic predicates and proves that every finite extension of ℚ₂ lies in exactly one of the four resulting cases. At an odd prime, it proves that exactly one of the free and nonexceptional Demushkin cases applies.

The partition is purely arithmetic: it does not assume a Demushkin presentation. It is the case split used when the abstract marked classification is applied to a local Galois group.

def TauCeti.IsFreeCase (p : ℕ) (K : Type u_1) [Field K] : Prop

The free arithmetic case: K does not contain a primitive p-th root of unity.

Equations

• TauCeti.IsFreeCase p K = ¬∃ (ζ : K), IsPrimitiveRoot ζ p

theorem TauCeti.isFreeCase_iff (p : ℕ) (K : Type u_1) [Field K] : IsFreeCase p K ↔ ¬∃ (ζ : K), IsPrimitiveRoot ζ p

Characterization of the free arithmetic case.

@[simp]

theorem TauCeti.not_isFreeCase_two {K : Type u_1} [Field K] [NeZero 2] : ¬IsFreeCase 2 K

A field in which 2 ≠ 0 (for example, any field of characteristic zero) is never in the free arithmetic case at p = 2, since -1 is a primitive square root of unity.

def TauCeti.IsQNeTwoCase (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Prop

The nonexceptional Demushkin case: K contains μ_p and its group of p-power roots of unity does not have order two.

Equations

• TauCeti.IsQNeTwoCase p K = ((∃ (ζ : K), IsPrimitiveRoot ζ p) ∧ TauCeti.localRootOfUnityOrder p K ⋯ ≠ 2)

theorem TauCeti.isQNeTwoCase_iff {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [Algebra ℚ_[p] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsQNeTwoCase p K ↔ have x := ⋯; (∃ (ζ : K), IsPrimitiveRoot ζ p) ∧ localRootOfUnityOrder p K ⋯ ≠ 2

Characterization of the nonexceptional Demushkin case.

theorem TauCeti.odd_isFreeCase_xor_isQNeTwoCase (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hp : p ≠ 2) : IsFreeCase p K ∧ ¬IsQNeTwoCase p K ∨ ¬IsFreeCase p K ∧ IsQNeTwoCase p K

At an odd prime, exactly one of the free and nonexceptional Demushkin arithmetic cases applies. The exceptional value q = 2 cannot occur because the local root-of-unity order is a power of p.

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

The even dyadic case in which the cyclotomic image contains -1.

Equations

• TauCeti.IsDyadicEvenPlusMinusCase K = (TauCeti.localRootOfUnityOrder 2 K ⋯ = 2 ∧ Even (Module.finrank ℚ_[2] K) ∧ -1 ∈ (TauCeti.localCyclotomicCharacter 2 K).range)

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

The even dyadic case in which the cyclotomic image does not contain -1.

Equations

• TauCeti.IsDyadicEvenPrincipalCase K = (TauCeti.localRootOfUnityOrder 2 K ⋯ = 2 ∧ Even (Module.finrank ℚ_[2] K) ∧ -1 ∉ (TauCeti.localCyclotomicCharacter 2 K).range)

inductive TauCeti.DyadicMarkedCase : Type

The four arithmetic branches of the dyadic marked classification.

• qNeTwo : DyadicMarkedCase
• odd : DyadicMarkedCase
• evenPlusMinus : DyadicMarkedCase
• evenPrincipal : DyadicMarkedCase

@[instance_reducible]

instance TauCeti.instDecidableEqDyadicMarkedCase : DecidableEq DyadicMarkedCase

Equations

• TauCeti.instDecidableEqDyadicMarkedCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

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

The arithmetic predicate represented by a dyadic marked case.

Equations

• TauCeti.DyadicMarkedCase.Holds K TauCeti.DyadicMarkedCase.qNeTwo = TauCeti.IsQNeTwoCase 2 K
• TauCeti.DyadicMarkedCase.Holds K TauCeti.DyadicMarkedCase.odd = TauCeti.IsDyadicOddCase K
• TauCeti.DyadicMarkedCase.Holds K TauCeti.DyadicMarkedCase.evenPlusMinus = TauCeti.IsDyadicEvenPlusMinusCase K
• TauCeti.DyadicMarkedCase.Holds K TauCeti.DyadicMarkedCase.evenPrincipal = TauCeti.IsDyadicEvenPrincipalCase K

@[simp]

theorem TauCeti.DyadicMarkedCase.holds_qNeTwo (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Holds K qNeTwo ↔ IsQNeTwoCase 2 K

@[simp]

theorem TauCeti.DyadicMarkedCase.holds_odd (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Holds K odd ↔ IsDyadicOddCase K

@[simp]

theorem TauCeti.DyadicMarkedCase.holds_evenPlusMinus (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Holds K evenPlusMinus ↔ IsDyadicEvenPlusMinusCase K

@[simp]

theorem TauCeti.DyadicMarkedCase.holds_evenPrincipal (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Holds K evenPrincipal ↔ IsDyadicEvenPrincipalCase K

theorem TauCeti.isDyadicEvenPlusMinusCase_iff {K : Type u_1} [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsDyadicEvenPlusMinusCase K ↔ have x := ⋯; localRootOfUnityOrder 2 K ⋯ = 2 ∧ Even (Module.finrank ℚ_[2] K) ∧ -1 ∈ (localCyclotomicCharacter 2 K).range

Characterization of the numerical and cyclotomic conditions in the even plus-minus case.

theorem TauCeti.isDyadicEvenPrincipalCase_iff {K : Type u_1} [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsDyadicEvenPrincipalCase K ↔ have x := ⋯; localRootOfUnityOrder 2 K ⋯ = 2 ∧ Even (Module.finrank ℚ_[2] K) ∧ -1 ∉ (localCyclotomicCharacter 2 K).range

Characterization of the numerical and cyclotomic conditions in the even principal case.

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

The even plus-minus case has exactly two 2-power roots of unity.

theorem TauCeti.IsDyadicEvenPlusMinusCase.even_finrank {K : Type u_1} [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hcase : IsDyadicEvenPlusMinusCase K) : Even (Module.finrank ℚ_[2] K)

The degree in the even plus-minus case is even.

theorem TauCeti.IsDyadicEvenPlusMinusCase.neg_one_mem_range {K : Type u_1} [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hcase : IsDyadicEvenPlusMinusCase K) : -1 ∈ (localCyclotomicCharacter 2 K).range

In the even plus-minus case, the cyclotomic image contains -1.

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

The even principal case has exactly two 2-power roots of unity.

theorem TauCeti.IsDyadicEvenPrincipalCase.even_finrank {K : Type u_1} [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hcase : IsDyadicEvenPrincipalCase K) : Even (Module.finrank ℚ_[2] K)

The degree in the even principal case is even.

theorem TauCeti.IsDyadicEvenPrincipalCase.neg_one_notMem_range {K : Type u_1} [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hcase : IsDyadicEvenPrincipalCase K) : -1 ∉ (localCyclotomicCharacter 2 K).range

In the even principal case, the cyclotomic image does not contain -1.

theorem TauCeti.dyadic_markedCase_exists_unique {K : Type u_1} [Field K] [Algebra ℚ_[2] K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ∃! c : DyadicMarkedCase, DyadicMarkedCase.Holds K c

Every finite extension of ℚ₂ belongs to exactly one arithmetic branch of the marked classification.