Closed subgroups of ℤ_pˣ generated by prescribed units

The orientation character of a Demushkin group in normal form takes, on the marked basis, the values (1 - q)⁻¹, -1 and -(1 + α)⁻¹, with q = p ^ f a power of p and α ∈ 4ℤ_2, and its image is the closed subgroup of ℤ_pˣ these values generate (Labute, corollary to Theorem 4). This file computes those closed subgroups. A unit is specified by the equation it satisfies, as in (u : ℤ_[p]) * (1 - p ^ f) = 1, so that no inverse has to be constructed to state a result.

• A unit u with u (1 - p^f) = 1 has exact level f, and for f ≥ 1 (f ≥ 2 when p = 2) it topologically generates U^(f) = 1 + p^f ℤ_p.
• In ℤ_2ˣ, a unit u of exact level f ≥ 2 together with any v with -v ∈ U^(f) topologically generates V^(f) = {±1} × U^(f); in particular -1 and (1 - 2^f)⁻¹ do.
• In ℤ_2ˣ, a unit v with -v of exact level g ≥ 2 together with any u ∈ U^(g+1) topologically generates the twisted subgroup U^[g] generated by v alone.
• For v (1 + a) = -1 with a : ℤ_[2], -v ∈ U^(k) iff 2 ^ k ∣ a. Hence, for f ≥ 2, the values -(1 + a)⁻¹ and (1 - 2^f)⁻¹ generate V^(f) when 2 ^ f ∣ a, including a = 0. When 4 ∣ a but 2 ^ f ∤ a, they generate U^[g], where 2 ≤ g < f is the exact divisibility depth of a: 2 ^ g ∣ a and 2 ^ (g + 1) ∤ a.
• The value -(1 + a)⁻¹ alone, the only marked value in rank two, generates {±1} when a = 0 and U^[g] when 4 ∣ a ≠ 0, with g the exact divisibility depth of a.

Main results

• TauCeti.mem_unitsPrincipal_iff_of_val_mul_one_sub_pow_eq_one, TauCeti.topologicalClosure_zpowers_eq_unitsPrincipal_of_val_mul_one_sub_pow_eq_one: the unit (1 - p^f)⁻¹ has exact level f and topologically generates U^(f); TauCeti.not_isOfFinOrder_of_val_mul_one_sub_pow_eq_one: it has infinite order.
• TauCeti.topologicalClosure_zpowers_sup_zpowers_eq_unitsPlusMinus: v and u with -v ∈ U^(f) and u of exact level f ≥ 2 topologically generate V^(f); TauCeti.topologicalClosure_zpowers_neg_one_sup_zpowers_eq_unitsPlusMinus: so do -1 and (1 - 2^f)⁻¹.
• TauCeti.topologicalClosure_zpowers_sup_zpowers_eq_of_mem_unitsPrincipal_succ: adjoining an element of U^(g+1) to a generator of the twisted subgroup U^[g] does not enlarge it.
• TauCeti.neg_mem_unitsPrincipal_iff_of_val_mul_one_add_eq_neg_one: -v ∈ U^(k) ↔ 2 ^ k ∣ a for v (1 + a) = -1; TauCeti.topologicalClosure_zpowers_sup_zpowers_eq_unitsPlusMinus_of_dvd and TauCeti.exists_topologicalClosure_zpowers_sup_zpowers_eq_of_not_dvd: the closed subgroup generated by -(1 + a)⁻¹ and (1 - 2^f)⁻¹ is V^(f) if 2 ^ f ∣ a, and U^[v₂(a)] if not; TauCeti.mem_topologicalClosure_zpowers_of_not_dvd: in the latter case (1 - 2^f)⁻¹ already lies in the closed subgroup generated by -(1 + a)⁻¹ alone.
• TauCeti.topologicalClosure_zpowers_neg_one and TauCeti.exists_topologicalClosure_zpowers_eq_of_ne_zero: the closed subgroup generated by -(1 + a)⁻¹ alone is {±1} if a = 0, and U^[v₂(a)] if 4 ∣ a ≠ 0, in which case TauCeti.not_isOfFinOrder_of_val_mul_one_add_eq_neg_one says that -(1 + a)⁻¹ has infinite order; TauCeti.topologicalClosure_zpowers_eq_of_val_mul_one_add_eq_neg_one: when a has exact divisibility depth g ≥ 2 it is U^[g], the closed subgroup generated by -1 + 2^g, and TauCeti.topologicalClosure_zpowers_eq_of_val_mul_one_add_two_pow_eq_neg_one is the case a = 2^g.

