Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Odd.Image

The orientation image pins the odd dyadic normal form #

Labute's normal form for a Demushkin group G at p = 2 of odd rank n says that G is presented on n generators by x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n), the level f = ∞, or by x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) for some finite level f ≥ 2 (TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Odd.Exact). The level is not a free parameter: the canonical character of the presented group at level f has image {±1} × U^(f), at level f = ∞ it has image {±1}, and these closed subgroups of ℤ₂ˣ are pairwise distinct (TauCeti.unitsPlusMinus_inj, TauCeti.unitsPlusMinus_ne_zpowers_neg_one). Since the image of the canonical character is an isomorphism invariant, the image of G determines the level of its normal form. This file draws the two consequences.

First, the image pins the normal form: a Demushkin group of odd rank n whose canonical character has image {±1} × U^(f) is presented by the level-f word, and one whose canonical character has image {±1} is presented by the level-∞ word; in relator form, an automorphism of the free pro-2 group carries any relator in Φ(F) with that image to that word. The finite-level statements carry the hypothesis 3 ≤ n, because at rank one the image is {±1} whatever the level, the word x₁² x₂^{2^f} reading x₁² when the second generator is out of range.

Second, the necessity half of the existence theorem for odd rank (Labute, Theorem 1 with Remark 2; Serre, Theorem 3.2): the image of the canonical character of a Demushkin group of odd rank is {±1}, or the rank is at least 3 and the image is {±1} × U^(f) for some f ≥ 2. With the realization half of TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Existence, the existence theorem for odd rank becomes an equivalence: a subgroup A ≤ ℤ₂ˣ is the image of the canonical character of a Demushkin group of odd rank n exactly when A = {±1}, or n ≥ 3 and A = {±1} × U^(f) for some f ≥ 2. The uniqueness and marked forms of the odd-rank classification are drawn from the pinned normal form in TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Uniqueness and TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Marked.

Main results #

References #

source
theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_presentedProP_demushkinWordTwoOddTop_of_range_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (hn : Odd (demushkinRank hG)) (hrange : (demushkinCharacter hG).range = Subgroup.zpowers (-1)) :
Nonempty (G ≃ₜ* presentedProP 2 (Fin (demushkinRank hG)) {demushkinWordTwoOddTop (demushkinRank hG) (freeProPGen 2 (demushkinRank hG))})

The image {±1} pins the odd normal form at level f = ∞. A Demushkin group at p = 2 of odd rank n whose canonical character has image {±1} is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n)⟩; at rank one this is ℤ/2 = ⟨x₁ ∣ x₁²⟩.

source
theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_presentedProP_demushkinWordTwoOdd_of_range_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (hn : Odd (demushkinRank hG)) (hn₃ : 3 ≤ demushkinRank hG) {f : ℕ} (hf : 2 ≤ f) (hrange : (demushkinCharacter hG).range = unitsPlusMinus f) :
Nonempty (G ≃ₜ* presentedProP 2 (Fin (demushkinRank hG)) {demushkinWordTwoOdd f (demushkinRank hG) (freeProPGen 2 (demushkinRank hG))})

The image {±1} × U^(f) pins the odd normal form at level f. A Demushkin group at p = 2 of odd rank n ≥ 3 whose canonical character has image {±1} × U^(f), with f ≥ 2, is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n)⟩.

source
theorem TauCeti.IsDemushkin.range_demushkinCharacter_eq_zpowers_neg_one_or_unitsPlusMinus_of_odd_demushkinRank {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (hn : Odd (demushkinRank hG)) :
(demushkinCharacter hG).range = Subgroup.zpowers (-1) ∨ 3 ≤ demushkinRank hG ∧ ∃ (f : ℕ), 2 ≤ f ∧ (demushkinCharacter hG).range = unitsPlusMinus f

The necessity half of the existence theorem for odd rank (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). The image of the canonical character of a Demushkin group of odd rank is {±1}, or the rank is at least 3 and the image is {±1} × U^(f) for some f ≥ 2.

source
theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordTwoOdd_of_range_eq {n : ℕ} (hn : Odd n) (hn₃ : 3 ≤ n) {r : freeProP 2 (Fin n)} (hr : r ∈ proPFrattini 2 (freeProP 2 (Fin n))) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})) {f : ℕ} (hf : 2 ≤ f) (hrange : (demushkinCharacter hG).range = unitsPlusMinus f) :
∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), e r = demushkinWordTwoOdd f n (freeProPGen 2 n)

The image {±1} × U^(f) pins the odd normal form at level f, relator form. Let r ∈ Φ(F) be a relator of the free pro-2 group on an odd number n ≥ 3 of generators presenting a Demushkin group whose canonical character has image {±1} × U^(f), with f ≥ 2. Then a continuous automorphism of F carries r to x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n).

source
theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordTwoOddTop_of_range_eq {n : ℕ} (hn : Odd n) {r : freeProP 2 (Fin n)} (hr : r ∈ proPFrattini 2 (freeProP 2 (Fin n))) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})) (hrange : (demushkinCharacter hG).range = Subgroup.zpowers (-1)) :
∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), e r = demushkinWordTwoOddTop n (freeProPGen 2 n)

The image {±1} pins the odd normal form at level f = ∞, relator form. Let r ∈ Φ(F) be a relator of the free pro-2 group on an odd number n of generators presenting a Demushkin group whose canonical character has image {±1}. Then a continuous automorphism of F carries r to x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n). At rank one this is the relator x₁² of ℤ/2.

source
theorem TauCeti.freeProP.range_demushkinCharacter_eq_zpowers_neg_one_or_unitsPlusMinus_of_odd {n : ℕ} (hn : Odd n) {r : freeProP 2 (Fin n)} (hr : r ∈ proPFrattini 2 (freeProP 2 (Fin n))) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})) :
(demushkinCharacter hG).range = Subgroup.zpowers (-1) ∨ 3 ≤ n ∧ ∃ (f : ℕ), 2 ≤ f ∧ (demushkinCharacter hG).range = unitsPlusMinus f

The necessity half of the existence theorem for odd rank, relator form (Labute, Theorem 1 and Remark 2). Let r ∈ Φ(F) be a relator of the free pro-2 group on an odd number n of generators presenting a Demushkin group. Then the image of the canonical character of ⟨X ∣ r⟩ is {±1}, or n ≥ 3 and the image is {±1} × U^(f) for some f ≥ 2. At rank one the image is {±1}, the odd word at every level reading x₁² there.

source
theorem TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_odd {n : ℕ} (hn : Odd n) {A : Subgroup ℤ_[2]ˣ} :
(∃ (r : freeProP 2 (Fin n)) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})), demushkinRank hG = n ∧ (demushkinCharacter hG).range = A) ↔ A = Subgroup.zpowers (-1) ∨ 3 ≤ n ∧ ∃ (f : ℕ), 2 ≤ f ∧ A = unitsPlusMinus f

The existence theorem of the classification for odd rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). Let n be odd and let A ≤ ℤ₂ˣ be a subgroup. Then (n, A) is the pair of invariants of a Demushkin group, presented on n generators by one relator, exactly when A = {±1}, or n ≥ 3 and A = {±1} × U^(f) for some f ≥ 2. At n = 1 the only admissible image is {±1}, the image of the canonical character of ℤ/2. Every such A is closed and pro-2, so no hypothesis on A is needed.