The closed subgroups of ℤ_2ˣ

The dyadic unit group decomposes as ℤ_2ˣ = {±1} × U^(2) with U^(2) = 1 + 4ℤ_2, and the nontrivial closed subgroups of U^(2) are the principal unit groups U^(f) = 1 + 2^f ℤ_2, f ≥ 2. Sorting a closed subgroup A ≤ ℤ_2ˣ by how it sits over {±1} gives Labute's description of all of them. Writing A₀ = A ⊓ U^(2) for the even part:

• if A₀ = 1 then A = {±1} (or A is trivial);
• if A₀ = U^(f) and -1 ∈ A then A = V^(f) := {±1} × U^(f), the subgroup generated by -1 together with U^(f);
• if A₀ = U^(f) and -1 ∉ A then either A = U^(f), or f ≥ 3 and A is the twisted subgroup U^[f-1], the closed subgroup generated by -1 + 2^(f-1).

No two members of the resulting list U^(f), V^(f) (f ≥ 2), {±1}, U^[f] (f ≥ 2) coincide, and each family is indexed faithfully by its level. The principal and twisted subgroups are procyclic, while V^(f) is not: [V^(f) : U^(f+1)] = 4 but every element of V^(f) squares into U^(f+1). Together with the indices [ℤ_2ˣ : U^(f)] = 2^(f-1), [ℤ_2ˣ : V^(f)] = 2^(f-2) and [ℤ_2ˣ : U^[f]] = 2^(f-1), this is the table from which the image of a continuous character G → ℤ_2ˣ on a pro-2 group is read off.

The last column of that table is the index (A : A²) of the subgroup of squares, which is the numerical invariant of the image of an orientation character that the existence half of the classification of Demushkin groups compares with 2 ^ n. The squares of U^(f), of V^(f) and of U^[f] are all U^(f+1), and the squares of {±1} are trivial, so (A : A²) is 2 for the three procyclic families and 4 for V^(f); for a closed subgroup A of ℤ_2ˣ it is 1, 2 or 4, with 1 exactly for A = 1 and 4 exactly for A = V^(f).

Main declarations

• TauCeti.unitsPlusMinus f: V^(f) = {±1} × U^(f), with TauCeti.mem_unitsPlusMinus_iff (u ∈ V^(f) ↔ u ∈ U^(f) ∨ -u ∈ U^(f)), TauCeti.unitsPlusMinus_le_iff (V^(f) ≤ A ↔ U^(f) ≤ A ∧ -1 ∈ A), TauCeti.index_unitsPlusMinus ([ℤ_2ˣ : V^(f)] = 2 ^ (f - 2)), TauCeti.unitsPlusMinus_inf_unitsPrincipal_two (V^(f) ⊓ U^(2) = U^(f)) and TauCeti.unitsPlusMinus_inj.
• TauCeti.unitsPlusMinus_two, TauCeti.disjoint_unitsPrincipal_zpowers_neg_one: the decomposition ℤ_2ˣ = {±1} × U^(2).
• TauCeti.closedSubgroup_units_two_classification: every nontrivial closed subgroup of ℤ_2ˣ is a U^(f), a V^(f), {±1}, or a twisted subgroup U^[f] with its model generator -1 + 2 ^ f; the lemmas TauCeti.unitsPrincipal_ne_unitsPlusMinus and their companions show that the four families are pairwise distinct.
• TauCeti.exists_topologicalClosure_zpowers_eq_of_isClosed_of_neg_one_notMem: a closed subgroup of ℤ_2ˣ not containing -1 is procyclic; TauCeti.not_exists_topologicalClosure_zpowers_eq_unitsPlusMinus: V^(f) is not.
• TauCeti.map_powMonoidHom_two_unitsPlusMinus: (V^(f))² = U^(f+1); TauCeti.relIndex_map_powMonoidHom_two_unitsPlusMinus: (V^(f) : (V^(f))²) = 4.
• TauCeti.unitsPrincipal_three_eq_range_powMonoidHom_two: the squares of ℤ_2ˣ are U^(3) = 1 + 8ℤ_2.
• TauCeti.relIndex_map_powMonoidHom_two_eq_one_or_two_or_four: (A : A²) ∈ {1, 2, 4} for closed A; TauCeti.relIndex_map_powMonoidHom_two_eq_four_iff and TauCeti.relIndex_map_powMonoidHom_two_eq_one_iff: the value 4 characterizes the V^(f) and the value 1 the trivial subgroup.

References

• J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), the remark following the corollary to Theorem 4.
• J. Neukirch, Algebraic Number Theory, Chapter II, Proposition 5.7.

