Source: ProCGroups.Frattini
1import Mathlib.GroupTheory.Frattini
2import Mathlib.Topology.Algebra.Group.ClosedSubgroup
4/-!
5# Pro C Groups / Frattini
7This module formalizes Frattini-type constructions for profinite groups.
8-/
10open Set
11open scoped Topology Pointwise
13namespace ProCGroups.Frattini
15universe u
17section MaximalSubgroups
19variable {G : Type u} [Group G]
21/--
22A subgroup is maximal with respect to a predicate P if it satisfies P, is proper, and every
23proper overgroup satisfying P is equal to it.
24-/
25def Subgroup.IsMaximalWithProperty (P : Subgroup G → Prop) (H : Subgroup G) : Prop :=
26 P H ∧
27 H ≠ ⊤ ∧
28 ∀ K : Subgroup G, H ≤ K → P K → K ≠ ⊤ → K = H
30namespace Subgroup.IsMaximalWithProperty
32variable {P : Subgroup G → Prop} {H K : Subgroup G}
34/-- A maximal subgroup with property P satisfies the property P. -/
35theorem property (hH : Subgroup.IsMaximalWithProperty (G := G) P H) :
36 P H :=
37 hH.1
39/-- A maximal subgroup in the given class is a proper subgroup. -/
40theorem ne_top (hH : Subgroup.IsMaximalWithProperty (G := G) P H) :
41 H ≠ ⊤ :=
42 hH.2.1
44/-- Maximality forces a larger proper subgroup in the same class to be equal. -/
45theorem eq_of_le (hH : Subgroup.IsMaximalWithProperty (G := G) P H)
46 (hHK : H ≤ K) (hK : P K) (hKne : K ≠ ⊤) :
47 K = H :=
48 hH.2.2 K hHK hK hKne
50end Subgroup.IsMaximalWithProperty
52namespace Subgroup.IsMaximalOpen
54variable [TopologicalSpace G] {H K : Subgroup G}
56/-- A subgroup that is maximal among open subgroups is open. -/
57theorem isOpen
58 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H) :
59 IsOpen (H : Set G) :=
60 hH.1
62/-- A maximal subgroup in the given class is a proper subgroup. -/
63theorem ne_top
64 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H) :
65 H ≠ ⊤ :=
66 hH.2.1
68/-- Maximality forces a larger proper subgroup in the same class to be equal. -/
69theorem eq_of_le
70 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H)
71 (hHK : H ≤ K)
72 (hKopen : IsOpen (K : Set G)) (hKne : K ≠ ⊤) :
73 K = H :=
74 hH.2.2 K hHK hKopen hKne
76end Subgroup.IsMaximalOpen
78namespace Subgroup.IsMaximalClosed
80variable [TopologicalSpace G] {H K : Subgroup G}
82/-- A maximal closed subgroup is closed. -/
83theorem isClosed
84 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H) :
85 IsClosed (H : Set G) :=
86 hH.1
88/-- A maximal subgroup in the given class is a proper subgroup. -/
89theorem ne_top
90 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H) :
91 H ≠ ⊤ :=
92 hH.2.1
94/-- Maximality forces a larger proper subgroup in the same class to be equal. -/
95theorem eq_of_le
96 (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H)
97 (hHK : H ≤ K)
98 (hKclosed : IsClosed (K : Set G)) (hKne : K ≠ ⊤) :
99 K = H :=
100 hH.2.2 K hHK hKclosed hKne
102end Subgroup.IsMaximalClosed
104end MaximalSubgroups
106section FrattiniWithin
108variable {G : Type u} [Group G]
110/-- The Frattini subgroup of \(H\), viewed back inside the ambient group \(G\). -/
111def frattiniWithin (H : Subgroup G) : Subgroup G :=
112 (frattini H).map H.subtype
114/-- The Frattini subgroup within a class is contained in every subgroup from that class. -/
115theorem frattiniWithin_le (H : Subgroup G) :
116 frattiniWithin (G := G) H ≤ H := by
117 intro x hx
118 rcases hx with ⟨y, hy, rfl⟩
119 exact y.2
121/--
122Membership in the Frattini subgroup within a class means membership in every subgroup from that
123class.
124-/
125@[simp] theorem mem_frattiniWithin {H : Subgroup G} {x : H} :
126 (x : G) ∈ frattiniWithin (G := G) H ↔ x ∈ frattini H := by
127 constructor
128 · rintro ⟨y, hy, hxy⟩
129 exact (Subtype.ext hxy) ▸ hy
130 · intro hx
131 exact ⟨x, hx, rfl⟩
133end FrattiniWithin
135end ProCGroups.Frattini