Open subgroups of Demushkin groups, up to isomorphism

An open subgroup U of an infinite Demushkin group G is again a Demushkin group, of rank n(U) = 2 + [G : U] (n(G) - 2) and with canonical character the restriction χ|_U of the canonical character χ of G, so that Im(χ|_U) = χ(U) (TauCeti/Topology/Algebra/Group/Profinite/Demushkin/OpenSubgroup.lean). Since a Demushkin group is determined up to topological isomorphism by its rank and the image of its canonical character (TauCeti.IsDemushkin.nonempty_continuousMulEquiv_iff), these two invariants identify U up to isomorphism: the isomorphism type of U depends only on n(G), the index [G : U] and the subgroup χ(U) of ℤ_pˣ. This is the classification content of Serre's open-subgroup theorem (Serre's exposé, §9.2), read through Labute's classification.

In rank two the rank formula gives n(U) = 2 for every U, so an open subgroup is isomorphic to G exactly when χ(U) = χ(G); this happens for proper subgroups, for instance every open subgroup of ℤ_p × ℤ_p, where χ is trivial, is isomorphic to ℤ_p × ℤ_p. In rank at least three, the rank strictly grows on passing to a proper open subgroup, so G is isomorphic to none of its proper open subgroups.

Main results

• TauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_iff: an open subgroup U of an infinite Demushkin group G is topologically isomorphic to a Demushkin group H if and only if n(H) = 2 + [G : U] (n(G) - 2) and Im χ_H = χ_G(U).
• TauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_openSubgroup_iff: open subgroups U ≤ G and V ≤ H of infinite Demushkin groups are topologically isomorphic if and only if [G : U] (n(G) - 2) = [H : V] (n(H) - 2) and χ_G(U) = χ_H(V).
• TauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_self_iff: an open subgroup U of an infinite Demushkin group G is topologically isomorphic to G if and only if U = G, or n(G) = 2 and χ(U) = χ(G).

References

• J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki 8 (1962/63), exposé 252, §9.2.
• J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132.

theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Infinite G] (hG : IsDemushkin p G) (U : OpenSubgroup G) {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hH : IsDemushkin p H) : Nonempty (↥↑U ≃ₜ* H) ↔ demushkinRank hH = 2 + (↑U).index * (demushkinRank hG - 2) ∧ (demushkinCharacter hH).range = Subgroup.map (demushkinCharacter hG).toMonoidHom ↑U

The isomorphism type of an open subgroup of a Demushkin group: an open subgroup U of an infinite Demushkin group G is topologically isomorphic to a Demushkin group H if and only if H has rank 2 + [G : U] (n(G) - 2) and the canonical character of H has image χ(U), where χ is the canonical character of G.

theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_openSubgroup_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Infinite G] (hG : IsDemushkin p G) (U : OpenSubgroup G) {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] [Infinite H] (hH : IsDemushkin p H) (V : OpenSubgroup H) : Nonempty (↥↑U ≃ₜ* ↥↑V) ↔ (↑U).index * (demushkinRank hG - 2) = (↑V).index * (demushkinRank hH - 2) ∧ Subgroup.map (demushkinCharacter hG).toMonoidHom ↑U = Subgroup.map (demushkinCharacter hH).toMonoidHom ↑V

Open subgroups of Demushkin groups up to isomorphism: open subgroups U ≤ G and V ≤ H of infinite Demushkin groups are topologically isomorphic if and only if [G : U] (n(G) - 2) = [H : V] (n(H) - 2) and χ_G(U) = χ_H(V), where χ_G and χ_H are the canonical characters. In particular two open subgroups of G of the same index with the same image under χ_G are isomorphic. The subtractions are not truncated, since an infinite Demushkin group has rank at least 2.

theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_self_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Infinite G] (hG : IsDemushkin p G) (U : OpenSubgroup G) : Nonempty (↥↑U ≃ₜ* G) ↔ U = ⊤ ∨ demushkinRank hG = 2 ∧ Subgroup.map (demushkinCharacter hG).toMonoidHom ↑U = (demushkinCharacter hG).range

When an open subgroup of a Demushkin group is isomorphic to the group: an open subgroup U of an infinite Demushkin group G is topologically isomorphic to G if and only if U = G, or G has rank 2 and χ(U) = χ(G) for the canonical character χ of G. In particular an infinite Demushkin group of rank at least 3 is isomorphic to none of its proper open subgroups.