The subgroups V^(f) = {±1} × U^(f)

noncomputable def TauCeti.unitsPlusMinus (f : ℕ) : Subgroup ℤ_[2]ˣ

V^(f) = {±1} × U^(f), the subgroup of ℤ_2ˣ generated by -1 together with the principal unit group U^(f). For f ≥ 2 it is the closed subgroup with even part U^(f) containing -1; at f ≤ 2 it is all of ℤ_2ˣ.

Equations

• TauCeti.unitsPlusMinus f = TauCeti.unitsPrincipal 2 f ⊔ Subgroup.zpowers (-1)

theorem TauCeti.unitsPlusMinus_def (f : ℕ) : unitsPlusMinus f = unitsPrincipal 2 f ⊔ Subgroup.zpowers (-1)

V^(f) = U^(f) ⊔ ⟨-1⟩.

@[simp]

theorem TauCeti.unitsPlusMinus_le_iff {f : ℕ} {A : Subgroup ℤ_[2]ˣ} : unitsPlusMinus f ≤ A ↔ unitsPrincipal 2 f ≤ A ∧ -1 ∈ A

V^(f) is the least subgroup containing U^(f) and -1: V^(f) ≤ A iff U^(f) ≤ A and -1 ∈ A.

@[simp]

theorem TauCeti.mem_unitsPlusMinus_iff {f : ℕ} {u : ℤ_[2]ˣ} : u ∈ unitsPlusMinus f ↔ u ∈ unitsPrincipal 2 f ∨ -u ∈ unitsPrincipal 2 f

u ∈ V^(f) iff u ∈ U^(f) or -u ∈ U^(f).

theorem TauCeti.unitsPrincipal_le_unitsPlusMinus (f : ℕ) : unitsPrincipal 2 f ≤ unitsPlusMinus f

U^(f) ≤ V^(f).

theorem TauCeti.neg_one_mem_unitsPlusMinus (f : ℕ) : -1 ∈ unitsPlusMinus f

-1 ∈ V^(f).

theorem TauCeti.unitsPlusMinus_antitone : Antitone unitsPlusMinus

The subgroups V^(f) decrease with the level.

theorem TauCeti.isOpen_unitsPlusMinus (f : ℕ) : IsOpen ↑(unitsPlusMinus f)

V^(f) is open: it contains the open subgroup U^(f).

theorem TauCeti.isClosed_unitsPlusMinus (f : ℕ) : IsClosed ↑(unitsPlusMinus f)

V^(f) is closed, being an open subgroup.

theorem TauCeti.sq_mem_unitsPrincipal_succ_of_mem_unitsPlusMinus {f : ℕ} (hf : 0 < f) {x : ℤ_[2]ˣ} (hx : x ∈ unitsPlusMinus f) : x ^ 2 ∈ unitsPrincipal 2 (f + 1)

Every element of V^(f) squares into U^(f+1), for f ≥ 1.

The decomposition ℤ_2ˣ = {±1} × U^(2)

@[simp]

theorem TauCeti.unitsPlusMinus_two : unitsPlusMinus 2 = ⊤

ℤ_2ˣ = {±1} · U^(2): every dyadic unit is ≡ ±1 mod 4.

theorem TauCeti.disjoint_unitsPrincipal_zpowers_neg_one {f : ℕ} (hf : 2 ≤ f) : Disjoint (unitsPrincipal 2 f) (Subgroup.zpowers (-1))

{±1} ⊓ U^(f) = 1 for f ≥ 2: the two factors of ℤ_2ˣ = {±1} × U^(2) meet trivially.

theorem TauCeti.isClosed_zpowers_neg_one : IsClosed ↑(Subgroup.zpowers (-1))

{±1} is closed in ℤ_2ˣ, being the finite set {1, -1}.

Indices and levels of V^(f)

theorem TauCeti.unitsPlusMinus_inf_unitsPrincipal_two {f : ℕ} (hf : 2 ≤ f) : unitsPlusMinus f ⊓ unitsPrincipal 2 2 = unitsPrincipal 2 f

V^(f) ⊓ U^(2) = U^(f) for f ≥ 2: the even part of V^(f) is U^(f).

theorem TauCeti.relIndex_unitsPrincipal_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) : (unitsPrincipal 2 f).relIndex (unitsPlusMinus f) = 2

[V^(f) : U^(f)] = 2 for f ≥ 2: V^(f) = U^(f) ∪ -U^(f).

