Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Even.UnitsPlusMinus

Labute's normal form for the dyadic Demushkin groups of even rank with image {±1} × U^(f) #

Let G be a Demushkin group at p = 2 of even rank n ≥ 4 whose canonical character has image V^(f) = {±1} × U^(f) for a finite f ≥ 2. Labute's Theorem 6 says that G is presented on n generators by the single relator x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), the normal-form word TauCeti.demushkinWordTwoEven 0 f n; in particular two such groups with the same rank and the same f are topologically isomorphic. This file proves that theorem, from the exact normal form of the dyadic relators of even rank (TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Even.Exact), the values of the canonical character forced by that normal form, the symplectic transvection pair TauCeti.freeProP.symplecticTransvection of TauCeti.Topology.Algebra.Group.Profinite.Free.ElementaryAutomorphism, which adjusts the character value at x₂, and the constrained successive approximation of TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Even.Approximation.

Main results #

References #

The symplectic transvection pair and the normal-form word #

source
theorem TauCeti.freeProP.gradedMap_symplecticTransvection_gradedMk_demushkinWordNeTwo {n p : ℕ} [Fact (Nat.Prime p)] (hn3 : 3 < n) (c : ℤ_[p]) {q : ℕ} (hq : p ∣ q) :
(gradedMap p (↑(symplecticTransvection hn3 c)).toMonoidHom ⋯ 1) (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩) = gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩

The symplectic transvection pair fixes the class of the normal-form word x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) in gr_1(F), for n ≥ 4 and p ∣ q.

The character values forced by the exact normal form #

source
theorem TauCeti.freeProP.apply_eq_of_forall_isCrossedHom_eq_zero_padicPow_mul_labuteComm_mul {n : ℕ} (hn : Even n) (hn3 : 3 < n) (χ : freeProP 2 (Fin n) →ₜ* ℤ_[2]ˣ) (α : ℤ_[2]) (q : ℕ) (hkill : ∀ (D : freeProP 2 (Fin n) → ℤ_[2]), Continuous D → IsCrossedHom (⇑χ) D → D (⋯.padicPow (freeProPGen 2 n 0) (2 + α) * labuteComm (freeProPGen 2 n 0) (freeProPGen 2 n 1) * demushkinWordNeTwo q (n - 2) fun (i : ℕ) => freeProPGen 2 n (i + 2)) = 0) :
(∀ (j : ℕ), j ≠ 1 → j ≠ 3 → χ (freeProPGen 2 n j) = 1) ∧ ↑(χ (freeProPGen 2 n 1)) * (1 + α) = -1 ∧ ↑(χ (freeProPGen 2 n 3)) * (1 - ↑q) = 1

The character values forced by the exact dyadic relator of even rank (Labute, Theorem 4, read on the exact normal form). Let n ≥ 4 be even and let χ be a continuous character of the free pro-2 group on n generators all of whose continuous crossed homomorphisms kill x₁^{2+α} (x₁, x₂) x₃^{q} (x₃, x₄) ⋯ (x_{n-1}, x_n), with α ∈ ℤ₂ and q : ℕ. Then χ(x₂) (1 + α) = -1, χ(x₄) (1 - q) = 1, and χ(x_i) = 1 for every other generator.

Labute's Theorem 6 #

source
theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordTwoEven_of_range_eq {n : ℕ} {r : freeProP 2 (Fin n)} (hr : r ∈ proPFrattini 2 (freeProP 2 (Fin n))) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})) (hn : Even n) (hn3 : 3 < n) {f : ℕ} (hf : 2 ≤ f) (hA : (demushkinCharacter hG).range = unitsPlusMinus f) :
∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), e r = demushkinWordTwoEven 0 f n (freeProPGen 2 n)

Labute's normal form for the dyadic Demushkin groups of even rank with image {±1} × U^(f) (Labute, Theorem 6). Let r ∈ Φ(F) be a relator of the free pro-2 group on an even number n ≥ 4 of generators presenting a Demushkin group G = ⟨x₁, …, x_n ∣ r⟩ whose canonical character has image V^(f) = {±1} × U^(f) for a finite f ≥ 2. Then a continuous automorphism of F carries r to x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n).

source
theorem TauCeti.freeProP.exists_continuousMulEquiv_presentedProP_demushkinWordTwoEven_of_range_eq {n : ℕ} {r : freeProP 2 (Fin n)} (hr : r ∈ proPFrattini 2 (freeProP 2 (Fin n))) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})) (hn : Even n) (hn3 : 3 < n) {f : ℕ} (hf : 2 ≤ f) (hA : (demushkinCharacter hG).range = unitsPlusMinus f) :
Nonempty (presentedProP 2 (Fin n) {r} ≃ₜ* presentedProP 2 (Fin n) {demushkinWordTwoEven 0 f n (freeProPGen 2 n)})

Labute's normal form for a one-relator dyadic Demushkin group of even rank with image {±1} × U^(f). Let r ∈ Φ(F) be a relator of the free pro-2 group on an even number n ≥ 4 of generators presenting a Demushkin group whose canonical character has image V^(f), f ≥ 2 finite. Then ⟨x₁, …, x_n ∣ r⟩ is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n)⟩.

source
theorem TauCeti.IsDemushkin.exists_continuousMulEquiv_presentedProP_demushkinWordTwoEven_of_range_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (hn : Even (demushkinRank hG)) (hn3 : 3 < demushkinRank hG) {f : ℕ} (hf : 2 ≤ f) (hA : (demushkinCharacter hG).range = unitsPlusMinus f) :
Nonempty (G ≃ₜ* presentedProP 2 (Fin (demushkinRank hG)) {demushkinWordTwoEven 0 f (demushkinRank hG) (freeProPGen 2 (demushkinRank hG))})

Labute's normal form for a dyadic Demushkin group of even rank with image {±1} × U^(f), intrinsic form (Labute, Theorem 6). A Demushkin group G at p = 2 of even rank n ≥ 4 whose canonical character has image V^(f) = {±1} × U^(f) for a finite f ≥ 2 is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n)⟩ on n = demushkinRank hG generators.

source
theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_of_even_demushkinRank_of_range_eq_unitsPlusMinus {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hG : IsDemushkin 2 G) (hH : IsDemushkin 2 H) (hn : demushkinRank hG = demushkinRank hH) (heven : Even (demushkinRank hG)) (hn3 : 3 < demushkinRank hG) {f : ℕ} (hf : 2 ≤ f) (hA : (demushkinCharacter hG).range = unitsPlusMinus f) (hB : (demushkinCharacter hH).range = unitsPlusMinus f) :
Nonempty (G ≃ₜ* H)

Uniqueness of the dyadic Demushkin groups of even rank with image {±1} × U^(f) (Labute, Theorem 6). Two Demushkin groups at p = 2 of the same even rank n ≥ 4 whose canonical characters have the same image V^(f) = {±1} × U^(f), f ≥ 2 finite, are topologically isomorphic.