The finite-quotient definition of the profinite Frattini subgroup is equivalent to intersection over open normal subgroups of index two. For the reverse inclusion, each maximal subgroup of a finite two-group quotient pulls back to an actual open normal subgroup of index two. Finite generation and finiteness of the Frattini quotient are not needed.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u v
namespace ClassFieldTower.Sawininstance twoPrime : Fact (Nat.Prime 2)Surrounding namespaces, section variables, and local commands at this declaration.
universe u v
namespace ClassFieldTower.Sawin
private local instance twoPrime : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩theorem frattini_eq_bot_of_card_two
(Q : Type v) [Group Q] (hCard : Nat.card Q = 2) : frattini Q = ⊥In a group with an open-normal finite two-group basis, the profinite Frattini subgroup is the intersection of the open normal subgroups of index two. This does not require the group to be finitely generated.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u v
namespace ClassFieldTower.Sawin
private local instance twoPrime : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩theorem profiniteFrattini_eq_iInf_openNormal_index_two
(G : Type u) [Group G] [TopologicalSpace G] [ContinuousMul G]
(hG : ProCGroups.ProC.HasPGroupOpenNormalBasis 2 G) :
ClassFieldTower.ProP.profiniteFrattini G =
⨅ (U : OpenNormalSubgroup G) (_ : (U : Subgroup G).index = 2),
(U : Subgroup G)