Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.Character.Image

The image of the canonical character of a Demushkin group #

Let G be a Demushkin group with canonical character χ : G → ℤ_pˣ (TauCeti.demushkinCharacter) and q-invariant q = q(G) (TauCeti.demushkinQ), the order of the torsion subgroup of G^{ab}, or 0 when G^{ab} is torsion-free. The two invariants are tied together: χ is congruent to 1 modulo q and to nothing finer,

χ(G) ≤ 1 + p^k ℤ_p ↔ p^k ∣ q for every k

(TauCeti.range_demushkinCharacter_le_unitsPrincipal_iff). In particular χ is trivial exactly when q = 0 (TauCeti.range_demushkinCharacter_eq_bot_iff), and when q ≠ 2 the image of χ is the principal unit group 1 + qℤ_p (TauCeti.range_demushkinCharacter_eq_unitsPrincipal), because every nontrivial closed subgroup of 1 + pℤ_p for odd p, and of 1 + 4ℤ_2, is a principal unit group. For q = 2 the equivalence only says that χ is not congruent to 1 modulo 4: the image is then a closed subgroup of ℤ_2ˣ not contained in 1 + 4ℤ_2, and q does not determine which one. Conversely the image determines q, for every value of q, because the powers of p dividing q are read off the principal unit groups containing it (TauCeti.demushkinQ_eq_of_range_demushkinCharacter_eq); in particular q ≠ 2 is the condition that, at p = 2, the image lies in 1 + 4ℤ_2 (TauCeti.demushkinQ_ne_two_iff_range_demushkinCharacter_le).

The equivalence is a statement about any one-relator pro-p group ⟨X ∣ r⟩ with finite X and r ∈ Φ(F) whose relator has nondegenerate degree-one form, and it is proved there (TauCeti.HasPrescriptionProperty.range_le_unitsPrincipal_iff_forall_pow_dvd_exponentSum): the character with the prescription property is ≡ 1 mod p^k on the generators exactly when every exponent sum of r is divisible by p^k. One direction compares, for each generator x_j, the exponent sum at x_j, a crossed homomorphism for the trivial character, with the crossed homomorphism for χ taking the same values on the generators; the latter vanishes at r by the prescription property, and the two are congruent modulo p^k when χ ≡ 1 mod p^k. For the other direction, the first-order expansion of a crossed homomorphism in its character (TauCeti.IsCrossedHom.pow_succ_dvd_sub_sub_sum_degreeOneForm) turns χ ≡ 1 mod p^k and p^(k+1) ∣ exponent sums into the vanishing modulo p of the degree-one form of r against the vector (χ(x_i) - 1) / p^k, so nondegeneracy raises the congruence to p^(k+1). The exponent sums of r in turn compute q, through the abelianization G^{ab} ≅ ℤ_p^{n-1} × ℤ_p ⧸ (q).

Main results #

References #

source
@[simp]
theorem TauCeti.range_demushkinCharacter_le_unitsPrincipal_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (k : ℕ) :
(↑(demushkinCharacter hG)).range ≤ unitsPrincipal p k ↔ p ^ k ∣ demushkinQ hG

The canonical character of a Demushkin group is congruent to 1 modulo q(G), and modulo no higher power of p: it takes values in 1 + p^kℤ_p exactly when p^k divides the q-invariant. For q(G) = 0 this holds for every k.

source
@[simp]
theorem TauCeti.range_demushkinCharacter_eq_bot_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
(↑(demushkinCharacter hG)).range = ⊥ ↔ demushkinQ hG = 0

The canonical character of a Demushkin group is trivial exactly when q(G) = 0, that is when the abelianization of G is torsion-free.

source
theorem TauCeti.range_demushkinCharacter_eq_unitsPrincipal {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) {s : ℕ} (hs : demushkinQ hG = p ^ s) (h2 : demushkinQ hG ≠ 2) :
(demushkinCharacter hG).range = unitsPrincipal p s

The image of the canonical character is 1 + qℤ_p when q ≠ 2 (Labute, corollary to Theorem 4). If the q-invariant of a Demushkin group is q(G) = p^s ≠ 2, then the canonical character maps G onto the principal unit group 1 + p^sℤ_p. The case q(G) = 0 is TauCeti.range_demushkinCharacter_eq_bot_iff.

source
theorem TauCeti.demushkinQ_ne_two_iff_range_demushkinCharacter_le {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
demushkinQ hG ≠ 2 ↔ p = 2 → (demushkinCharacter hG).range ≤ unitsPrincipal p 2

q(G) ≠ 2 is read off the image of the canonical character: it holds exactly when, at p = 2, the canonical character lands in 1 + 4ℤ_2. At an odd prime q(G) is 0 or a power of p, never 2; at p = 2 it is 0 or a power of 2, and it differs from 2 exactly when 4 divides it.

source
theorem TauCeti.demushkinQ_eq_of_range_demushkinCharacter_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) {H : Type w} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hH : IsDemushkin p H) (h : (demushkinCharacter hG).range = (demushkinCharacter hH).range) :
demushkinQ hG = demushkinQ hH

The image of the canonical character determines the q-invariant. Two Demushkin groups whose canonical characters have the same image have the same q-invariant: the powers of p dividing q(G) are read off the principal unit groups 1 + p^kℤ_p containing the image (TauCeti.range_demushkinCharacter_le_unitsPrincipal_iff), and q(G) is 0 or a power of p. This holds for every value of q, including q = 2, where the image is not determined by q.

source
theorem TauCeti.demushkinQ_eq_two_of_neg_one_mem_range_demushkinCharacter {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (h : -1 ∈ (demushkinCharacter hG).range) :
demushkinQ hG = 2

A canonical character taking the value -1 forces q(G) = 2. For a Demushkin group at p = 2 whose canonical character has -1 in its image, the image does not lie in 1 + 4ℤ_2, so q(G) = 2 by TauCeti.demushkinQ_ne_two_iff_range_demushkinCharacter_le.

source
theorem TauCeti.IsDemushkin.range_demushkinCharacter_trichotomy_of_demushkinQ_eq_two {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (hq : demushkinQ hG = 2) :
(demushkinCharacter hG).range = Subgroup.zpowers (-1) ∨ (∃ (f : ℕ), 2 ≤ f ∧ (demushkinCharacter hG).range = unitsPlusMinus f) ∨ ∃ (f : ℕ) (u : ℤ_[2]ˣ), 2 ≤ f ∧ ↑u = -1 + 2 ^ f ∧ (demushkinCharacter hG).range = (Subgroup.zpowers u).topologicalClosure

The image of the canonical character of a Demushkin group with q(G) = 2. At p = 2 with q(G) = 2 the image is a closed subgroup of ℤ_2ˣ not contained in 1 + 4ℤ_2 (TauCeti.demushkinQ_ne_two_iff_range_demushkinCharacter_le), so by the classification of the closed subgroups of ℤ_2ˣ it is {±1}, or {±1} × U^(f) for some finite f ≥ 2, or Labute's twisted subgroup U^[f], the closed subgroup generated by -1 + 2^f, for some finite f ≥ 2. These three families, with the principal unit groups 1 + qℤ_p of the groups with q ≠ 2 (TauCeti.range_demushkinCharacter_eq_unitsPrincipal), are the orientation images of the classification of Demushkin groups.