References

• J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), Theorem 4 and its corollary, and the remark following it.

The unit (1 - p ^ f)⁻¹

theorem TauCeti.exists_val_mul_one_sub_pow_eq_one (p : ℕ) [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) : ∃ (u : ℤ_[p]ˣ), ↑u * (1 - ↑p ^ f) = 1

For f ≥ 1, 1 - p ^ f is a unit of ℤ_p, so there is a unit u with u (1 - p ^ f) = 1: the value (1 - q)⁻¹ of the orientation character in normal form, for q = p ^ f.

theorem TauCeti.mem_unitsPrincipal_iff_of_val_mul_one_sub_eq_one {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℤ_[p]} {u : ℤ_[p]ˣ} (hu : ↑u * (1 - a) = 1) {k : ℕ} : u ∈ unitsPrincipal p k ↔ ↑p ^ k ∣ a

A unit u with u (1 - a) = 1 lies in U^(k) exactly when p ^ k ∣ a: its inverse is 1 - a.

theorem TauCeti.mem_unitsPrincipal_iff_of_val_mul_one_sub_pow_eq_one {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} {u : ℤ_[p]ˣ} (hu : ↑u * (1 - ↑p ^ f) = 1) {k : ℕ} : u ∈ unitsPrincipal p k ↔ k ≤ f

A unit u with u (1 - p ^ f) = 1 lies in U^(k) exactly when k ≤ f: it has exact level f.

theorem TauCeti.topologicalClosure_zpowers_eq_unitsPrincipal_of_val_mul_one_sub_pow_eq_one {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {u : ℤ_[p]ˣ} (hu : ↑u * (1 - ↑p ^ f) = 1) : (Subgroup.zpowers u).topologicalClosure = unitsPrincipal p f

A unit u with u (1 - p ^ f) = 1 topologically generates U^(f), for f ≥ 1, and f ≥ 2 when p = 2: the image of the orientation character χ(x₂) = (1 - q)⁻¹, χ(x_i) = 1 otherwise, of a Demushkin group with q = p ^ f ≠ 2 is 1 + qℤ_p.

theorem TauCeti.not_isOfFinOrder_of_val_mul_one_sub_pow_eq_one {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf₂ : p = 2 → 2 ≤ f) {u : ℤ_[p]ˣ} (hu : ↑u * (1 - ↑p ^ f) = 1) : ¬IsOfFinOrder u

A unit u with u (1 - p ^ f) = 1 has infinite order, for f ≥ 2 when p = 2 (the equation forces f ≥ 1): it is a principal unit ≠ 1 of level f, and those have infinite order (TauCeti.not_isOfFinOrder_of_mem_unitsPrincipal).

Two generators in ℤ_2ˣ

theorem TauCeti.topologicalClosure_zpowers_sup_zpowers_eq_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) {v u : ℤ_[2]ˣ} (hv : -v ∈ unitsPrincipal 2 f) (hu : u ∈ unitsPrincipal 2 f) (hu' : u ∉ unitsPrincipal 2 (f + 1)) : (Subgroup.zpowers v ⊔ Subgroup.zpowers u).topologicalClosure = unitsPlusMinus f

In ℤ_2ˣ, a unit u of exact level f ≥ 2 together with any v with -v ∈ U^(f) topologically generates V^(f) = {±1} × U^(f): u generates U^(f), and -1 = (-v) v⁻¹.

theorem TauCeti.topologicalClosure_zpowers_neg_one_sup_zpowers_eq_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hu : ↑u * (1 - 2 ^ f) = 1) : (Subgroup.zpowers (-1) ⊔ Subgroup.zpowers u).topologicalClosure = unitsPlusMinus f

