The canonical character of the even-rank dyadic normal form with a 2-adic exponent

Labute's normal form for the Demushkin relators with q = 2 of even rank n is

x₁^{2+α} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n)

with a 2-adic exponent α ∈ 4ℤ₂ and a level 2 ≤ f ≤ ∞, the factor x₃^{2^f} being absent at f = ∞. The word TauCeti.demushkinWordTwoEven carries a natural exponent 2 + a, which is all the marked classification needs, because the group presented depends on α only through its valuation. The successive-approximation argument, however, produces the relator with a genuine 2-adic exponent, and reading the invariants of the group it presents off that relator needs its canonical character. The word TauCeti.demushkinWordTwoEvenPadic of TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Even.PadicExponent.Basic realises this relator, with x₁^{2+α} the 2-adic power TauCeti.IsProP.padicPow and the tail x₃^q (x₃, x₄) ⋯ (x_{n-1}, x_n) for a natural number q, even whenever the factor x₃^q is present (2 < n), so that q = 2^f is Labute's level f and q = 0 is the level f = ∞; by TauCeti.hasPrescriptionProperty_presentedProP_demushkinWordTwoEvenPadic_iff of TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Prescription, a continuous character of the pro-2 group it presents has the prescription property exactly when χ(x₂)(1 + α) = -1, χ(x₄)(1 - q) = 1 whenever the factor x₃^q is present (2 < n), and χ(x_i) = 1 otherwise. This file proves Labute's Theorem 4 and its corollary for that group:

• the presented group has exactly one character with the prescription property, the orientation TauCeti.orientationTwoEvenPadic with those values;
• the image of that character is {±1} × U^(f) when q = 2^f with 2 ≤ f and 2^f ∣ α, the twisted subgroup U^[g] generated by -1 + 2^g when g = v₂(α) ≥ 2 is smaller than the level (including the level f = ∞, that is q = 0), and {±1} when α = 0 and q = 0.

Read on the canonical character of a Demushkin group isomorphic to the presented group, the table gives the marking of the generators and the image invariant, and in particular identifies the endpoint of the even-rank dyadic family: a Demushkin group isomorphic to ⟨x₁, …, xₙ ∣ x₁^{2+α} (x₁, x₂) x₃^q (x₃, x₄) ⋯⟩ with 4 ∣ α and, as soon as the factor x₃^q is present, q ∈ {0} ∪ {2^f : f ≥ 2}, has orientation image {±1} only when α = 0 and, as soon as the factor x₃^q is present (2 < n), q = 0 (TauCeti.IsDemushkin.eq_zero_and_eq_zero_of_range_demushkinCharacter_eq_zpowers_neg_one), in which case its relator is x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) (TauCeti.demushkinWordTwoEvenPadic_zero_zero, and x₁² (x₁, x₂) at n = 2 by TauCeti.demushkinWordTwoEvenPadic_two).

Main definitions

• TauCeti.orientationTwoEvenPadic: the character of the presented group with marked values on x₂ and x₄ and trivial on the other generators.

Main results

• TauCeti.existsUnique_hasPrescriptionProperty_presentedProP_demushkinWordTwoEvenPadic: the presented group has exactly one character with the prescription property.
• TauCeti.range_eq_unitsPlusMinus_of_hasPrescriptionProperty_demushkinWordTwoEvenPadic, TauCeti.range_eq_of_hasPrescriptionProperty_demushkinWordTwoEvenPadic_of_not_dvd, TauCeti.range_eq_zpowers_neg_one_of_hasPrescriptionProperty_demushkinWordTwoEvenPadic: the image table of the canonical character; at rank two the image is procyclic, generated by χ(x₂), which is the theorem range_eq_topologicalClosure_zpowers_of_hasPrescriptionProperty_demushkinWordTwoEvenPadic_two.
• TauCeti.demushkinCharacter_apply_equiv_symm_of_equiv_demushkinWordTwoEvenPadic and the range_demushkinCharacter_…_of_equiv_demushkinWordTwoEvenPadic theorems: both tables read on the canonical character of a Demushkin group along an isomorphism onto the presented group.
• TauCeti.IsDemushkin.eq_zero_and_eq_zero_of_range_demushkinCharacter_eq_zpowers_neg_one: the image {±1} forces α = 0, and q = 0 whenever the factor x₃^q is present.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §3, Theorem 3, Theorem 4 and its corollary.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter III, §9.

The orientation of the presented group

noncomputable def TauCeti.orientationTwoEvenPadic (α : ℤ_[2]) (q n : ℕ) (v u : ℤ_[2]ˣ) : presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ

The orientation of the even dyadic normal form with 2-adic exponent and marked values v, u: the continuous character of the pro-2 group presented on n generators by x₁^{2+α} (x₁, x₂) x₃^q (x₃, x₄) ⋯ (x_{n-1}, x_n) with χ(x₂) = v, χ(x₄) = u and χ(x_i) = 1 otherwise. The canonical character is the case v = -(1 + α)⁻¹, u = (1 - q)⁻¹.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.orientationTwoEvenPadic_of (α : ℤ_[2]) (q n : ℕ) (v u : ℤ_[2]ˣ) (i : Fin n) : (orientationTwoEvenPadic α q n v u) (presentedProP.of 2 {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} i) = if ↑i = 1 then v else if ↑i = 3 then u else 1

The value of the orientation on the generators.

theorem TauCeti.orientationTwoEvenPadic_presentedProPGen_one (α : ℤ_[2]) (q n : ℕ) (v u : ℤ_[2]ˣ) (hn : 1 < n) : (orientationTwoEvenPadic α q n v u) (presentedProPGen 2 n {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} 1) = v

The orientation takes x₂ to its marked value v.

theorem TauCeti.orientationTwoEvenPadic_presentedProPGen_three (α : ℤ_[2]) (q n : ℕ) (v u : ℤ_[2]ˣ) (hn : 3 < n) : (orientationTwoEvenPadic α q n v u) (presentedProPGen 2 n {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} 3) = u

The orientation takes x₄ to its marked value u.

@[simp]

theorem TauCeti.orientationTwoEvenPadic_presentedProPGen_of_ne (α : ℤ_[2]) (q n : ℕ) (v u : ℤ_[2]ˣ) {i : ℕ} (hi₁ : i ≠ 1) (hi₃ : i ≠ 3) : (orientationTwoEvenPadic α q n v u) (presentedProPGen 2 n {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} i) = 1

The orientation is trivial on every generator other than x₂ and x₄.

theorem TauCeti.range_orientationTwoEvenPadic (α : ℤ_[2]) (q n : ℕ) (v u : ℤ_[2]ˣ) (hn : 3 < n) : (orientationTwoEvenPadic α q n v u).range = (Subgroup.zpowers v ⊔ Subgroup.zpowers u).topologicalClosure

The image of the orientation is the closed subgroup generated by its marked values v and u, as soon as the generator x₄ exists.

