Demushkin groups under topological isomorphism

The cohomological definition of a Demushkin group is intrinsic to its topological group. Continuous group isomorphisms transport its finite-dimensionality and cup-pairing conditions. The maps on cohomology use the identity on trivial ZMod p coefficients.

Main results

• TauCeti.IsDemushkin.of_equiv: transport the Demushkin property along a topological group isomorphism.
• TauCeti.isDemushkin_congr: the Demushkin property is invariant under a topological group isomorphism.

theorem TauCeti.IsDemushkin.of_equiv (p : ℕ) {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Fact (Nat.Prime p)] (hG : IsDemushkin p G) (e : G ≃ₜ* H) : IsDemushkin p H

The Demushkin property is invariant under topological group isomorphism.

theorem TauCeti.isDemushkin_congr (p : ℕ) {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Fact (Nat.Prime p)] (e : G ≃ₜ* H) : IsDemushkin p G ↔ IsDemushkin p H

A topological group isomorphism preserves the Demushkin property in both directions.