Pro-p groups and the unit group ℤ_pˣ

Every open normal subgroup of ℤ_2ˣ contains a principal unit group U^(f) = 1 + 2^f ℤ_2, whose index is 2 ^ (f - 1), so every continuous finite quotient of ℤ_2ˣ is a 2-group. This is what makes ℤ_2ˣ an admissible target for continuous characters of pro-2 groups, such as the orientation character of a dyadic Demushkin group. For odd p the unit group ℤ_pˣ is not pro-p, since it contains the roots of unity of order p - 1. In the other direction, a continuous character of a pro-p group into ℤ_pˣ has pro-p range, so it takes values in the principal units 1 + pℤ_p. More precisely, a continuous character with values in 1 + pℤ_p takes the k-th term λ_k(G) of the lower p-series into 1 + p ^ (k + 1) ℤ_p, one power of p per step, because p-th powers raise the level of a principal unit by one and ℤ_pˣ is commutative.

Since ℤ_2ˣ is pro-2, its elements have 2-adic powers v ^ l, l ∈ ℤ_2 (TauCeti.IsProP.padicPow), and a unit is a 2-adic power of v exactly when it lies in the closed subgroup generated by v (TauCeti.IsProP.mem_topologicalClosure_closure_singleton_iff). Combined with the computation of the closed subgroups generated by prescribed units in TauCeti.NumberTheory.Padics.GeneratedClosedSubgroups, this gives explicit power relations between units: when 4 ∣ a and 2 ^ f ∤ a, the unit (1 - 2^f)⁻¹ is a 2-adic power of -(1 + a)⁻¹.

The sign -1 has order two, so (-1) ^ s depends only on s mod 2, and a relation v ^ s u ^ t = 1 between a unit v of sign -1 and a unit u ∈ 1 + 4ℤ_2 forces s to be even: this is how the two marked values of a character with image {±1} × U^(f) are separated. In that situation v ^ 2 = (-v) ^ 2 ∈ U^(f) is a 2-adic power of a topological generator u of U^(f).

For f ≥ 1, and f ≥ 2 when p = 2, the principal unit group U^(f) is itself a copy of ℤ_p: a unit w of exact level f topologically generates it and has infinite order, so l ↦ w ^ l is a topological group isomorphism Multiplicative ℤ_[p] ≃ₜ* U^(f). Its inverse reads off the p-adic exponent of a principal unit with respect to w, continuously and multiplicatively.

Main results

• TauCeti.isProP_units_padicInt_two: ℤ_2ˣ is a pro-2 group.
• TauCeti.neg_one_padicPow, TauCeti.two_dvd_of_padicPow_mul_padicPow_eq_one: (-1) ^ s is (-1) ^ (s mod 2), and a relation v ^ s u ^ t = 1 with -v, u ∈ 1 + 4ℤ_2 has s even.
• TauCeti.exists_padicPow_eq_sq_of_neg_mem_unitsPrincipal: if -v ∈ U^(f) and u has exact level f ≥ 2, then v ^ 2 is a 2-adic power of u.
• TauCeti.IsProP.mem_unitsPrincipal_one: a continuous character of a pro-p group into ℤ_pˣ takes values in the principal units 1 + pℤ_p.
• TauCeti.mem_unitsPrincipal_of_mem_pLowerCentralSeries: a continuous character with values in 1 + pℤ_p takes λ_k(G) into 1 + p ^ (k + 1) ℤ_p.
• TauCeti.exists_padicPow_eq_of_not_dvd: when 4 ∣ a and 2 ^ f ∤ a, the unit (1 - 2^f)⁻¹ is a 2-adic power of -(1 + a)⁻¹ in ℤ_2ˣ.
• TauCeti.principalUnitsEquiv: for a unit w of exact level f, the isomorphism Multiplicative ℤ_[p] ≃ₜ* U^(f), l ↦ w ^ l.

theorem TauCeti.IsProP.mem_unitsPrincipal_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] (hG : IsProP p G) (χ : G →ₜ* ℤ_[p]ˣ) (g : G) : χ g ∈ unitsPrincipal p 1

A continuous character of a pro-p group takes values in the principal units 1 + pℤ_p: its range is a pro-p subgroup of ℤ_pˣ.

theorem TauCeti.mem_unitsPrincipal_of_mem_pLowerCentralSeries {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) {k : ℕ} {g : G} (hg : g ∈ pLowerCentralSeries p G k) : χ g ∈ unitsPrincipal p (k + 1)

A character with values in 1 + pℤ_p takes λ_k(G) into 1 + p ^ (k + 1) ℤ_p. The p-th power of an element of 1 + p ^ (k + 1) ℤ_p lies in 1 + p ^ (k + 2) ℤ_p, commutators are killed because ℤ_pˣ is commutative, and 1 + p ^ (k + 2) ℤ_p is closed.

theorem TauCeti.isProP_units_padicInt_two : IsProP 2 ℤ_[2]ˣ

ℤ_2ˣ is pro-2: every open normal subgroup contains a principal unit group U^(f), of index 2 ^ (f - 1).

2-adic powers in ℤ_2ˣ

@[simp]

theorem TauCeti.neg_one_padicPow (s : ℤ_[2]) : isProP_units_padicInt_two.padicPow (-1) s = (-1) ^ s.appr 1

In ℤ_2ˣ, the 2-adic power (-1) ^ s is (-1) ^ (s mod 2).

theorem TauCeti.two_dvd_of_neg_one_padicPow_mem_unitsPrincipal {s : ℤ_[2]} (h : isProP_units_padicInt_two.padicPow (-1) s ∈ unitsPrincipal 2 2) : 2 ∣ s