theorem TauCeti.relIndex_unitsPrincipal_succ_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) : (unitsPrincipal 2 (f + 1)).relIndex (unitsPlusMinus f) = 4

[V^(f) : U^(f+1)] = 4 for f ≥ 2.

theorem TauCeti.index_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) : (unitsPlusMinus f).index = 2 ^ (f - 2)

[ℤ_2ˣ : V^(f)] = 2 ^ (f - 2) for f ≥ 2.

instance TauCeti.instFiniteIndexUnitsPadicIntOfNatNatUnitsPlusMinus (f : ℕ) : (unitsPlusMinus f).FiniteIndex

theorem TauCeti.unitsPlusMinus_inj {f g : ℕ} (hf : 2 ≤ f) (hg : 2 ≤ g) : unitsPlusMinus f = unitsPlusMinus g ↔ f = g

The level of V^(f) is determined by the subgroup, for f ≥ 2.

The four families are distinct

theorem TauCeti.unitsPrincipal_ne_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) (g : ℕ) : unitsPrincipal 2 f ≠ unitsPlusMinus g

U^(f) ≠ V^(g) for f ≥ 2: -1 ∈ V^(g) but -1 ∉ U^(f).

theorem TauCeti.unitsPrincipal_ne_zpowers_neg_one {f : ℕ} (hf : 2 ≤ f) : unitsPrincipal 2 f ≠ Subgroup.zpowers (-1)

U^(f) ≠ {±1} for f ≥ 2.

theorem TauCeti.unitsPlusMinus_ne_zpowers_neg_one (f : ℕ) : unitsPlusMinus f ≠ Subgroup.zpowers (-1)

V^(f) ≠ {±1}: V^(f) contains a nontrivial principal unit group.

theorem TauCeti.unitsPrincipal_ne_topologicalClosure_zpowers {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hu : -u ∈ unitsPrincipal 2 2) : unitsPrincipal 2 f ≠ (Subgroup.zpowers u).topologicalClosure

U^(f) ≠ U^[g] for f ≥ 2: the generator u ≡ -1 mod 4 of U^[g] lies outside 1 + 4ℤ_2.

theorem TauCeti.unitsPlusMinus_ne_topologicalClosure_zpowers (f : ℕ) {g : ℕ} (hg : 2 ≤ g) {u : ℤ_[2]ˣ} (hu : -u ∈ unitsPrincipal 2 g) (hu' : -u ∉ unitsPrincipal 2 (g + 1)) : unitsPlusMinus f ≠ (Subgroup.zpowers u).topologicalClosure

V^(f) ≠ U^[g]: -1 ∈ V^(f) but -1 ∉ U^[g].

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

{±1} ≠ U^[g]: -1 ∉ U^[g].

The classification

theorem TauCeti.eq_zpowers_neg_one_of_inf_unitsPrincipal_two_eq_bot {A : Subgroup ℤ_[2]ˣ} (hA : A ≠ ⊥) (h : A ⊓ unitsPrincipal 2 2 = ⊥) : A = Subgroup.zpowers (-1)

A nontrivial subgroup of ℤ_2ˣ meeting 1 + 4ℤ_2 trivially is {±1}: every element squares into the even part.

theorem TauCeti.eq_unitsPlusMinus_of_inf_unitsPrincipal_two_eq {A : Subgroup ℤ_[2]ˣ} {f : ℕ} (h : A ⊓ unitsPrincipal 2 2 = unitsPrincipal 2 f) (h1 : -1 ∈ A) : A = unitsPlusMinus f

A subgroup of ℤ_2ˣ containing -1 with even part U^(f) is V^(f).

theorem TauCeti.exists_eq_topologicalClosure_zpowers_of_inf_unitsPrincipal_two_eq {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) {f : ℕ} (h : A ⊓ unitsPrincipal 2 2 = unitsPrincipal 2 f) (h1 : -1 ∉ A) {a : ℤ_[2]ˣ} (ha : a ∈ A) (ha2 : a ∉ unitsPrincipal 2 2) : ∃ (g : ℕ) (u : ℤ_[2]ˣ), f = g + 1 ∧ 2 ≤ g ∧ ↑u = -1 + 2 ^ g ∧ A = (Subgroup.zpowers u).topologicalClosure

A closed subgroup of ℤ_2ˣ with even part U^(f), not containing -1 and not contained in 1 + 4ℤ_2, is the twisted subgroup U^[g] with f = g + 1: it is generated by -1 + 2 ^ g.

theorem TauCeti.closedSubgroup_units_two_classification {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) (hA' : A ≠ ⊥) : (∃ (f : ℕ), 2 ≤ f ∧ A = unitsPrincipal 2 f) ∨ (∃ (f : ℕ), 2 ≤ f ∧ A = unitsPlusMinus f) ∨ A = Subgroup.zpowers (-1) ∨ ∃ (f : ℕ) (u : ℤ_[2]ˣ), 2 ≤ f ∧ ↑u = -1 + 2 ^ f ∧ A = (Subgroup.zpowers u).topologicalClosure

Labute's classification of the closed subgroups of ℤ_2ˣ. Every nontrivial closed subgroup of ℤ_2ˣ is a principal unit group U^(f) with f ≥ 2, a subgroup V^(f) = {±1} × U^(f) with f ≥ 2, the subgroup {±1}, or a twisted subgroup U^[f] with f ≥ 2, generated by -1 + 2 ^ f. The four families are pairwise distinct and faithfully indexed by f: unitsPrincipal_inj, unitsPlusMinus_inj, topologicalClosure_zpowers_two_eq_iff and the ne lemmas above.

Procyclicity

theorem TauCeti.exists_topologicalClosure_zpowers_eq_of_isClosed_of_neg_one_notMem {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) (h1 : -1 ∉ A) : ∃ (u : ℤ_[2]ˣ), (Subgroup.zpowers u).topologicalClosure = A

A closed subgroup of ℤ_2ˣ not containing -1 is procyclic: it is 1, a principal unit group U^(f), or a twisted subgroup U^[f], each topologically generated by one element.

theorem TauCeti.not_exists_topologicalClosure_zpowers_eq_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) : ¬∃ (u : ℤ_[2]ˣ), (Subgroup.zpowers u).topologicalClosure = unitsPlusMinus f

V^(f) is not procyclic for f ≥ 2: [V^(f) : U^(f+1)] = 4, while a closed subgroup closure ⟨u⟩ with u² ∈ U^(f+1) is contained in U^(f+1) ∪ u U^(f+1).

The subgroup of squares and the index (A : A²)

@[simp]

theorem TauCeti.map_powMonoidHom_two_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) : Subgroup.map (powMonoidHom 2) (unitsPlusMinus f) = unitsPrincipal 2 (f + 1)

