Supernatural indices of the closed subgroups of ℤ_2ˣ

The nontrivial closed subgroups of the profinite group ℤ_2ˣ are the principal unit groups U^(f) = 1 + 2^f ℤ_2, the subgroups V^(f) = {±1} × U^(f), the subgroup {±1} and the twisted subgroups U^[f] = closure ⟨-1 + 2^f⟩, where each finite parameter satisfies f ≥ 2. The three finite-parameter families have ordinary indices 2 ^ (f - 1), 2 ^ (f - 2) and 2 ^ (f - 1), so as supernatural numbers their indices are the supernatural prime powers with those exponents. This file records that table, together with the one entry that has no finite index: the supernatural index of {±1} has infinite exponent at 2, which is the value 2 ^ ∞ that the V-family formula takes at f = ∞.

The last line of the table is the supernatural index (A : A²) of the closed subgroup of squares of a closed subgroup A ≤ ℤ_2ˣ. It is p for a principal unit group U^(f) in ℤ_pˣ when f ≥ 1, with the additional restriction f ≥ 2 when p = 2; for p = 2 it is 2 for U^(f), {±1} and U^[f] and 4 for V^(f); the three values 1, 2 and 4 are the only ones it takes, 1 exactly for the trivial subgroup and 4 exactly for the V^(f). It is the numerical invariant that distinguishes the non-procyclic family V^(f) from the procyclic ones, and the one read off from the image of a continuous character of a pro-2 group in ℤ_2ˣ.

Main results

• TauCeti.profiniteIndex_unitsPrincipal_two, TauCeti.profiniteIndex_unitsPlusMinus, TauCeti.profiniteIndex_topologicalClosure_zpowers_two: the supernatural indices 2 ^ (f - 1), 2 ^ (f - 2) and 2 ^ (f - 1) of U^(f), V^(f) and U^[f] in ℤ_2ˣ.
• TauCeti.profiniteIndex_zpowers_neg_one: the index of {±1} in ℤ_2ˣ is the entry 2 ^ ∞ of the V-family at f = ∞.
• TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_unitsPrincipal, TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_unitsPlusMinus, TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_zpowers_neg_one, TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_topologicalClosure_zpowers_two: the values p, 4, 2 and 2 of (A : A²) on the four families, each read off from the ordinary relative index by TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_eq_primePower.
• TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_eq_one_or_two_or_four: (A : A²) is 1, 2 or 4 for every closed subgroup A ≤ ℤ_2ˣ; TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_eq_one_iff and TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_eq_primePower_two_iff say which subgroups take the values 1 and 4.

References

• J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), the remark following the corollary to Theorem 4.
• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.3.

The indices of the closed subgroups of ℤ_2ˣ

theorem TauCeti.profiniteIndex_unitsPrincipal_two (f : ℕ) : (unitsPrincipal 2 f).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ ↑(f - 1)

The supernatural index of the principal unit group U^(f) = 1 + 2^f ℤ_2 in ℤ_2ˣ is 2 ^ (f - 1).

theorem TauCeti.profiniteIndex_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) : (unitsPlusMinus f).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ ↑(f - 2)

The supernatural index of V^(f) = {±1} × U^(f) in ℤ_2ˣ is 2 ^ (f - 2).

theorem TauCeti.profiniteIndex_topologicalClosure_zpowers_two {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) : (Subgroup.zpowers u).topologicalClosure.profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ ↑(f - 1)

The supernatural index of the twisted subgroup U^[f] in ℤ_2ˣ is 2 ^ (f - 1), for f ≥ 2 and -u of exact level f.

theorem TauCeti.profiniteIndex_zpowers_neg_one : (Subgroup.zpowers (-1)).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ ⊤

The supernatural index of {±1} in ℤ_2ˣ is 2 ^ ∞: {±1} is contained in every V^(f), whose index 2 ^ (f - 2) is unbounded, while ℤ_2ˣ is pro-2, so every exponent away from 2 vanishes. This is the value of the V-family at f = ∞, where V^(∞) = {±1}.

The supernatural index of the squares

theorem TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_eq_primePower {p : ℕ} [hp : Fact (Nat.Prime p)] {A : Subgroup ℤ_[p]ˣ} (hA : IsClosed ↑A) {k : ℕ} (h : (Subgroup.map (powMonoidHom p) A).relIndex A = p ^ k) : ((Subgroup.map (powMonoidHom p) A).subgroupOf A).profiniteIndex = Supernatural.primePower ⟨p, ⋯⟩ ↑k

The supernatural index (A : A^p) of the subgroup of p-th powers of a closed subgroup A ≤ ℤ_pˣ is the supernatural prime power whose exponent at p is read off from the ordinary relative index.

theorem TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) : ((Subgroup.map (powMonoidHom p) (unitsPrincipal p f)).subgroupOf (unitsPrincipal p f)).profiniteIndex = Supernatural.primePower ⟨p, ⋯⟩ 1

(U^(f) : (U^(f))^p) = p as a supernatural number, for f ≥ 1, and f ≥ 2 when p = 2.

theorem TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) : ((Subgroup.map (powMonoidHom 2) (unitsPlusMinus f)).subgroupOf (unitsPlusMinus f)).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ 2

(V^(f) : (V^(f))²) = 4 as a supernatural number, for f ≥ 2.

theorem TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_zpowers_neg_one : ((Subgroup.map (powMonoidHom 2) (Subgroup.zpowers (-1))).subgroupOf (Subgroup.zpowers (-1))).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ 1

({±1} : {±1}²) = 2 as a supernatural number: squaring kills {±1}, which has order 2. This is the entry of the (A : A²) table at the closed subgroup {±1} = V^(∞).

theorem TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_topologicalClosure_zpowers_two {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) : ((Subgroup.map (powMonoidHom 2) (Subgroup.zpowers u).topologicalClosure).subgroupOf (Subgroup.zpowers u).topologicalClosure).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ 1

(U^[f] : (U^[f])²) = 2 as a supernatural number, for f ≥ 2 and -u of exact level f.

theorem TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_eq_one_or_two_or_four {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) : ((Subgroup.map (powMonoidHom 2) A).subgroupOf A).profiniteIndex = 1 ∨ ((Subgroup.map (powMonoidHom 2) A).subgroupOf A).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ 1 ∨ ((Subgroup.map (powMonoidHom 2) A).subgroupOf A).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ 2

The supernatural index (A : A²) of a closed subgroup of ℤ_2ˣ is 1, 2 or 4. Which of the three values occurs is settled by TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_eq_one_iff and TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_eq_primePower_two_iff.

theorem TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_eq_one_iff {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) : ((Subgroup.map (powMonoidHom 2) A).subgroupOf A).profiniteIndex = 1 ↔ A = ⊥

(A : A²) = 1 exactly for the trivial subgroup, among the closed subgroups of ℤ_2ˣ: every nontrivial closed subgroup has a non-square.

theorem TauCeti.profiniteIndex_subgroupOf_map_powMonoidHom_two_eq_primePower_two_iff {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) : ((Subgroup.map (powMonoidHom 2) A).subgroupOf A).profiniteIndex = Supernatural.primePower ⟨2, Nat.prime_two⟩ 2 ↔ ∃ (f : ℕ), 2 ≤ f ∧ A = unitsPlusMinus f

(A : A²) = 4, that is 2 ^ 2 as a supernatural number, exactly for the subgroups A = V^(f), f ≥ 2, among the closed subgroups of ℤ_2ˣ: the value 4 characterizes the one non-procyclic family.