Documentation

TauCeti.Topology.Algebra.Group.Profinite.ProP.Frattini.Series

The Frattini series of a profinite group #

The Frattini series Φ_k = TauCeti.proPFrattiniSeries p G k of a topological group is defined and studied for arbitrary topological groups in TauCeti.Topology.Algebra.Group.FrattiniSeries. This file adds what holds for a profinite group G and a prime p.

For a prime p and a closed subgroup H of a profinite group, one step of the recursion is the honest Frattini subgroup of H, transported to the ambient group along the inclusion (TauCeti.proPFrattiniStep_eq_map_proPFrattini), so Φ_{k+1} = Φ(Φ_k); in particular Φ_1 = proPFrattini p G.

The Frattini series and the lower p-series λ_k = TauCeti.pLowerCentralSeries p G k interleave: the two steps differ only in that the Frattini step takes commutators inside the subgroup while the lower p-series step takes them against the whole group, so Φ_k ≤ λ_k always; and in a topologically finitely generated pro-p group every Φ_k is open, so conversely every Φ_k contains a λ_j. The two series are therefore cofinal in one another, and both are neighbourhood bases of 1; the arguments that run level by level along one of them run equally along the other.

Cofinality of the Frattini series among the open normal subgroups of a pro-p group needs no finite generation, because Φ_k ≤ λ_k and the lower p-series is already cofinal. So the Φ_k have trivial intersection in any pro-p group and such a group is the inverse limit of its quotients G ⧸ Φ_k. With finite generation the quotients are finite p-groups. Without finite generation the terms need not be open: an infinite product of copies of ℤ ⧸ p has Φ_1 = 1.

Main results #

References #

source
theorem TauCeti.proPFrattiniSeries_succ_eq_map_proPFrattini {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) (k : ℕ) :
proPFrattiniSeries p G (k + 1) = Subgroup.map (proPFrattiniSeries p G k).subtype (proPFrattini p ↥(proPFrattiniSeries p G k))

The Frattini series is the iterated pro-p Frattini subgroup. For a prime p and a profinite group, Φ_{k+1} is the pro-p Frattini subgroup of Φ_k, viewed inside the ambient group along the inclusion.

source
@[simp]
theorem TauCeti.proPFrattiniStep_top_eq_proPFrattini {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) :
proPFrattiniStep p ⊤ = proPFrattini p G

The Frattini step at the whole group of a profinite group is its pro-p Frattini subgroup. This is the simp-normal form of TauCeti.proPFrattiniSeries_one: TauCeti.proPFrattiniSeries_succ and TauCeti.proPFrattiniSeries_zero rewrite Φ_1 to proPFrattiniStep p ⊤, and this lemma carries it on to proPFrattini p G.

source
theorem TauCeti.proPFrattiniSeries_one {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) :
proPFrattiniSeries p G 1 = proPFrattini p G

The first term of the Frattini series of a profinite group is its pro-p Frattini subgroup.

source
theorem TauCeti.IsTopologicallyFinitelyGenerated.isOpen_proPFrattiniSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (k : ℕ) :
IsOpen ↑(proPFrattiniSeries p G k)

Openness of the Frattini series. For a prime p, in a topologically finitely generated profinite group every term of the Frattini series is open.

source
theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_quotient_proPFrattiniSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (k : ℕ) :
Finite (G ⧸ proPFrattiniSeries p G k)

For a prime p, in a topologically finitely generated profinite group every quotient G ⧸ Φ_k is finite.

source
theorem TauCeti.IsProP.isPGroup_quotient_proPFrattiniSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (k : ℕ) :
IsPGroup p (G ⧸ proPFrattiniSeries p G k)

For a prime p, in a topologically finitely generated pro-p group every quotient G ⧸ Φ_k is a finite p-group.

Cofinality of the Frattini series in a pro-p group #

source
theorem TauCeti.IsProP.exists_proPFrattiniSeries_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (hp : Nat.Prime p) (U : OpenNormalSubgroup G) :
∃ (k : ℕ), proPFrattiniSeries p G k ≤ ↑U.toOpenSubgroup

Cofinality of the Frattini series. In a compact pro-p group every open normal subgroup contains a term of the Frattini series. No finite generation is needed.

source
theorem TauCeti.IsProP.iInf_proPFrattiniSeries_eq_bot {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) :
⨅ (k : ℕ), proPFrattiniSeries p G k = ⊥

In a pro-p group the terms of the Frattini series have trivial intersection.

source
theorem TauCeti.IsProP.exists_pLowerCentralSeries_le_proPFrattiniSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (k : ℕ) :
∃ (j : ℕ), pLowerCentralSeries p G j ≤ proPFrattiniSeries p G k

The interleaving of the two series. For a prime p, in a topologically finitely generated pro-p group every term of the Frattini series contains a term of the lower p-series. Together with TauCeti.proPFrattiniSeries_le_pLowerCentralSeries this makes the two series cofinal in one another.

source
theorem TauCeti.IsProP.existsUnique_forall_mk_eq_proPFrattiniSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) (x : (k : ℕ) → G ⧸ proPFrattiniSeries p G k) (hcompat : ∀ (k : ℕ) (g : G), ↑g = x (k + 1) → ↑g = x k) :
∃! g : G, ∀ (k : ℕ), ↑g = x k

A pro-p group is the inverse limit of its quotients by the Frattini series. A sequence of cosets of the Φ_k, compatible along the quotient maps, is realized by a unique element.

source
theorem TauCeti.IsProP.hasAntitoneBasis_nhds_one_proPFrattiniSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) :
(nhds 1).HasAntitoneBasis fun (k : ℕ) => ↑(proPFrattiniSeries p G k)

The Frattini series is a neighbourhood basis of 1 in a topologically finitely generated pro-p group.