Open subgroups of Demushkin groups

An open subgroup U of an infinite Demushkin group G is again a Demushkin group, its rank is n(U) = 2 + [G : U] (n(G) - 2), and its canonical character is the restriction of the canonical character of G (Serre's exposé, §9.2). The first two statements are read off Tate's perfect duality on the finite 𝔽_p[G]-modules of G (TauCeti/Topology/Algebra/Group/Profinite/Demushkin/Duality/Basic.lean), applied to the permutation module Coind_U^G 𝔽_p, whose cohomology is that of U by Shapiro's lemma.

• H²(U, 𝔽_p) is one-dimensional: it is H²(G, Coind_U^G 𝔽_p), which the duality map α₂ identifies with the dual of H⁰(G, Hom(Coind_U^G 𝔽_p, 𝔽_p)); the dual of the permutation module is again the permutation module, so these invariants are H⁰(U, 𝔽_p) = 𝔽_p.
• The cup product of U is nondegenerate: a nonzero class of H¹(U, 𝔽_p) is a nonzero class of H¹(G, Coind_U^G 𝔽_p), which the bijective duality map α₁ pairs nontrivially with some class of H¹(G, Hom(Coind_U^G 𝔽_p, 𝔽_p)), and that pairing is the corestriction of the cup product of U (TauCeti.ContCohomology.explicitDualityPairing11_explicitCoeff1_toInternalHom).
• The rank formula is the three-term Euler formula 1 - d(U) + dim H²(U, 𝔽_p) = [G : U] (1 - d(G) + dim H²(G, 𝔽_p)) of TauCeti/Topology/Algebra/Group/Profinite/ProP/EulerCharacteristic/ThreeTerm.lean, which applies because cd_p G ≤ 2, itself a consequence of the duality, with both H² terms equal to 1.
• The canonical character of U is the restriction χ|_U of the canonical character χ of G, because χ|_U has the prescription property on U. That property follows from the injectivity of Tate's duality map α₂ of U with values in H²(U, I(χ|_U)/pⁱ⁺¹) on the twists I(χ|_U)/pⁱ (TauCeti.hasPrescriptionProperty_of_forall_injective_dualityMap2); and α₂ of U is injective because α₂ of G is injective with values in H²(G, I(χ)/pⁱ⁺¹), by Tate's duality at level pⁱ⁺¹ (TauCeti/Topology/Algebra/Group/Profinite/Demushkin/Duality/Twisted.lean), and injectivity descends from G to U through the coinduced module Coind_U^G I(χ|_U)/pⁱ by Shapiro's lemma (TauCeti.ContCohomology.dualityMap2_injective_of_injective_discreteCoind).

The hypothesis that G is infinite is used: ℤ/2 is a finite Demushkin group whose trivial subgroup is open and not Demushkin.

Main results

• TauCeti.IsDemushkin.finrank_cohomFp_two_openSubgroup: dim H²(U, 𝔽_p) = 1 for an open subgroup U of an infinite Demushkin group.
• TauCeti.IsDemushkin.openSubgroup: an open subgroup of an infinite Demushkin group is Demushkin.
• TauCeti.IsDemushkin.demushkinRank_openSubgroup_sub_two: n(U) - 2 = [G : U] (n(G) - 2) in ℤ.
• TauCeti.IsDemushkin.demushkinRank_openSubgroup: n(U) = 2 + [G : U] (n(G) - 2) in ℕ.
• TauCeti.IsDemushkin.demushkinCharacter_openSubgroup: the canonical character of an open subgroup is the restriction of the canonical character; its image is χ(U) (TauCeti.IsDemushkin.range_demushkinCharacter_openSubgroup).

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. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.9.15).

theorem TauCeti.IsDemushkin.finrank_cohomFp_two_openSubgroup {p : ℕ} [hp : 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) : Module.finrank (ZMod p) ↑(cohomFp p (↥↑U) 2).toModuleCat = 1

H²(U, 𝔽_p) of an open subgroup U of an infinite Demushkin group is one-dimensional: its explicit model has p elements.

theorem TauCeti.IsDemushkin.openSubgroup {p : ℕ} [hp : 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) : IsDemushkin p ↥↑U

An open subgroup of an infinite Demushkin group is Demushkin (Serre's exposé, §9.2). The subgroup is pro-p and topologically finitely generated with G; its H²(U, 𝔽_p) is one-dimensional by TauCeti.IsDemushkin.finrank_cohomFp_two_openSubgroup; and its cup product is nondegenerate because a nonzero class of H¹(U, 𝔽_p) ≅ H¹(G, Coind_U^G 𝔽_p) is paired nontrivially by Tate's duality map α₁ of G, a pairing which is the corestriction of a cup product of U.

theorem TauCeti.IsDemushkin.demushkinRank_openSubgroup_sub_two {p : ℕ} [hp : 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) : ↑(demushkinRank ⋯) - 2 = ↑(↑U).index * (↑(demushkinRank hG) - 2)

The rank formula for an open subgroup of an infinite Demushkin group, in ℤ: n(U) - 2 = [G : U] (n(G) - 2). This is the three-term Euler formula 1 - d(U) + dim H²(U, 𝔽_p) = [G : U] (1 - d(G) + dim H²(G, 𝔽_p)), which applies because cd_p G ≤ 2, with both H² terms equal to 1.

theorem TauCeti.IsDemushkin.demushkinRank_openSubgroup {p : ℕ} [hp : 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) : demushkinRank ⋯ = 2 + (↑U).index * (demushkinRank hG - 2)

The rank formula for an open subgroup of an infinite Demushkin group, in ℕ: n(U) = 2 + [G : U] (n(G) - 2). The subtraction is not truncated, since an infinite Demushkin group has rank at least 2.

theorem TauCeti.IsDemushkin.demushkinCharacter_openSubgroup {p : ℕ} [hp : 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) : demushkinCharacter ⋯ = (demushkinCharacter hG).comp (ContinuousMonoidHom.subgroupSubtype ↑U)

The canonical character of an open subgroup of an infinite Demushkin group is the restriction of the canonical character (Serre's exposé, §9.2): the restriction χ|_U has the prescription property on U, since Tate's duality map α₂ of U with values in H²(U, I(χ|_U)/pⁱ⁺¹) is injective on I(χ|_U)/pⁱ, as it is for G by Tate's duality at level pⁱ⁺¹.

theorem TauCeti.IsDemushkin.range_demushkinCharacter_openSubgroup {p : ℕ} [hp : 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) : (demushkinCharacter ⋯).range = Subgroup.map (demushkinCharacter hG).toMonoidHom ↑U

The image of the canonical character of an open subgroup U is the image of U under the canonical character: Im(χ|_U) = χ(U). Together with the rank formula, this is the invariant form of the open-subgroup theorem that the classification reads.