The pro-p Frattini subgroup

The pro-p Frattini subgroup proPFrattini p G of a topological group G is the intersection of its open normal subgroups of index p. For a prime p and a profinite G it is the smallest closed normal subgroup with elementary abelian quotient, so that G ⧸ proPFrattini p G is the largest elementary abelian quotient of G by a closed normal subgroup; and for a pro-p group it is the Frattini subgroup in the usual sense, the intersection of the maximal open subgroups. That last identification needs the finite p-group theory of maximal subgroups and is TauCeti.IsProP.proPFrattini_eq_iInf_isCoatom, in TauCeti.Topology.Algebra.Group.Profinite.ProP.MaximalSubgroup.

The main theorem is the verbal description proPFrattini p G = closure (Gᵖ [G, G]), the topological closure of the subgroup generated by the p-th powers and the commutators. One inclusion is immediate: a quotient of prime order p is cyclic, hence commutative of exponent p, so it kills both generators. The other inclusion is where profiniteness enters. Writing N for the right-hand side, an element outside N is outside N ⊔ U for some open normal U, because a closed subgroup of a profinite group is the intersection of the subgroups N ⊔ U; the quotient by W = N ⊔ U is then a finite group that is commutative of exponent dividing p, and in such a group the subgroups of index p separate points (TauCeti.exists_index_eq_notMem_of_exponent_dvd). Pulling one of them back gives an open normal subgroup of index p missing the element.

Two consequences are recorded because they are what consumers use: for a prime p the Frattini quotient G ⧸ proPFrattini p G is commutative of exponent dividing p — an 𝔽_p-vector space — and, for a profinite G, proPFrattini p G is trivial exactly when G itself already is one. The maximality of that quotient is likewise a profinite statement, recorded as TauCeti.proPFrattini_le_iff.

Everything up to the verbal description is stated for an arbitrary topological group; compactness and total disconnectedness are assumed exactly where they are used.

Main definitions

• TauCeti.proPFrattini: the intersection of the open normal subgroups of index p.

Main results

• TauCeti.pow_mem_proPFrattini and TauCeti.commutator_le_proPFrattini: the p-th powers and the commutators lie in the pro-p Frattini subgroup.
• TauCeti.proPFrattini_eq_topologicalClosure: the verbal description proPFrattini p G = closure (Gᵖ [G, G]).
• TauCeti.isMulCommutative_quotient_proPFrattini and TauCeti.exponent_quotient_proPFrattini_dvd: the Frattini quotient is elementary abelian for a prime p.
• TauCeti.proPFrattini_le_iff: for a profinite G, a closed normal subgroup contains proPFrattini p G exactly when its quotient is elementary abelian.
• TauCeti.proPFrattini_le_ker_of_exponent_dvd: for a profinite G, the pro-p Frattini subgroup lies in the kernel of every homomorphism with closed kernel to a commutative group of exponent dividing p.
• MonoidHom.map_proPFrattini_le_of_prime: a continuous homomorphism from a profinite group preserves the pro-p Frattini subgroup, without a surjectivity hypothesis.
• TauCeti.map_proPFrattini_eq_of_surjective and TauCeti.comap_proPFrattini_eq_of_surjective: a continuous surjection of profinite groups carries the pro-p Frattini subgroup onto the pro-p Frattini subgroup, and the preimage of the latter is the former joined with the kernel.
• TauCeti.proPFrattini_eq_bot_iff: for a profinite G, the pro-p Frattini subgroup is trivial exactly when G is commutative of exponent dividing p.
• TauCeti.proPFrattini_eq_range_powMonoidHom and TauCeti.mem_proPFrattini_iff_exists_pow: for a commutative profinite group the pro-p Frattini subgroup is the subgroup of p-th powers, with no closure.
• ContinuousMulEquiv.map_proPFrattini_eq: the pro-p Frattini subgroup is characteristic under continuous automorphisms.
• TauCeti.isTopCharacteristic_proPFrattini: the pro-p Frattini subgroup is topologically characteristic.

References

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

