The dyadic twisted subgroups U^[f]

For f ≥ 2, Labute's twisted subgroup U^[f] of ℤ_2ˣ is the closed subgroup generated by a dyadic unit u whose negative -u has exact principal-unit level f, the model case being u = -1 + 2 ^ f. The square of the generator has principal-unit depth f + 1, so U^[f] is U^(f+1) ∪ u U^(f+1): it meets 1 + 4ℤ₂ in exactly U^(f+1) = 1 + 2 ^ (f + 1)ℤ₂, has index 2 ^ (f - 1) in ℤ_2ˣ, does not contain -1, and depends only on f, not on the generator.

Main declarations

• TauCeti.topologicalClosure_zpowers_inf_unitsPrincipal_two: U^[f] ⊓ U^(2) = U^(f+1); TauCeti.mem_topologicalClosure_zpowers_two_iff: x ∈ U^[f] ↔ x ∈ U^(f+1) ∨ u⁻¹ x ∈ U^(f+1).
• TauCeti.index_topologicalClosure_zpowers_two: [ℤ_2ˣ : U^[f]] = 2 ^ (f - 1); TauCeti.neg_one_notMem_topologicalClosure_zpowers_two: -1 ∉ U^[f].
• TauCeti.map_powMonoidHom_two_topologicalClosure_zpowers_two: (U^[f])² = U^(f+1); TauCeti.relIndex_map_powMonoidHom_two_topologicalClosure_zpowers_two: (U^[f] : (U^[f])²) = 2.
• TauCeti.topologicalClosure_zpowers_two_eq_iff: two twisted subgroups agree iff their levels do; TauCeti.exists_val_eq_neg_one_add_two_pow: the model generator -1 + 2 ^ f exists.

References

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

theorem TauCeti.topologicalClosure_zpowers_sq_eq_unitsPrincipal_two {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) : (Subgroup.zpowers (u ^ 2)).topologicalClosure = unitsPrincipal 2 (f + 1)

For f ≥ 2 and a dyadic unit u with -u of exact level f, that is -u ∈ U^(f) but -u ∉ U^(f+1), the square u² = (-u)² has exact level f + 1, so it topologically generates U^(f+1).

theorem TauCeti.topologicalClosure_zpowers_inf_unitsPrincipal_two {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) : (Subgroup.zpowers u).topologicalClosure ⊓ unitsPrincipal 2 2 = unitsPrincipal 2 (f + 1)

For f ≥ 2 and a dyadic unit u with -u of exact level f, the even part of the closed subgroup generated by u is U^(f+1). The shift by one comes from the exact principal-unit depth of u².

theorem TauCeti.unitsPrincipal_succ_le_topologicalClosure_zpowers_two {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) : unitsPrincipal 2 (f + 1) ≤ (Subgroup.zpowers u).topologicalClosure

U^(f+1) ≤ U^[f]: the even part of the twisted subgroup.

theorem TauCeti.mem_topologicalClosure_zpowers_two_iff {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) {x : ℤ_[2]ˣ} : x ∈ (Subgroup.zpowers u).topologicalClosure ↔ x ∈ unitsPrincipal 2 (f + 1) ∨ u⁻¹ * x ∈ unitsPrincipal 2 (f + 1)

Membership in the twisted subgroup: for f ≥ 2 and -u of exact level f, the closed subgroup generated by u is U^(f+1) ∪ u U^(f+1).

theorem TauCeti.neg_mem_unitsPrincipal_and_notMem_succ_of_mem_topologicalClosure_zpowers_two {f : ℕ} (hf : 2 ≤ f) {w u : ℤ_[2]ˣ} (hw : -w ∈ unitsPrincipal 2 f) (hw' : -w ∉ unitsPrincipal 2 (f + 1)) (hu : u ∈ (Subgroup.zpowers w).topologicalClosure) (hu2 : u ∉ unitsPrincipal 2 2) : -u ∈ unitsPrincipal 2 f ∧ -u ∉ unitsPrincipal 2 (f + 1)

An element of the twisted subgroup U^[f] outside 1 + 4ℤ_2 is a topological generator of it, in the sense that its negative has exact level f: U^[f] = U^(f+1) ∪ w U^(f+1) for the generator w, and the elements outside 1 + 4ℤ_2 are those of the coset w U^(f+1).

theorem TauCeti.neg_one_notMem_topologicalClosure_zpowers_two {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) : -1 ∉ (Subgroup.zpowers u).topologicalClosure

-1 ∉ U^[f]: unlike {±1} × U^(f+1), the twisted subgroup does not contain -1.

theorem TauCeti.relIndex_unitsPrincipal_succ_topologicalClosure_zpowers_two {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) : (unitsPrincipal 2 (f + 1)).relIndex (Subgroup.zpowers u).topologicalClosure = 2

[U^[f] : U^(f+1)] = 2: the twisted subgroup is U^(f+1) ∪ u U^(f+1).

theorem TauCeti.index_topologicalClosure_zpowers_two {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hneg : -u ∈ unitsPrincipal 2 f) (hneg' : -u ∉ unitsPrincipal 2 (f + 1)) : (Subgroup.zpowers u).topologicalClosure.index = 2 ^ (f - 1)

[ℤ_2ˣ : U^[f]] = 2 ^ (f - 1): the twisted subgroup contains U^(f+1) with index 2.

The subgroup of squares

theorem TauCeti.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 = unitsPrincipal 2 (f + 1)

(U^[f])² = U^(f+1): the squares of the twisted subgroup are the principal units of level f + 1, for f ≥ 2 and -u of exact level f.

theorem TauCeti.relIndex_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).relIndex (Subgroup.zpowers u).topologicalClosure = 2

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

The level of a twisted subgroup

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

Two twisted subgroups agree iff their levels agree: U^[f] depends only on f, not on the choice of generator u with -u of exact level f.

The model generator -1 + 2 ^ f

theorem TauCeti.neg_mem_unitsPrincipal_two_of_val_eq {f : ℕ} {u : ℤ_[2]ˣ} (hu : ↑u = -1 + 2 ^ f) : -u ∈ unitsPrincipal 2 f

For (u : ℤ_[2]) = -1 + 2 ^ f, the negative -u = 1 - 2 ^ f lies in U^(f).

theorem TauCeti.neg_notMem_unitsPrincipal_two_succ_of_val_eq {f : ℕ} {u : ℤ_[2]ˣ} (hu : ↑u = -1 + 2 ^ f) : -u ∉ unitsPrincipal 2 (f + 1)

For (u : ℤ_[2]) = -1 + 2 ^ f, the negative -u = 1 - 2 ^ f does not lie in U^(f+1): it has exact level f.

theorem TauCeti.exists_val_eq_neg_one_add_two_pow {f : ℕ} (hf : 1 ≤ f) : ∃ (u : ℤ_[2]ˣ), ↑u = -1 + 2 ^ f

For f ≥ 1, -1 + 2 ^ f is a unit of ℤ_2, the model generator of U^[f].

theorem TauCeti.topologicalClosure_zpowers_inf_unitsPrincipal_two_of_val_eq {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hu : ↑u = -1 + 2 ^ f) : (Subgroup.zpowers u).topologicalClosure ⊓ unitsPrincipal 2 2 = unitsPrincipal 2 (f + 1)

The model case u = -1 + 2 ^ f of topologicalClosure_zpowers_inf_unitsPrincipal_two: here -u = 1 - 2 ^ f has exact level f.