ProCGroups/Frattini.lean
1import Mathlib.GroupTheory.Frattini
2import Mathlib.Topology.Algebra.Group.ClosedSubgroup
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Frattini.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Frattini subgroups of profinite groups
15Records Frattini subgroup constructions and quotient criteria used in finite generation and pro-C arguments.
16-/
18open Set
19open scoped Topology Pointwise
21namespace ProCGroups.Frattini
23universe u
25section MaximalSubgroups
27variable {G : Type u} [Group G]
29/-- A subgroup is maximal with respect to a predicate `P` if it satisfies `P`, is proper,
30and every proper overgroup satisfying `P` is equal to it. -/
31def Subgroup.IsMaximalWithProperty (P : Subgroup G → Prop) (H : Subgroup G) : Prop :=
32 P H ∧
33 H ≠ ⊤ ∧
34 ∀ K : Subgroup G, H ≤ K → P K → K ≠ ⊤ → K = H
36namespace Subgroup.IsMaximalWithProperty
38variable {P : Subgroup G → Prop} {H K : Subgroup G}
40/-- A maximal subgroup with property `P` satisfies the property `P`. -/
42 P H :=
43 hH.1
45/-- A maximal subgroup in the relevant class is a proper subgroup. -/
46theorem ne_top (hH : Subgroup.IsMaximalWithProperty (G := G) P H) :
47 H ≠ ⊤ :=
48 hH.2.1
50/-- Maximality forces a larger proper subgroup in the same class to be equal. -/
51theorem eq_of_le (hH : Subgroup.IsMaximalWithProperty (G := G) P H)
52 (hHK : H ≤ K) (hK : P K) (hKne : K ≠ ⊤) :
53 K = H :=
54 hH.2.2 K hHK hK hKne
56end Subgroup.IsMaximalWithProperty
58namespace Subgroup.IsMaximalOpen
60variable [TopologicalSpace G] {H K : Subgroup G}
62/-- A maximal open subgroup is open. -/
64 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H) :
65 IsOpen (H : Set G) :=
66 hH.1
68/-- A maximal subgroup in the relevant class is a proper subgroup. -/
69theorem ne_top
70 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H) :
71 H ≠ ⊤ :=
72 hH.2.1
74/-- Maximality forces a larger proper subgroup in the same class to be equal. -/
75theorem eq_of_le
76 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H)
77 (hHK : H ≤ K)
78 (hKopen : IsOpen (K : Set G)) (hKne : K ≠ ⊤) :
79 K = H :=
80 hH.2.2 K hHK hKopen hKne
82end Subgroup.IsMaximalOpen
84namespace Subgroup.IsMaximalClosed
86variable [TopologicalSpace G] {H K : Subgroup G}
88/-- A maximal closed subgroup is closed. -/
89theorem isClosed
90 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H) :
91 IsClosed (H : Set G) :=
92 hH.1
94/-- A maximal subgroup in the relevant class is a proper subgroup. -/
95theorem ne_top
96 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H) :
97 H ≠ ⊤ :=
98 hH.2.1
100/-- Maximality forces a larger proper subgroup in the same class to be equal. -/
101theorem eq_of_le
102 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H)
103 (hHK : H ≤ K)
104 (hKclosed : IsClosed (K : Set G)) (hKne : K ≠ ⊤) :
105 K = H :=
106 hH.2.2 K hHK hKclosed hKne
108end Subgroup.IsMaximalClosed
110end MaximalSubgroups
112section FrattiniWithin
114variable {G : Type u} [Group G]
116/-- The Frattini subgroup of `H`, viewed back inside the ambient group `G`. -/
117def frattiniWithin (H : Subgroup G) : Subgroup G :=
118 (frattini H).map H.subtype
120/-- The Frattini subgroup within a class is contained in every subgroup from that class. -/
121theorem frattiniWithin_le (H : Subgroup G) :
122 frattiniWithin (G := G) H ≤ H := by
123 intro x hx
124 rcases hx with ⟨y, hy, rfl⟩
125 exact y.2
127/-- Membership in the Frattini subgroup within a class means membership in every subgroup from that class. -/
128@[simp] theorem mem_frattiniWithin {H : Subgroup G} {x : H} :
129 (x : G) ∈ frattiniWithin (G := G) H ↔ x ∈ frattini H := by
130 constructor
131 · rintro ⟨y, hy, hxy⟩
132 exact (Subtype.ext hxy) ▸ hy
133 · intro hx
134 exact ⟨x, hx, rfl⟩
136end FrattiniWithin
138end ProCGroups.Frattini