(V^(f))² = U^(f+1) for f ≥ 2: the squares of {±1} × U^(f) are the squares of U^(f).

theorem TauCeti.relIndex_map_powMonoidHom_two_unitsPlusMinus {f : ℕ} (hf : 2 ≤ f) : (Subgroup.map (powMonoidHom 2) (unitsPlusMinus f)).relIndex (unitsPlusMinus f) = 4

(V^(f) : (V^(f))²) = 4 for f ≥ 2.

theorem TauCeti.unitsPrincipal_three_eq_range_powMonoidHom_two : unitsPrincipal 2 3 = (powMonoidHom 2).range

The squares of ℤ_2ˣ are the units U^(3) that are 1 mod 8.

theorem TauCeti.relIndex_map_powMonoidHom_two_eq_two_or_exists_eq_unitsPlusMinus {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) (hA' : A ≠ ⊥) : (Subgroup.map (powMonoidHom 2) A).relIndex A = 2 ∨ ∃ (f : ℕ), 2 ≤ f ∧ A = unitsPlusMinus f

The table of (A : A²). A nontrivial closed subgroup A ≤ ℤ_2ˣ has (A : A²) = 2 unless it is some V^(f) with f ≥ 2: the three procyclic families U^(f), {±1} and U^[f] have (A : A²) = 2, while V^(f) has (A : A²) = 4.

theorem TauCeti.relIndex_map_powMonoidHom_two_eq_four_iff {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) : (Subgroup.map (powMonoidHom 2) A).relIndex A = 4 ↔ ∃ (f : ℕ), 2 ≤ f ∧ A = unitsPlusMinus f

(A : A²) = 4 exactly for the subgroups A = V^(f), f ≥ 2, among the closed subgroups of ℤ_2ˣ.

theorem TauCeti.relIndex_map_powMonoidHom_two_eq_one_iff {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) : (Subgroup.map (powMonoidHom 2) A).relIndex A = 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.relIndex_map_powMonoidHom_two_eq_one_or_two_or_four {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A) : (Subgroup.map (powMonoidHom 2) A).relIndex A = 1 ∨ (Subgroup.map (powMonoidHom 2) A).relIndex A = 2 ∨ (Subgroup.map (powMonoidHom 2) A).relIndex A = 4

(A : A²) ∈ {1, 2, 4} for every closed subgroup A ≤ ℤ_2ˣ.