theorem TauCeti.range_orientationTwoEvenPadic_of_le_three (α : ℤ_[2]) (q n : ℕ) (v u : ℤ_[2]ˣ) (hn : 1 < n) (hn' : n ≤ 3) : (orientationTwoEvenPadic α q n v u).range = (Subgroup.zpowers v).topologicalClosure

For 1 < n ≤ 3 the image of the orientation is the closed subgroup generated by its marked value v: the generator x₂ exists but x₄ does not.

theorem TauCeti.hasPrescriptionProperty_orientationTwoEvenPadic (α : ℤ_[2]) (q n : ℕ) (v u : ℤ_[2]ˣ) (hn₃ : 3 < n) (hv : ↑v * (1 + α) = -1) (hu : ↑u * (1 - ↑q) = 1) : HasPrescriptionProperty (orientationTwoEvenPadic α q n v u)

The orientation with the canonical values has the prescription property: for 3 < n, the character with χ(x₂) = v, v (1 + α) = -1, χ(x₄) = u, u (1 - q) = 1, and χ(x_i) = 1 otherwise.

theorem TauCeti.hasPrescriptionProperty_orientationTwoEvenPadic_two (α : ℤ_[2]) (q : ℕ) (v u : ℤ_[2]ˣ) (hv : ↑v * (1 + α) = -1) : HasPrescriptionProperty (orientationTwoEvenPadic α q 2 v u)

The orientation with the canonical value has the prescription property in rank two: for the relator x₁^{2+α} (x₁, x₂), the character with χ(x₂) = v, v (1 + α) = -1, and χ(x₁) = 1, whatever q, which does not enter the rank-two relator, and the unused marked value u.

theorem TauCeti.eq_orientationTwoEvenPadic_of_hasPrescriptionProperty {α : ℤ_[2]} {q n : ℕ} (hα : 2 ∣ α) (hq : 2 < n → 2 ∣ q) (hn : Even n) (hn₁ : 1 < n) {χ : presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} (hχ : HasPrescriptionProperty χ) : χ = orientationTwoEvenPadic α q n (χ (presentedProPGen 2 n {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} 1)) (χ (presentedProPGen 2 n {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} 3))

Uniqueness of the canonical character: for α even, n ≥ 2 even and q even whenever the factor x₃^q is present (2 < n), a character with the prescription property is the orientation with marked values its own values χ(x₂) and χ(x₄).

theorem TauCeti.existsUnique_hasPrescriptionProperty_presentedProP_demushkinWordTwoEvenPadic {α : ℤ_[2]} {q n : ℕ} (hα : 2 ∣ α) (hq : 2 < n → 2 ∣ q) (hn : Even n) (hn₁ : 1 < n) : ∃! χ : presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ, HasPrescriptionProperty χ

The presented group has exactly one character with the prescription property (Labute, Theorem 4, for the normal form x₁^{2+α} (x₁, x₂) x₃^q (x₃, x₄) ⋯ (x_{n-1}, x_n) with α even, n ≥ 2 even and q even whenever the factor x₃^q is present (2 < n)): the orientation with χ(x₂) = -(1 + α)⁻¹ and, when the factor x₃^q is present (2 < n), χ(x₄) = (1 - q)⁻¹. At n = 2 the generator x₄ does not exist and only the value χ(x₂) is prescribed.

The image table

theorem TauCeti.range_eq_unitsPlusMinus_of_hasPrescriptionProperty_demushkinWordTwoEvenPadic {α : ℤ_[2]} {q n : ℕ} {χ : presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} {f : ℕ} (hf : 2 ≤ f) (hq : q = 2 ^ f) (hn : Even n) (hn₃ : 3 < n) (hα : 2 ^ f ∣ α) (hχ : HasPrescriptionProperty χ) : χ.range = unitsPlusMinus f

The image of the canonical character when q = 2^f and 2^f ∣ α is {±1} × U^(f), for f ≥ 2 and n ≥ 4 even: any character with the prescription property takes x₂ to -(1 + α)⁻¹ ∈ -U^(f) and x₄ to (1 - 2^f)⁻¹. This includes α = 0.

theorem TauCeti.range_eq_of_hasPrescriptionProperty_demushkinWordTwoEvenPadic_of_not_dvd {α : ℤ_[2]} {q n : ℕ} {χ : presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} {g : ℕ} (hg : 2 ≤ g) (hαg : 2 ^ g ∣ α) (hαg' : ¬2 ^ (g + 1) ∣ α) (hqg : 2 ^ (g + 1) ∣ ↑q) (hn : Even n) (hn₃ : 3 < n) {w : ℤ_[2]ˣ} (hw : ↑w = -1 + 2 ^ g) (hχ : HasPrescriptionProperty χ) : χ.range = (Subgroup.zpowers w).topologicalClosure

The image of the canonical character when v₂(α) = g is smaller than the level is the twisted subgroup U^[g], the closed subgroup generated by -1 + 2^g, for g ≥ 2 and n ≥ 4 even. The level is encoded by q, and the hypothesis 2^(g+1) ∣ q is stated for every such multiple; it includes the normal-form cases q = 2^f with f > g and q = 0, the level f = ∞. The character takes x₂ to -(1 + α)⁻¹, which generates U^[g], and x₄ to (1 - q)⁻¹ ∈ U^(g+1) ≤ U^[g].

theorem TauCeti.range_eq_zpowers_neg_one_of_hasPrescriptionProperty_demushkinWordTwoEvenPadic {α : ℤ_[2]} {q n : ℕ} {χ : presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} (hα : α = 0) (hq : 2 < n → q = 0) (hn : Even n) (hn₁ : 1 < n) (hχ : HasPrescriptionProperty χ) : χ.range = Subgroup.zpowers (-1)

The image of the canonical character at α = 0 and q = 0 is {±1}, for n ≥ 2 even, q = 0 being required only when the factor x₃^q is present (2 < n): the relator is x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n), the endpoint f = ∞ of the even dyadic family, and the character takes x₂ to -1 and every other generator to 1.

theorem TauCeti.range_eq_topologicalClosure_zpowers_of_hasPrescriptionProperty_demushkinWordTwoEvenPadic_two {α : ℤ_[2]} {q : ℕ} (hα : 2 ∣ α) {χ : presentedProP 2 (Fin 2) {demushkinWordTwoEvenPadic ⋯ α q 2 (freeProPGen 2 2)} →ₜ* ℤ_[2]ˣ} (hχ : HasPrescriptionProperty χ) : χ.range = (Subgroup.zpowers (χ (presentedProPGen 2 2 {demushkinWordTwoEvenPadic ⋯ α q 2 (freeProPGen 2 2)} 1))).topologicalClosure

At rank two the image of the canonical character is procyclic, generated by χ(x₂): for the relator x₁^{2+α} (x₁, x₂) with α even, any character with the prescription property is trivial on x₁, so its image is the closed subgroup generated by its value -(1 + α)⁻¹ on x₂.

The tables on the canonical character of a Demushkin group

theorem TauCeti.demushkinCharacter_apply_equiv_symm_of_equiv_demushkinWordTwoEvenPadic {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) {α : ℤ_[2]} {q n : ℕ} (hα : 2 ∣ α) (hq : 2 < n → 2 ∣ q) (hn : Even n) (hn₁ : 1 < n) (e : G ≃ₜ* presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)}) : ↑((demushkinCharacter hG) (e.symm (presentedProPGen 2 n {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} 1))) * (1 + α) = -1 ∧ (2 < n → ↑((demushkinCharacter hG) (e.symm (presentedProPGen 2 n {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} 3))) * (1 - ↑q) = 1) ∧ ∀ (i : ℕ), i ≠ 1 → i ≠ 3 → (demushkinCharacter hG) (e.symm (presentedProPGen 2 n {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)} i)) = 1

