Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.QInvariant

The q-invariant of the Demushkin normal forms #

Labute's classification puts a Demushkin group of rank n with q-invariant q in one of three normal forms, presented on x₁, …, xₙ by the relator words

This file checks that the parameter q of a normal form is the q-invariant of the group it presents: whenever such a presented group is a Demushkin group, TauCeti.demushkinQ of it is q for the first word (p^{v_p(q)} in general, so q itself for q = 0 or q a positive power of p), and 2 for the dyadic words. The computation goes through the one-relator abelianization structure theorem TauCeti.presentedProP.oneRelatorAbelianizationEquiv, in the form TauCeti.demushkinQ_presentedProP_eq_pow_valuation: the exponent vector of the first word is q e₁, that of the second is 2 e₁ + 2^f e₂ = 2 (e₁ + 2^{f-1} e₂), or 2 e₁ at level f = ∞, and that of the third is (2 + a) e₁ + 2^f e₃ = (2 + a)(e₁ + c e₃) with 2 + a = 2u for the unit u = 1 + a/2 of ℤ₂, so the abelianizations are ℤ_p^{n-1} × ℤ_p ⧸ (q), ℤ₂^{n-1} × ℤ/2 and ℤ₂^{n-1} × ℤ/2. The hypothesis 4 ∣ a in the third word is Labute's normalisation α ∈ 4ℤ₂, and it is what makes 1 + a/2 a unit: for a ≡ 2 mod 4 and f ≥ 2 the whole exponent vector is divisible by 4, so the q-invariant would be at least 4. (For f = 1 the coordinate 2 at x₃ alone gives q-invariant 2, whatever a is.)

Main results #

References #

Exponent vectors of the normal-form words #

source
theorem TauCeti.freeProP.toAdd_exponentSum_demushkinWordNeTwo (p : ℕ) [Fact (Nat.Prime p)] {n : ℕ} (q : ℕ) :
Multiplicative.toAdd ((exponentSum p (Fin n)) (demushkinWordNeTwo q n (freeProPGen p n))) = ↑q • Multiplicative.toAdd ((exponentSum p (Fin n)) (freeProPGen p n 0))

The exponent vector of the q ≠ 2 word x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) on the free generators is q e₁.

source
theorem TauCeti.freeProP.toAdd_exponentSum_demushkinWordTwoOdd (p : ℕ) [Fact (Nat.Prime p)] {n : ℕ} (f : ℕ) :
Multiplicative.toAdd ((exponentSum p (Fin n)) (demushkinWordTwoOdd f n (freeProPGen p n))) = 2 • Multiplicative.toAdd ((exponentSum p (Fin n)) (freeProPGen p n 0)) + 2 ^ f • Multiplicative.toAdd ((exponentSum p (Fin n)) (freeProPGen p n 1))

The exponent vector of the q = 2, n odd word x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) on the free generators is 2 e₁ + 2^f e₂.

source
theorem TauCeti.freeProP.toAdd_exponentSum_demushkinWordTwoOddTop (p : ℕ) [Fact (Nat.Prime p)] {n : ℕ} :
Multiplicative.toAdd ((exponentSum p (Fin n)) (demushkinWordTwoOddTop n (freeProPGen p n))) = 2 • Multiplicative.toAdd ((exponentSum p (Fin n)) (freeProPGen p n 0))

The exponent vector of the q = 2, n odd word at level f = ∞, x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n), on the free generators is 2 e₁.

source
theorem TauCeti.freeProP.toAdd_exponentSum_demushkinWordTwoEven (p : ℕ) [Fact (Nat.Prime p)] {n : ℕ} (a f : ℕ) :
Multiplicative.toAdd ((exponentSum p (Fin n)) (demushkinWordTwoEven a f n (freeProPGen p n))) = (2 + ↑a) • Multiplicative.toAdd ((exponentSum p (Fin n)) (freeProPGen p n 0)) + 2 ^ f • Multiplicative.toAdd ((exponentSum p (Fin n)) (freeProPGen p n 2))

The exponent vector of the q = 2, n even word x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) on the free generators is (2 + a) e₁ + 2^f e₃.

The q-invariant of the normal forms #

source
theorem TauCeti.demushkinQ_presentedProP_demushkinWordNeTwo_eq_zero_iff {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} (hq : p ∣ q) (hG : IsDemushkin p (presentedProP p (Fin n) {demushkinWordNeTwo q n (freeProPGen p n)})) :
demushkinQ hG = 0 ↔ q = 0

The q-invariant of the q ≠ 2 normal form vanishes exactly when q = 0: for p ∣ q, if ⟨x₁, …, xₙ ∣ x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n)⟩ is a Demushkin group, its q-invariant is 0 if and only if q = 0.

source
@[simp]
theorem TauCeti.demushkinQ_presentedProP_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} (hq : p ∣ q) (hq0 : q ≠ 0) (hG : IsDemushkin p (presentedProP p (Fin n) {demushkinWordNeTwo q n (freeProPGen p n)})) :
demushkinQ hG = p ^ padicValNat p q

The q-invariant of the q ≠ 2 normal form is p^{v_p(q)}: for p ∣ q and q ≠ 0, if ⟨x₁, …, xₙ ∣ x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n)⟩ is a Demushkin group, its q-invariant is p ^ padicValNat p q.

source
theorem TauCeti.demushkinQ_presentedProP_demushkinWordNeTwo_of_eq_pow {p : ℕ} [Fact (Nat.Prime p)] {n q f : ℕ} (hq : q = p ^ f) (hf : 0 < f) (hG : IsDemushkin p (presentedProP p (Fin n) {demushkinWordNeTwo q n (freeProPGen p n)})) :
demushkinQ hG = q

The q ≠ 2 normal form with parameter q = p^f, f ≥ 1, has q-invariant q: if ⟨x₁, …, xₙ ∣ x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n)⟩ is a Demushkin group, its q-invariant is q.

source
@[simp]
theorem TauCeti.demushkinQ_presentedProP_demushkinWordTwoOdd {n f : ℕ} (hf : 0 < f) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {demushkinWordTwoOdd f n (freeProPGen 2 n)})) :
demushkinQ hG = 2

The q = 2, n odd normal form has q-invariant 2: for f ≥ 1, if ⟨x₁, …, xₙ ∣ x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n)⟩ is a Demushkin group, its q-invariant is 2.

source
@[simp]
theorem TauCeti.demushkinQ_presentedProP_demushkinWordTwoOddTop {n : ℕ} (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {demushkinWordTwoOddTop n (freeProPGen 2 n)})) :
demushkinQ hG = 2

The q = 2, n odd normal form at level f = ∞ has q-invariant 2: if ⟨x₁, …, xₙ ∣ x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n)⟩ is a Demushkin group, its q-invariant is 2.

source
@[simp]
theorem TauCeti.demushkinQ_presentedProP_demushkinWordTwoEven {n f a : ℕ} (ha : 4 ∣ a) (hf : 0 < f) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {demushkinWordTwoEven a f n (freeProPGen 2 n)})) :
demushkinQ hG = 2

The q = 2, n even normal form has q-invariant 2: for 4 ∣ a and f ≥ 1, if ⟨x₁, …, xₙ ∣ x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n)⟩ is a Demushkin group, its q-invariant is 2. The hypothesis 4 ∣ a makes 2 + a exactly divisible by 2.