def TauCeti.proPFrattini (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : Subgroup G

The pro-p Frattini subgroup of a topological group G: the intersection of the open normal subgroups of G of index p. For a prime p and a profinite G it is the smallest closed normal subgroup whose quotient is elementary abelian, so that G ⧸ proPFrattini p G is then the largest elementary abelian quotient of G by a closed normal subgroup; see TauCeti.proPFrattini_le_iff.

Equations

• TauCeti.proPFrattini p G = ⨅ (U : { U : OpenNormalSubgroup G // (↑U.toOpenSubgroup).index = p }), ↑(↑U).toOpenSubgroup

theorem TauCeti.proPFrattini_def (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : proPFrattini p G = ⨅ (U : { U : OpenNormalSubgroup G // (↑U.toOpenSubgroup).index = p }), ↑(↑U).toOpenSubgroup

The defining equation of the pro-p Frattini subgroup: the body of TauCeti.proPFrattini is not exposed, so unfolding it goes through this lemma.

instance TauCeti.proPFrattini_normal (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : (proPFrattini p G).Normal

The pro-p Frattini subgroup is a normal subgroup.

theorem TauCeti.mem_proPFrattini_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {x : G} : x ∈ proPFrattini p G ↔ ∀ (U : OpenNormalSubgroup G), (↑U.toOpenSubgroup).index = p → x ∈ ↑U.toOpenSubgroup

Membership in the pro-p Frattini subgroup, unfolded over the defining family.

theorem TauCeti.proPFrattini_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {U : OpenNormalSubgroup G} (hU : (↑U.toOpenSubgroup).index = p) : proPFrattini p G ≤ ↑U.toOpenSubgroup

The pro-p Frattini subgroup is contained in every open normal subgroup of index p.

instance TauCeti.isClosed_proPFrattini {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsClosed ↑(proPFrattini p G)

The pro-p Frattini subgroup is closed, being an intersection of open subgroups.

The elementary abelian generators

@[simp]

theorem TauCeti.pow_mem_proPFrattini {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (g : G) : g ^ p ∈ proPFrattini p G

Every p-th power lies in the pro-p Frattini subgroup: a quotient of order p has exponent dividing p.

theorem TauCeti.pow_mem_proPFrattini_of_dvd {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {q : ℕ} (hq : p ∣ q) (g : G) : g ^ q ∈ proPFrattini p G

Every q-th power with p ∣ q lies in the pro-p Frattini subgroup.

theorem TauCeti.commutator_le_proPFrattini {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (hp : Nat.Prime p) : commutator G ≤ proPFrattini p G

Every commutator lies in the pro-p Frattini subgroup: a quotient of prime order is cyclic, hence commutative.

theorem TauCeti.isMulCommutative_quotient_proPFrattini {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (hp : Nat.Prime p) : IsMulCommutative (G ⧸ proPFrattini p G)

The Frattini quotient is commutative.

theorem TauCeti.exponent_quotient_proPFrattini_dvd {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] : Monoid.exponent (G ⧸ proPFrattini p G) ∣ p

The Frattini quotient has exponent dividing p. For a prime p, together with TauCeti.isMulCommutative_quotient_proPFrattini this says that G ⧸ proPFrattini p G is elementary abelian, that is an 𝔽_p-vector space.

@[instance_reducible]

instance TauCeti.instCommGroupQuotientProPFrattini {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [Fact (Nat.Prime p)] : CommGroup (G ⧸ proPFrattini p G)

The Frattini quotient is an abelian group, with its existing quotient operations.

Equations

• TauCeti.instCommGroupQuotientProPFrattini = { toGroup := QuotientGroup.Quotient.group (TauCeti.proPFrattini p G), mul_comm := ⋯ }

@[instance_reducible]

instance TauCeti.instModuleQuotientProPFrattini {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [Fact (Nat.Prime p)] : Module (ZMod p) (Additive (G ⧸ proPFrattini p G))

The additive Frattini quotient is a vector space over 𝔽_p. Scalar multiplication is the canonical action on an abelian group killed by p, from AddCommGroup.zmodModule.

Equations

• TauCeti.instModuleQuotientProPFrattini = AddCommGroup.zmodModule ⋯

Functoriality

theorem MonoidHom.proPFrattini_le_comap {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : TauCeti.proPFrattini p G ≤ Subgroup.comap f (TauCeti.proPFrattini p H)

A continuous surjection carries the pro-p Frattini subgroup into the pro-p Frattini subgroup of the target: the preimage of an open normal subgroup of index p again has index p.

theorem MonoidHom.map_proPFrattini_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Subgroup.map f (TauCeti.proPFrattini p G) ≤ TauCeti.proPFrattini p H

The image of the pro-p Frattini subgroup under a continuous surjection lies in the pro-p Frattini subgroup of the target.

theorem ContinuousMulEquiv.map_proPFrattini_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) : Subgroup.map e.toMonoidHom (TauCeti.proPFrattini p G) = TauCeti.proPFrattini p H

Continuous multiplicative equivalences identify the pro-p Frattini subgroups of their source and target. In particular, the pro-p Frattini subgroup is characteristic under continuous automorphisms.

theorem TauCeti.isTopCharacteristic_proPFrattini {G : Type u} [Group G] [TopologicalSpace G] (p : ℕ) : IsTopCharacteristic G (proPFrattini p G)

The pro-p Frattini subgroup is topologically characteristic for every topological group and every natural number p.

The verbal description

theorem TauCeti.proPFrattini_eq_topologicalClosure {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) : proPFrattini p G = (Subgroup.closure (Set.range fun (g : G) => g ^ p) ⊔ commutator G).topologicalClosure

The verbal description of the pro-p Frattini subgroup. For a profinite group G and a prime p, the intersection of the open normal subgroups of index p is the closed subgroup topologically generated by the p-th powers and the commutators.

theorem TauCeti.proPFrattini_le_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) (K : Subgroup G) [K.Normal] (hK : IsClosed ↑K) : proPFrattini p G ≤ K ↔ IsMulCommutative (G ⧸ K) ∧ Monoid.exponent (G ⧸ K) ∣ p

The universal property of the Frattini quotient. For a profinite group G and a prime p, a closed normal subgroup K contains proPFrattini p G exactly when the quotient G ⧸ K is elementary abelian; that is, G ⧸ proPFrattini p G is the largest elementary abelian quotient of G by a closed normal subgroup.

theorem TauCeti.proPFrattini_le_ker_of_exponent_dvd {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) {A : Type u_1} [CommGroup A] (f : G →* A) (hf : IsClosed ↑f.ker) (hA : Monoid.exponent A ∣ p) : proPFrattini p G ≤ f.ker

For a profinite group G and a prime p, the pro-p Frattini subgroup lies in the kernel of every homomorphism with closed kernel to a commutative group of exponent dividing p; for instance, of every continuous homomorphism to a discrete elementary abelian p-group.

theorem MonoidHom.proPFrattini_le_comap_of_prime {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup H] (hp : Nat.Prime p) (f : G →* H) (hf : Continuous ⇑f) : TauCeti.proPFrattini p G ≤ Subgroup.comap f (TauCeti.proPFrattini p H)

A continuous homomorphism from a profinite group carries its pro-p Frattini subgroup into the pro-p Frattini subgroup of the target. Surjectivity is not required: the verbal description shows that the image of every p-th power and every commutator has the same form in the target.

theorem MonoidHom.map_proPFrattini_le_of_prime {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup H] (hp : Nat.Prime p) (f : G →* H) (hf : Continuous ⇑f) : Subgroup.map f (TauCeti.proPFrattini p G) ≤ TauCeti.proPFrattini p H

A continuous homomorphism from a profinite group carries its pro-p Frattini subgroup into the pro-p Frattini subgroup of the target.

theorem TauCeti.proPFrattini_eq_bot_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) : proPFrattini p G = ⊥ ↔ IsMulCommutative G ∧ Monoid.exponent G ∣ p

The pro-p Frattini subgroup of a profinite group is trivial exactly when the group is already commutative of exponent dividing p, that is an 𝔽_p-vector space.

The commutative case

theorem TauCeti.proPFrattini_eq_range_powMonoidHom {p : ℕ} {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hp : Nat.Prime p) : proPFrattini p A = (powMonoidHom p).range

The pro-p Frattini subgroup of a commutative profinite group is the subgroup of p-th powers. In the commutative case the verbal description closure (Gᵖ [G, G]) needs no closure: the p-th powers form a subgroup, which is compact, hence closed.

theorem TauCeti.mem_proPFrattini_iff_exists_pow {p : ℕ} {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hp : Nat.Prime p) {a : A} : a ∈ proPFrattini p A ↔ ∃ (b : A), b ^ p = a

In a commutative profinite group, an element lies in the pro-p Frattini subgroup exactly when it is a p-th power.

Surjective images

theorem TauCeti.map_proPFrattini_eq_of_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup G] [CompactSpace G] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hp : Nat.Prime p) (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Subgroup.map f (proPFrattini p G) = proPFrattini p H

A continuous surjection of profinite groups carries the pro-p Frattini subgroup onto the pro-p Frattini subgroup.

theorem TauCeti.comap_proPFrattini_eq_of_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup G] [CompactSpace G] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hp : Nat.Prime p) (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Subgroup.comap f (proPFrattini p H) = proPFrattini p G ⊔ f.ker

Along a continuous surjection of profinite groups, the preimage of the pro-p Frattini subgroup of the target is generated by the pro-p Frattini subgroup of the source together with the kernel.