Separating closed subgroups by finite characters

A closed subgroup of a profinite abelian pro-p group is cut out by its continuous characters with values in the finite cyclic groups ZMod (p ^ k). Given a point outside the subgroup, first enlarge the subgroup by an open normal subgroup while still missing the point. The resulting finite quotient is killed by a power of p; the ZMod dual separates its nonzero elements.

This is the finite duality input used in the class-module argument for a profinite group of strict cohomological dimension two.

Main result

• TauCeti.exists_continuous_zmodChar_of_notMem: a continuous finite p-power character is trivial on a prescribed closed subgroup but nontrivial on a prescribed point outside it.

theorem TauCeti.exists_continuous_zmodChar_of_notMem {p : ℕ} [NeZero p] {Y : Type u_1} [CommGroup Y] [TopologicalSpace Y] [IsTopologicalGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] (hY : IsProP p Y) (I : Subgroup Y) (hI : IsClosed ↑I) (y : Y) (hy : y ∉ I) : ∃ (k : ℕ) (χ : Y →* Multiplicative (ZMod (p ^ k))), Continuous ⇑χ ∧ (∀ x ∈ I, χ x = 1) ∧ χ y ≠ 1

Continuous finite p-power characters separate points from closed subgroups. If I is a closed subgroup of a profinite abelian pro-p group and y ∉ I, there is a continuous character to some ZMod (p ^ k) which is trivial on I and nontrivial on y. The base p need only be nonzero.