Continuous characters and the pro-p Frattini subgroup

A continuous homomorphism to a discrete group of cardinality p is either trivial or has kernel of index p. Thus every continuous character into the multiplicative encoding Multiplicative (ZMod p) of 𝔽_p factors through the pro-p Frattini quotient. This is the character-theoretic input to describing the generator rank of a pro-p group by its continuous 𝔽_p-valued characters. The lift uses the quotient topology.

Conversely an open normal subgroup of index p has cyclic quotient of order p and is therefore the kernel of such a character, so the pro-p Frattini subgroup is exactly the intersection of the kernels of the continuous 𝔽_p-valued characters. Precomposition with the projection to the Frattini quotient is an isomorphism of 𝔽_p-vector spaces from the continuous 𝔽_p-dual TauCeti.continuousZModDual p of the quotient onto that of G.

Main results

• TauCeti.proPFrattini_le_ker: the pro-p Frattini subgroup is killed by every continuous character into a discrete group of cardinality p.
• TauCeti.exists_continuousMonoidHom_ker_eq: an open normal subgroup of index p is the kernel of a continuous 𝔽_p-valued character.
• TauCeti.proPFrattini_eq_iInf_ker: the pro-p Frattini subgroup is the intersection of the kernels of the continuous 𝔽_p-valued characters.
• ContinuousMonoidHom.ker_le_proPFrattini_of_forall_exists_comp_eq: a continuous homomorphism through which every continuous 𝔽_p-valued character factors has kernel inside the pro-p Frattini subgroup.
• TauCeti.frattiniQuotientDualEquiv: the continuous 𝔽_p-dual of the Frattini quotient is the continuous 𝔽_p-dual of G.
• TauCeti.continuousZModDualMap_quotientMk_bijective: for a normal subgroup N ≤ Φ(G), the continuous 𝔽_p-dual of G ⧸ N is the continuous 𝔽_p-dual of G, by precomposition with the quotient map.
• TauCeti.maximalProPQuotient.continuousZModDualMap_bijective: pullback identifies the continuous ZMod p-valued characters of G(p) and G.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.

theorem TauCeti.proPFrattini_le_ker {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] [DiscreteTopology H] (hH : Nat.card H = p) (f : G →ₜ* H) : proPFrattini p G ≤ f.ker

The pro-p Frattini subgroup lies in the kernel of every continuous homomorphism to a discrete group of cardinality p.

theorem TauCeti.exists_continuousMonoidHom_ker_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : OpenNormalSubgroup G} (hU : (↑U.toOpenSubgroup).index = p) : ∃ (φ : G →ₜ* Multiplicative (ZMod p)), φ.ker = ↑U.toOpenSubgroup

An open normal subgroup of index p is the kernel of a continuous 𝔽_p-valued character. Its quotient has prime order p, hence is cyclic of order p, and a homomorphism with open kernel is continuous.

theorem TauCeti.proPFrattini_eq_iInf_ker {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] : proPFrattini p G = ⨅ (φ : G →ₜ* Multiplicative (ZMod p)), φ.ker

The pro-p Frattini subgroup is the intersection of the kernels of the continuous 𝔽_p-valued characters. One inclusion is TauCeti.proPFrattini_le_ker; the other realises each open normal subgroup of index p as such a kernel.

theorem ContinuousMonoidHom.ker_le_proPFrattini_of_forall_exists_comp_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {H : Type u_1} [Group H] [TopologicalSpace H] (φ : G →ₜ* H) (h : ∀ (ψ : G →ₜ* Multiplicative (ZMod p)), ∃ (χ : H →ₜ* Multiplicative (ZMod p)), χ.comp φ = ψ) : φ.ker ≤ TauCeti.proPFrattini p G

The Frattini criterion for a kernel. If every continuous 𝔽_p-valued character of G factors through a continuous homomorphism φ : G → H, then the kernel of φ lies in the pro-p Frattini subgroup of G.

def TauCeti.frattiniQuotientHomEquiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] [DiscreteTopology H] (hH : Nat.card H = p) : (G ⧸ proPFrattini p G →ₜ* H) ≃ (G →ₜ* H)

Precomposition with the Frattini quotient projection identifies continuous homomorphisms from the quotient with continuous homomorphisms from G for a discrete target of cardinality p.

Equations

• TauCeti.frattiniQuotientHomEquiv hH = (TauCeti.ContinuousMonoidHom.quotientHomEquiv (TauCeti.proPFrattini p G)).trans (Equiv.subtypeUnivEquiv ⋯)

@[simp]

theorem TauCeti.frattiniQuotientHomEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] [DiscreteTopology H] (hH : Nat.card H = p) (g : G ⧸ proPFrattini p G →ₜ* H) : (frattiniQuotientHomEquiv hH) g = g.comp (ContinuousMonoidHom.quotientMk (proPFrattini p G))

Evaluation of precomposition with the Frattini quotient projection.

@[simp]

theorem TauCeti.frattiniQuotientHomEquiv_symm_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] [DiscreteTopology H] (hH : Nat.card H = p) (f : G →ₜ* H) : (frattiniQuotientHomEquiv hH).symm f = ContinuousMonoidHom.quotientLift (proPFrattini p G) f ⋯

Evaluation of the inverse Frattini quotient homomorphism equivalence.

theorem TauCeti.existsUnique_frattiniQuotient_lift {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] [DiscreteTopology H] (hH : Nat.card H = p) (f : G →ₜ* H) : ∃! g : G ⧸ proPFrattini p G →ₜ* H, g.comp (ContinuousMonoidHom.quotientMk (proPFrattini p G)) = f

Continuous homomorphisms to a discrete group of cardinality p factor uniquely through the pro-p Frattini quotient.

def TauCeti.frattiniQuotientDualEquiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] : continuousZModDual p (G ⧸ proPFrattini p G) ≃ₗ[ZMod p] continuousZModDual p G

Precomposition with the projection to the Frattini quotient is an isomorphism of 𝔽_p-vector spaces from the continuous 𝔽_p-dual of G ⧸ proPFrattini p G onto that of G: every continuous 𝔽_p-valued character of G kills the pro-p Frattini subgroup.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.frattiniQuotientDualEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (x : continuousZModDual p (G ⧸ proPFrattini p G)) (g : G) : (Additive.toMul (frattiniQuotientDualEquiv x)) g = (Additive.toMul x) ↑g

@[simp]

theorem TauCeti.frattiniQuotientDualEquiv_symm_apply_mk {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (x : continuousZModDual p G) (g : G) : (Additive.toMul (frattiniQuotientDualEquiv.symm x)) ↑g = (Additive.toMul x) g

A continuous 𝔽_p-valued character of G, viewed on the Frattini quotient through the inverse of the identification, evaluates on the class of an element as the character itself.

theorem TauCeti.continuousZModDualMap_quotientMk_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} [N.Normal] (hN : N ≤ proPFrattini p G) : Function.Bijective ⇑(ContinuousMonoidHom.quotientMk N).continuousZModDualMap

The characters of a quotient by a subgroup of the Frattini subgroup. For a normal subgroup N ≤ proPFrattini p G, precomposition with the quotient map G → G ⧸ N is a bijection from the continuous 𝔽_p-dual of G ⧸ N onto that of G: every continuous 𝔽_p-valued character of G kills the pro-p Frattini subgroup, hence N, and so descends to the quotient.

theorem TauCeti.maximalProPQuotient.continuousZModDualMap_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] : Function.Bijective ⇑{ toMonoidHom := mk p G, continuous_toFun := ⋯ }.continuousZModDualMap

Pullback along the maximal pro-p quotient identifies the continuous ZMod p-valued characters of the quotient with those of the original topological group.