If (-1) ^ s ∈ 1 + 4ℤ_2 for a 2-adic exponent s, then s is even.

theorem TauCeti.two_dvd_of_padicPow_mul_padicPow_eq_one {v u : ℤ_[2]ˣ} (hv : -v ∈ unitsPrincipal 2 2) (hu : u ∈ unitsPrincipal 2 2) {s t : ℤ_[2]} (h : isProP_units_padicInt_two.padicPow v s * isProP_units_padicInt_two.padicPow u t = 1) : 2 ∣ s

The sign of a relation between two dyadic units. If -v and u lie in 1 + 4ℤ_2 and v ^ s u ^ t = 1 for 2-adic exponents, then s is even: modulo 1 + 4ℤ_2 the relation reads (-1) ^ s = 1.

theorem TauCeti.exists_padicPow_eq_sq_of_neg_mem_unitsPrincipal {f : ℕ} (hf : 2 ≤ f) {v u : ℤ_[2]ˣ} (hv : -v ∈ unitsPrincipal 2 f) (hu : u ∈ unitsPrincipal 2 f) (hu' : u ∉ unitsPrincipal 2 (f + 1)) : ∃ (m : ℤ_[2]), isProP_units_padicInt_two.padicPow u m = v ^ 2

If -v ∈ U^(f) and u has exact level f ≥ 2, then v ^ 2 is a 2-adic power of u: v ^ 2 = (-v) ^ 2 lies in U^(f), which u topologically generates.

theorem TauCeti.exists_padicPow_sq_eq_of_mem_topologicalClosure_zpowers_two {f : ℕ} (hf : 2 ≤ f) {u x : ℤ_[2]ˣ} (hu : -u ∈ unitsPrincipal 2 f) (hu' : -u ∉ unitsPrincipal 2 (f + 1)) (hx : x ∈ (Subgroup.zpowers u).topologicalClosure) : ∃ (s : ℤ_[2]), isProP_units_padicInt_two.padicPow (u ^ 2) s = if x ∈ unitsPrincipal 2 2 then x else u⁻¹ * x

Elements of the twisted subgroup U^[f] as 2-adic powers of a generator. Let f ≥ 2 and let u generate U^[f], that is, -u has exact level f. Every x ∈ U^[f] is then a 2-adic power of u ^ 2, which generates U^(f+1) = U^[f] ∩ (1 + 4ℤ_2), after division by u when x ∉ 1 + 4ℤ_2.

theorem TauCeti.exists_padicPow_eq_of_not_dvd {f : ℕ} {a : ℤ_[2]} {v u : ℤ_[2]ˣ} (hv : ↑v * (1 + a) = -1) (hu : ↑u * (1 - 2 ^ f) = 1) (ha₄ : 4 ∣ a) (ha : ¬2 ^ f ∣ a) : ∃ (l : ℤ_[2]), isProP_units_padicInt_two.padicPow v l = u

When 4 ∣ a and 2 ^ f ∤ a, the unit (1 - 2^f)⁻¹ is a 2-adic power of -(1 + a)⁻¹: for units v, u of ℤ_2 with v (1 + a) = -1 and u (1 - 2^f) = 1, there is l ∈ ℤ_2 with v ^ l = u, because u lies in the closed subgroup U^[v₂(a)] generated by v (TauCeti.mem_topologicalClosure_zpowers_of_not_dvd).

The principal units as a copy of ℤ_p

theorem TauCeti.topologicalClosure_closure_singleton_unitsPrincipal_eq_top {p : ℕ} [Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {w : ℤ_[p]ˣ} (hw : w ∈ unitsPrincipal p f) (hw' : w ∉ unitsPrincipal p (f + 1)) : (Subgroup.closure {⟨w, hw⟩}).topologicalClosure = ⊤

A unit w of exact level f, with f ≥ 1 and f ≥ 2 when p = 2, topologically generates U^(f) also as an element of the topological group U^(f).

noncomputable def TauCeti.principalUnitsEquiv {p : ℕ} [Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {w : ℤ_[p]ˣ} (hw : w ∈ unitsPrincipal p f) (hw' : w ∉ unitsPrincipal p (f + 1)) : Multiplicative ℤ_[p] ≃ₜ* ↥(unitsPrincipal p f)

The principal units are a copy of ℤ_p. For f ≥ 1, with f ≥ 2 when p = 2, and a unit w of exact level f, the p-adic power map l ↦ w ^ l is a topological group isomorphism from the additive group of ℤ_[p] onto U^(f) = 1 + p ^ f ℤ_p. It is onto because w topologically generates U^(f), and injective because w has infinite order.

Equations

• TauCeti.principalUnitsEquiv hf hf₂ hw hw' = ⋯.padicPowEquiv ⋯ ⋯

@[simp]

theorem TauCeti.principalUnitsEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {w : ℤ_[p]ˣ} (hw : w ∈ unitsPrincipal p f) (hw' : w ∉ unitsPrincipal p (f + 1)) (l : Multiplicative ℤ_[p]) : (principalUnitsEquiv hf hf₂ hw hw') l = ⋯.padicPow ⟨w, hw⟩ (Multiplicative.toAdd l)

The isomorphism TauCeti.principalUnitsEquiv is the p-adic power map of w, computed in the pro-p group U^(f).

theorem TauCeti.principalUnitsEquiv_ofAdd_one {p : ℕ} [Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {w : ℤ_[p]ˣ} (hw : w ∈ unitsPrincipal p f) (hw' : w ∉ unitsPrincipal p (f + 1)) : (principalUnitsEquiv hf hf₂ hw hw') (Multiplicative.ofAdd 1) = ⟨w, hw⟩

The isomorphism TauCeti.principalUnitsEquiv sends 1 to w.