The character table on the canonical character. Along an isomorphism e : G ≃ₜ* ⟨x₁, …, xₙ ∣ x₁^{2+α} (x₁, x₂) x₃^q (x₃, x₄) ⋯ (x_{n-1}, x_n)⟩, for α even, n ≥ 2 even and q even whenever the factor x₃^q is present (2 < n), the canonical character of G satisfies χ(x₂)(1 + α) = -1, χ(x₄)(1 - q) = 1 when the factor x₃^q is present, and χ(x_i) = 1 otherwise, the generators being read back in G through e⁻¹.

theorem TauCeti.range_demushkinCharacter_eq_unitsPlusMinus_of_equiv_demushkinWordTwoEvenPadic {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) {α : ℤ_[2]} {q n f : ℕ} (hf : 2 ≤ f) (hq : q = 2 ^ f) (hn : Even n) (hn₃ : 3 < n) (hα : 2 ^ f ∣ α) (e : G ≃ₜ* presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)}) : (demushkinCharacter hG).range = unitsPlusMinus f

A Demushkin group isomorphic to the even dyadic normal form with q = 2^f and 2^f ∣ α has orientation image {±1} × U^(f), for f ≥ 2 and n ≥ 4 even.

theorem TauCeti.range_demushkinCharacter_eq_of_equiv_demushkinWordTwoEvenPadic_of_not_dvd {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) {α : ℤ_[2]} {q n g : ℕ} (hg : 2 ≤ g) (hαg : 2 ^ g ∣ α) (hαg' : ¬2 ^ (g + 1) ∣ α) (hqg : 2 ^ (g + 1) ∣ ↑q) (hn : Even n) (hn₃ : 3 < n) {w : ℤ_[2]ˣ} (hw : ↑w = -1 + 2 ^ g) (e : G ≃ₜ* presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)}) : (demushkinCharacter hG).range = (Subgroup.zpowers w).topologicalClosure

A Demushkin group isomorphic to the even dyadic normal form with v₂(α) = g below the level has orientation image U^[g], the closed subgroup generated by -1 + 2^g, for g ≥ 2 and n ≥ 4 even; the hypothesis 2^(g+1) ∣ q is stated for every such multiple and includes the normal-form cases q = 2^f with f > g and q = 0.

theorem TauCeti.range_demushkinCharacter_eq_zpowers_neg_one_of_equiv_demushkinWordTwoEvenPadic {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) {α : ℤ_[2]} {q n : ℕ} (hα : α = 0) (hq : 2 < n → q = 0) (hn : Even n) (hn₁ : 1 < n) (e : G ≃ₜ* presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)}) : (demushkinCharacter hG).range = Subgroup.zpowers (-1)

A Demushkin group isomorphic to the even dyadic normal form with α = 0 and q = 0 has orientation image {±1}, for n ≥ 2 even, q = 0 being required only when the factor x₃^q is present (2 < n): the relator is x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n), the endpoint f = ∞ of the even dyadic family.

theorem TauCeti.IsDemushkin.eq_zero_and_eq_zero_of_range_demushkinCharacter_eq_zpowers_neg_one {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) {α : ℤ_[2]} {q n : ℕ} (hα : 4 ∣ α) (hq : 2 < n → q = 0 ∨ ∃ (f : ℕ), 2 ≤ f ∧ q = 2 ^ f) (hn : Even n) (hn₁ : 1 < n) (e : G ≃ₜ* presentedProP 2 (Fin n) {demushkinWordTwoEvenPadic ⋯ α q n (freeProPGen 2 n)}) (hA : (demushkinCharacter hG).range = Subgroup.zpowers (-1)) : α = 0 ∧ (2 < n → q = 0)

The image {±1} pins the endpoint of the even dyadic family. If a Demushkin group is isomorphic to ⟨x₁, …, xₙ ∣ x₁^{2+α} (x₁, x₂) x₃^q (x₃, x₄) ⋯ (x_{n-1}, x_n)⟩ with 4 ∣ α and, as soon as the factor x₃^q is present (2 < n), with q = 0 or q = 2^f for some f ≥ 2, and its canonical character has image {±1}, then α = 0, and q = 0 as soon as the factor x₃^q is present (at n = 2 the relator x₁^{2+α} (x₁, x₂) does not involve q). The relator is then x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) (TauCeti.demushkinWordTwoEvenPadic_zero_zero, and TauCeti.demushkinWordTwoEvenPadic_two at n = 2).