In ℤ_2ˣ, the units -1 and (1 - 2 ^ f)⁻¹ topologically generate V^(f), for f ≥ 2: the image of the orientation character χ(x₁) = -1, χ(x₃) = (1 - 2^f)⁻¹, χ(x_i) = 1 otherwise, of a Demushkin group of odd rank with q = 2 is {±1} × U^(f).

theorem TauCeti.topologicalClosure_zpowers_sup_zpowers_eq_of_mem_unitsPrincipal_succ {g : ℕ} (hg : 2 ≤ g) {v u : ℤ_[2]ˣ} (hv : -v ∈ unitsPrincipal 2 g) (hv' : -v ∉ unitsPrincipal 2 (g + 1)) (hu : u ∈ unitsPrincipal 2 (g + 1)) : (Subgroup.zpowers v ⊔ Subgroup.zpowers u).topologicalClosure = (Subgroup.zpowers v).topologicalClosure

In ℤ_2ˣ, adjoining an element of U^(g+1) to a unit v with -v of exact level g ≥ 2 does not enlarge the closed subgroup it generates: the twisted subgroup U^[g] generated by v already contains U^(g+1).

The unit -(1 + a)⁻¹

theorem TauCeti.exists_val_mul_one_add_eq_neg_one {a : ℤ_[2]} (ha : 2 ∣ a) : ∃ (v : ℤ_[2]ˣ), ↑v * (1 + a) = -1

For a : ℤ_[2] divisible by 2, 1 + a is a unit, so there is a unit v with v (1 + a) = -1: the value -(1 + α)⁻¹ of the orientation character in the even-rank dyadic normal form.

theorem TauCeti.neg_mem_unitsPrincipal_iff_of_val_mul_one_add_eq_neg_one {a : ℤ_[2]} {v : ℤ_[2]ˣ} (hv : ↑v * (1 + a) = -1) {k : ℕ} : -v ∈ unitsPrincipal 2 k ↔ 2 ^ k ∣ a

For a unit v with v (1 + a) = -1, the negative -v lies in U^(k) exactly when 2 ^ k ∣ a in ℤ_[2]. For a = 0, this holds at every level.

theorem TauCeti.topologicalClosure_zpowers_sup_zpowers_eq_unitsPlusMinus_of_dvd {f : ℕ} {a : ℤ_[2]} (hf : 2 ≤ f) {v u : ℤ_[2]ˣ} (hv : ↑v * (1 + a) = -1) (hu : ↑u * (1 - 2 ^ f) = 1) (ha : 2 ^ f ∣ a) : (Subgroup.zpowers v ⊔ Subgroup.zpowers u).topologicalClosure = unitsPlusMinus f

In ℤ_2ˣ, the units -(1 + a)⁻¹ and (1 - 2 ^ f)⁻¹ topologically generate V^(f) when 2 ^ f ∣ a, for f ≥ 2: the image of the orientation character of a Demushkin group of even rank with q = 2 and v₂(α) ≥ f, including α = 0, is {±1} × U^(f).

theorem TauCeti.topologicalClosure_zpowers_neg_one : (Subgroup.zpowers (-1)).topologicalClosure = Subgroup.zpowers (-1)

In ℤ_2ˣ, the unit -1 generates the finite, hence closed, subgroup {±1}: the image of the orientation character of the rank-two Demushkin group with q = 2 and α = 0, whose only marked value is -(1 + 0)⁻¹ = -1.

theorem TauCeti.topologicalClosure_zpowers_eq_of_val_mul_one_add_eq_neg_one {g : ℕ} (hg : 2 ≤ g) {a : ℤ_[2]} (hag : 2 ^ g ∣ a) (hag' : ¬2 ^ (g + 1) ∣ a) {v w : ℤ_[2]ˣ} (hv : ↑v * (1 + a) = -1) (hw : ↑w = -1 + 2 ^ g) : (Subgroup.zpowers v).topologicalClosure = (Subgroup.zpowers w).topologicalClosure

In ℤ_2ˣ, if a has exact divisibility depth g ≥ 2, that is 2 ^ g ∣ a and 2 ^ (g + 1) ∤ a, the unit -(1 + a)⁻¹ topologically generates the twisted subgroup U^[g], the closed subgroup generated by -1 + 2 ^ g: this is the image of the orientation character of the even-rank dyadic normal form with v₂(α) = g below the level, whose marked value on x₂ is -(1 + α)⁻¹.

theorem TauCeti.topologicalClosure_zpowers_eq_of_val_mul_one_add_two_pow_eq_neg_one {g : ℕ} (hg : 2 ≤ g) {v w : ℤ_[2]ˣ} (hv : ↑v * (1 + 2 ^ g) = -1) (hw : ↑w = -1 + 2 ^ g) : (Subgroup.zpowers v).topologicalClosure = (Subgroup.zpowers w).topologicalClosure

In ℤ_2ˣ, for g ≥ 2, the unit -(1 + 2 ^ g)⁻¹ topologically generates the twisted subgroup U^[g], the closed subgroup generated by -1 + 2 ^ g: the case a = 2 ^ g of TauCeti.topologicalClosure_zpowers_eq_of_val_mul_one_add_eq_neg_one.

theorem TauCeti.exists_topologicalClosure_zpowers_eq_of_ne_zero {a : ℤ_[2]} {v : ℤ_[2]ˣ} (hv : ↑v * (1 + a) = -1) (ha₄ : 4 ∣ a) (ha : a ≠ 0) : ∃ (g : ℕ) (w : ℤ_[2]ˣ), 2 ≤ g ∧ 2 ^ g ∣ a ∧ ¬2 ^ (g + 1) ∣ a ∧ ↑w = -1 + 2 ^ g ∧ (Subgroup.zpowers v).topologicalClosure = (Subgroup.zpowers w).topologicalClosure

In ℤ_2ˣ, if 4 ∣ a and a ≠ 0, the unit -(1 + a)⁻¹ topologically generates the twisted subgroup U^[g], generated by -1 + 2 ^ g, where a has exact divisibility depth g ≥ 2. This is the image of the orientation character of the rank-two Demushkin group with q = 2 and α ≠ 0, whose only marked value is -(1 + α)⁻¹.

theorem TauCeti.exists_topologicalClosure_zpowers_sup_zpowers_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) : ∃ (g : ℕ) (w : ℤ_[2]ˣ), 2 ≤ g ∧ g < f ∧ 2 ^ g ∣ a ∧ ¬2 ^ (g + 1) ∣ a ∧ ↑w = -1 + 2 ^ g ∧ (Subgroup.zpowers v ⊔ Subgroup.zpowers u).topologicalClosure = (Subgroup.zpowers w).topologicalClosure

In ℤ_2ˣ, if 4 ∣ a but 2 ^ f ∤ a, the units -(1 + a)⁻¹ and (1 - 2 ^ f)⁻¹ topologically generate the twisted subgroup U^[g], generated by -1 + 2 ^ g, where a has exact divisibility depth g with 2 ≤ g < f. This is the image of the orientation character in the even-rank dyadic normal form with v₂(α) < f.

theorem TauCeti.not_isOfFinOrder_of_val_mul_one_add_eq_neg_one {a : ℤ_[2]} {v : ℤ_[2]ˣ} (hv : ↑v * (1 + a) = -1) (ha₄ : 4 ∣ a) (ha : a ≠ 0) : ¬IsOfFinOrder v

In ℤ_2ˣ, if 4 ∣ a and a ≠ 0, the unit -(1 + a)⁻¹ has infinite order: the closed subgroup it generates is the twisted subgroup U^[g], g = v₂(a), which contains the infinite group U^(g+1), while the closed subgroup generated by an element of finite order is finite.

theorem TauCeti.mem_topologicalClosure_zpowers_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) : u ∈ (Subgroup.zpowers v).topologicalClosure

In ℤ_2ˣ, when 4 ∣ a but 2 ^ f ∤ a, the unit (1 - 2 ^ f)⁻¹ lies in the closed subgroup generated by -(1 + a)⁻¹: that subgroup is U^[g] with g = v₂(a) < f, and it contains U^(g+1) ⊇ U^(f). So in this branch the image of the orientation character is topologically generated by the value -(1 + a)⁻¹ alone.