Source: ProCGroups.FiniteGroups.Classes
1import Mathlib.Algebra.Group.PUnit
2import Mathlib.Algebra.Group.ULift
3import Mathlib.Algebra.Category.Grp.FiniteGrp
4import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
5import Mathlib.GroupTheory.QuotientGroup.Basic
7/-!
8# Finite-group classes and their closure properties
10`FiniteGroupClass` bundles an isomorphism-invariant predicate whose members are finite. The
11module provides universe-independent membership through finite-group representatives and defines
12the closure conditions used throughout the pro-\(C\) library, including formations, varieties,
13Melnikov formations, hereditary classes, and full formations.
14-/
16namespace ProCGroups
18universe u v w
20/-- A class of groups, implemented as an unbundled predicate on group carriers. -/
21abbrev GroupClass := ∀ (G : Type u) [Group G], Prop
23/--
24A finite-group class is a predicate on group carriers together with a certificate that every
25member is finite.
26-/
27structure FiniteGroupClass where
28 /-- The membership predicate selecting the group carriers that belong to the class. -/
29 pred : GroupClass.{u}
30 /-- Membership supplies a `Finite` instance for the selected group. -/
31 finite_of_mem : ∀ {G : Type u} [Group G], pred G → Finite G
32 /--
33 Membership transports forward across a multiplicative equivalence, making the predicate
34 independent of the chosen carrier for a finite group.
35 -/
36 mem_of_mulEquiv :
37 ∀ {G H : Type u} [Group G] [Group H], (G ≃* H) → pred G → pred H
39/-- A finite group class coerces to its underlying predicate on finite groups. -/
40instance instCoeFunFiniteGroupClass : CoeFun FiniteGroupClass (fun _ => GroupClass.{u}) where
41 coe C := C.pred
43namespace FiniteGroupClass
46/-- Members of a bundled finite-group class are finite. -/
47theorem finite {C : FiniteGroupClass.{u}} {G : Type u} [Group G] (hG : C G) : Finite G :=
48 C.finite_of_mem hG
50/-- Cross-universe membership in a finite-group class: `G` belongs when it is multiplicatively
51equivalent to a member represented in the carrier universe of `C`. -/
52def MemAcrossUniverses (C : FiniteGroupClass.{u}) (G : Type v) [Group G] : Prop :=
53 ∃ H : FiniteGrp.{u}, C H ∧ Nonempty (H ≃* G)
55/-- Cross-universe membership still certifies that the represented group is finite. -/
56theorem finite_of_memAcrossUniverses {C : FiniteGroupClass.{u}}
57 {G : Type v} [Group G] (hG : C.MemAcrossUniverses G) : Finite G := by
58 rcases hG with ⟨H, _hH, ⟨e⟩⟩
59 exact Finite.of_equiv H e.toEquiv
61/-- Native membership gives cross-universe membership in the class's own universe. -/
62theorem memAcrossUniverses_of_mem {C : FiniteGroupClass.{u}}
63 {G : Type u} [Group G] (hG : C G) : C.MemAcrossUniverses G := by
64 letI : Finite G := C.finite hG
65 exact ⟨FiniteGrp.of G, hG, ⟨MulEquiv.refl G⟩⟩
67/-- In the class's own universe, cross-universe membership reduces to native membership. -/
68theorem mem_of_memAcrossUniverses {C : FiniteGroupClass.{u}}
69 {G : Type u} [Group G] (hG : C.MemAcrossUniverses G) : C G := by
70 rcases hG with ⟨H, hH, ⟨e⟩⟩
71 exact C.mem_of_mulEquiv e hH
73/-- Cross-universe membership agrees with the original predicate in the original universe. -/
74theorem memAcrossUniverses_iff (C : FiniteGroupClass.{u})
75 {G : Type u} [Group G] : C.MemAcrossUniverses G ↔ C G :=
76 ⟨mem_of_memAcrossUniverses, memAcrossUniverses_of_mem⟩
78/-- Cross-universe membership is invariant under a multiplicative equivalence, even when the two
79carriers live in different universes. -/
80theorem memAcrossUniverses_iff_of_mulEquiv (C : FiniteGroupClass.{u})
81 {G : Type v} {K : Type w} [Group G] [Group K] (e : G ≃* K) :
82 C.MemAcrossUniverses G ↔ C.MemAcrossUniverses K := by
83 constructor
84 · rintro ⟨H, hH, ⟨hHG⟩⟩
85 exact ⟨H, hH, ⟨hHG.trans e⟩⟩
86 · rintro ⟨H, hH, ⟨hHK⟩⟩
87 exact ⟨H, hH, ⟨hHK.trans e.symm⟩⟩
89/-- `ULift` does not affect cross-universe membership. This is the preferred public replacement
90for ad hoc Type-0 lowering lemmas. -/
91theorem memAcrossUniverses_ulift_iff (C : FiniteGroupClass.{u})
92 (G : Type v) [Group G] :
93 C.MemAcrossUniverses (ULift.{w} G) ↔ C.MemAcrossUniverses G :=
94 C.memAcrossUniverses_iff_of_mulEquiv MulEquiv.ulift
96/-- In the native universe, `ULift` invariance also holds for the original predicate. -/
97theorem ulift_mem_iff (C : FiniteGroupClass.{u}) (G : Type u) [Group G] :
98 C (ULift.{u} G) ↔ C G :=
99 ⟨fun h => C.mem_of_mulEquiv MulEquiv.ulift h,
100 fun h => C.mem_of_mulEquiv MulEquiv.ulift.symm h⟩
102/-- The object property represented by `C` on finite groups in any target universe. -/
103def objectPropertyAcrossUniverses (C : FiniteGroupClass.{u}) :
104 CategoryTheory.ObjectProperty FiniteGrp.{v} :=
105 fun G => C.MemAcrossUniverses G
107/-- The cross-universe categorical object property is closed under isomorphisms. -/
108instance objectPropertyAcrossUniverses_isClosedUnderIsomorphisms
109 (C : FiniteGroupClass.{u}) :
110 C.objectPropertyAcrossUniverses.IsClosedUnderIsomorphisms where
111 of_iso {G H} e hG := by
112 let eGrp : G.toGrp ≅ H.toGrp :=
113 (CategoryTheory.inducedFunctor FiniteGrp.toGrp).mapIso e
114 exact (C.memAcrossUniverses_iff_of_mulEquiv eGrp.groupIsoToMulEquiv).1 hG
117/--
118The finite-group class contains all trivial groups. This is the class-level form needed when a
119construction indexes over quotients and must include the terminal quotient. Formations provide
120this automatically via \(\mathrm{Formation.one\_mem}\); users of a formation should not add a
121separate hypothesis.
122-/
123class ContainsTrivialQuotients (C : FiniteGroupClass.{u}) : Prop where
124 /-- Every group with at most one element belongs to `C`, regardless of its chosen carrier. -/
125 of_subsingleton : ∀ {Q : Type u} [Group Q], Subsingleton Q → C Q
127/-- The finite group class is closed under isomorphism. -/
128def IsomClosed (C : FiniteGroupClass.{u}) : Prop :=
129 ∀ {G H : Type u} [Group G] [Group H], Nonempty (G ≃* H) → C G → C H
131/-- Every finite-group class is invariant under multiplicative equivalence by construction. -/
132theorem isomClosed (C : FiniteGroupClass.{u}) : IsomClosed C := by
133 intro G H _ _ hGH hG
134 exact C.mem_of_mulEquiv hGH.some hG
136/-- The canonical categorical object property attached to a finite-group class. -/
137def objectProperty (C : FiniteGroupClass.{u}) : CategoryTheory.ObjectProperty FiniteGrp.{u} :=
138 fun G => C G
140/-- The categorical object property of a finite-group class is closed under isomorphisms. -/
141instance objectProperty_isClosedUnderIsomorphisms (C : FiniteGroupClass.{u}) :
142 C.objectProperty.IsClosedUnderIsomorphisms where
143 of_iso {G H} e hG := by
144 let eGrp : G.toGrp ≅ H.toGrp :=
145 (CategoryTheory.inducedFunctor FiniteGrp.toGrp).mapIso e
146 exact C.mem_of_mulEquiv eGrp.groupIsoToMulEquiv hG
148/-- The finite group class is closed under taking subgroups. -/
149def SubgroupClosed (C : FiniteGroupClass.{u}) : Prop :=
150 ∀ {G : Type u} [Group G] (H : Subgroup G), C G → C H
152/-- A finite-group class is closed under taking normal subgroups. -/
153def NormalSubgroupClosed (C : FiniteGroupClass.{u}) : Prop :=
154 ∀ {G : Type u} [Group G] (N : Subgroup G) [N.Normal], C G → C N
156/-- The finite group class is closed under quotients. -/
157def QuotientClosed (C : FiniteGroupClass.{u}) : Prop :=
158 ∀ {G : Type u} [Group G] (N : Subgroup G) [N.Normal], C G → C (G ⧸ N)
160/-- Closed under forming finite direct products. -/
161def FiniteProductClosed (C : FiniteGroupClass.{u}) : Prop :=
162 ∀ {ι : Type u} [Fintype ι] {G : ι → Type u} [∀ i, Group (G i)],
163 (∀ i, C (G i)) → C (∀ i, G i)
165/--
166Closed under forming finite subdirect products. We package a finite subdirect product as an
167injective homomorphism into a finite product whose coordinate maps are all surjective.
168-/
169def FiniteSubdirectProductClosed (C : FiniteGroupClass.{u}) : Prop :=
170 ∀ {ι : Type u} [Fintype ι] {G : Type u} [Group G]
171 {H : ι → Type u} [∀ i, Group (H i)],
172 (f : G →* ∀ i, H i) →
173 Function.Injective f →
174 (∀ i, Function.Surjective fun g : G => f g i) →
175 (∀ i, C (H i)) →
176 C G
178/-- The finite group class is closed under extensions. -/
179def ExtensionClosed (C : FiniteGroupClass.{u}) : Prop :=
180 ∀ {E : Type u} [Group E] (N : Subgroup E) [N.Normal],
181 C N → C (E ⧸ N) → C E
183/--
184A formation is a family of finite groups closed under quotients and finite fiber or subdirect
185products; the empty finite subdirect product supplies membership of the trivial group.
186-/
187structure Formation (C : FiniteGroupClass.{u}) : Prop where
188 /-- Membership in `C` descends to quotients by arbitrary normal subgroups. -/
189 quotientClosed : QuotientClosed C
190 /--
191 A finite group belongs to `C` when it embeds as a subdirect product of finitely many members
192 of `C`.
193 -/
194 finiteSubdirectProductClosed : FiniteSubdirectProductClosed C
196/-- A variety of finite groups. -/
197structure Variety (C : FiniteGroupClass.{u}) : Prop where
198 /-- Membership in `C` descends to subgroups. -/
199 subgroupClosed : SubgroupClosed C
200 /-- Membership in `C` descends to quotients by normal subgroups. -/
201 quotientClosed : QuotientClosed C
202 /-- Finite direct products of members of `C` again belong to `C`. -/
203 finiteProductClosed : FiniteProductClosed C
205/--
206A Melnikov formation includes the underlying formation data directly, so the standard
207formulation, including unit membership, is immediately available.
208-/
209structure MelnikovFormation (C : FiniteGroupClass.{u}) : Prop where
210 /-- The quotient and finite-subdirect-product closure axioms of the underlying formation. -/
211 formation : Formation C
212 /-- Normal subgroups of members of `C` again belong to `C`. -/
213 normalSubgroupClosed : NormalSubgroupClosed C
214 /--
215 A finite group belongs to `C` whenever a normal subgroup and the corresponding quotient both
216 belong to `C`.
217 -/
218 extensionClosed : ExtensionClosed C
220/--
221A finite-group class is hereditary when it is closed under injective homomorphisms. This is the
222form used by finite-quotient comap constructions: a pullback quotient embeds into the target
223finite quotient, so membership descends along injections.
224-/
225structure Hereditary (C : FiniteGroupClass.{u}) : Prop where
226 /--
227 Membership pulls back along injective homomorphisms: a group embedded in a member of `C`
228 itself belongs to `C`.
229 -/
230 of_injective :
231 ∀ {G H : Type u} [Group G] [Group H],
232 C H → (f : G →* H) → Function.Injective f → C G
234/--
235A full formation of finite groups. Equivalently, this is a Melnikov formation whose finite
236groups are closed under subgroups. The \(Hereditary\) injective-hom formulation is derived as
237FullFormation.hereditary.
238-/
239structure FullFormation (C : FiniteGroupClass.{u}) : Prop where
240 /--
241 The formation, normal-subgroup, and extension closure data supplied by a Melnikov formation.
242 -/
243 melnikovFormation : MelnikovFormation C
244 /-- Arbitrary subgroups of members of `C` again belong to `C`. -/
245 subgroupClosed : SubgroupClosed C
247/-- A formation is closed under isomorphism. -/
248theorem Formation.isomClosed {C : FiniteGroupClass.{u}} (_hForm : Formation C) :
249 IsomClosed C :=
250 C.isomClosed
252/-- Every formation is closed under finite direct products. -/
253theorem Formation.finiteProductClosed {C : FiniteGroupClass.{u}}
254 (hForm : Formation C) : FiniteProductClosed C := by
255 classical
256 intro ι _ G _ hG
257 let f : (∀ i, G i) →* ∀ i, G i := MonoidHom.id _
258 refine hForm.finiteSubdirectProductClosed f ?_ ?_ hG
259 · intro x y hxy
260 simpa [f] using hxy
261 · intro i y
262 refine ⟨Function.update 1 i y, ?_⟩
263 simp only [MonoidHom.id_apply, Function.update_self, f]
265/--
266Every formation contains the trivial group. This is the standard trivial-object clause. In this
267version it is derived from the empty finite subdirect product, so no separate hypothesis
268asserting that the trivial group belongs to the class is needed.
269-/
270theorem Formation.one_mem {C : FiniteGroupClass.{u}} (hForm : Formation C) :
271 C PUnit := by
272 let G : PEmpty → Type u := fun _ => PUnit
273 letI : ∀ i : PEmpty, Group (G i) := by
274 intro i
275 cases i
276 let e : ((i : PEmpty) → G i) ≃* PUnit := by
277 refine
278 { toFun := fun _ => PUnit.unit
279 invFun := fun _ i => nomatch i
280 left_inv := ?_
281 right_inv := ?_
282 map_mul' := ?_ }
283 · intro x
284 ext i
285 · intro x
286 cases x
287 rfl
288 · intro x y
289 rfl
290 have hProd : C ((i : PEmpty) → G i) :=
291 hForm.finiteProductClosed (ι := PEmpty) (G := G) (fun i => by cases i)
292 exact hForm.isomClosed ⟨e⟩ hProd
294/--
295Use a specified multiplicative equivalence to transport membership in an isomorphism-closed
296finite-group class.
297-/
298theorem IsomClosed.of_mulEquiv {C : FiniteGroupClass.{u}}
299 (hIso : IsomClosed C) {G H : Type u} [Group G] [Group H]
300 (e : G ≃* H) (hG : C G) :
301 C H :=
302 hIso ⟨e⟩ hG
304/--
305Membership in an isomorphism-closed finite-group class is invariant under a specified
306multiplicative equivalence.
307-/
308theorem IsomClosed.iff_of_mulEquiv {C : FiniteGroupClass.{u}}
309 (hIso : IsomClosed C) {G H : Type u} [Group G] [Group H]
310 (e : G ≃* H) :
311 C G ↔ C H :=
312 ⟨hIso.of_mulEquiv e, hIso.of_mulEquiv e.symm⟩
314/-- An isomorphism-closed class containing the trivial group contains every trivial group. -/
315theorem containsTrivialQuotients_of_isomClosed_one_mem {C : FiniteGroupClass.{u}}
316 (hIso : IsomClosed C) (hOne : C PUnit) :
317 ContainsTrivialQuotients C := by
318 refine ⟨?_⟩
319 intro Q _ hQ
320 letI : Subsingleton Q := hQ
321 let e : PUnit ≃* Q :=
322 { toFun := fun _ => 1
323 invFun := fun _ => PUnit.unit
324 left_inv := by
325 intro x
326 cases x
327 rfl
328 right_inv := by
329 intro q
330 exact Subsingleton.elim _ _
331 map_mul' := by
332 intro x y
333 exact Subsingleton.elim _ _ }
334 exact hIso ⟨e⟩ hOne
336/-- A formation contains the trivial quotients required by the pro-\(C\) construction. -/
337theorem Formation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
338 (hForm : Formation C) :
339 ContainsTrivialQuotients C :=
340 containsTrivialQuotients_of_isomClosed_one_mem hForm.isomClosed hForm.one_mem
342/--
343Any isomorphism-closed subgroup-closed class that is closed under finite direct products is also
344closed under finite subdirect products.
345-/
346theorem finiteSubdirectProductClosed_of_isomClosed_subgroupClosed_finiteProductClosed
347 {C : FiniteGroupClass.{u}}
348 (hIso : IsomClosed C)
349 (hSub : SubgroupClosed C)
350 (hProd : FiniteProductClosed C) :
351 FiniteSubdirectProductClosed C := by
352 intro ι _ G _ H _ f hf _hsurj hH
353 have hPi : C (∀ i, H i) := hProd hH
354 have hRange : C f.range := hSub f.range hPi
355 have hRangeRestrictInj : Function.Injective f.rangeRestrict := by
356 intro x y hxy
357 exact hf (by simpa using congrArg Subtype.val hxy)
358 let e : G ≃* f.range := MulEquiv.ofBijective f.rangeRestrict
359 ⟨hRangeRestrictInj, f.rangeRestrict_surjective⟩
360 exact hIso ⟨e.symm⟩ hRange
362/-- An isomorphism-closed variety contains the trivial group. -/
363theorem variety_one_mem_of_isomClosed {C : FiniteGroupClass.{u}}
364 (hVar : Variety C) (hIso : IsomClosed C) :
365 C PUnit := by
366 let G : PEmpty → Type u := fun _ => PUnit
367 letI : ∀ i : PEmpty, Group (G i) := by
368 intro i
369 cases i
370 let e : ((i : PEmpty) → G i) ≃* PUnit := by
371 classical
372 refine
373 { toFun := fun _ => PUnit.unit
374 invFun := fun _ i => nomatch i
375 left_inv := ?_
376 right_inv := ?_
377 map_mul' := ?_ }
378 · intro x
379 ext i
380 · intro x
381 cases x
382 rfl
383 · intro x y
384 rfl
385 have hProd : C ((i : PEmpty) → G i) :=
386 hVar.finiteProductClosed (ι := PEmpty) (G := G) (fun i => by cases i)
387 exact hIso ⟨e⟩ hProd
389/--
390Any subgroup-closed, isomorphism-closed class that contains at least one group also contains the
391trivial group.
392-/
393theorem one_mem_of_subgroupClosed_isomClosed {C : FiniteGroupClass.{u}}
394 (hSub : SubgroupClosed C) (hIso : IsomClosed C)
395 {G : Type u} [Group G] (hG : C G) :
396 C PUnit := by
397 let eBot : (⊥ : Subgroup G) ≃* PUnit :=
398 { toFun := fun _ => PUnit.unit
399 invFun := fun _ => 1
400 left_inv := by
401 intro x
402 exact Subsingleton.elim _ _
403 right_inv := by
404 intro x
405 cases x
406 rfl
407 map_mul' := by
408 intro x y
409 rfl }
410 exact hIso ⟨eBot⟩ (hSub (⊥ : Subgroup G) hG)
412/-- Subgroup- and isomorphism-closure imply the injective-hom hereditary form. -/
413theorem Hereditary.of_subgroupClosed_isomClosed {C : FiniteGroupClass.{u}}
414 (hSub : SubgroupClosed C) (hIso : IsomClosed C) :
415 Hereditary C := by
416 refine ⟨?_⟩
417 intro G H _ _ hH f hf
418 have hRange : C f.range := hSub f.range hH
419 let e : G ≃* f.range := MulEquiv.ofBijective f.rangeRestrict
420 ⟨by
421 intro x y hxy
422 exact hf (by simpa using congrArg Subtype.val hxy),
423 f.rangeRestrict_surjective⟩
424 exact hIso ⟨e.symm⟩ hRange
426/-- The finite group class is closed under taking subgroups. -/
427theorem Hereditary.subgroupClosed {C : FiniteGroupClass.{u}}
428 (hHer : Hereditary C) :
429 SubgroupClosed C := by
430 intro G _ H hG
431 exact hHer.of_injective hG H.subtype Subtype.val_injective
433/--
434Use a specified multiplicative equivalence to transport membership in an isomorphism-closed
435finite-group class.
436-/
437theorem Hereditary.of_mulEquiv {C : FiniteGroupClass.{u}}
438 (hHer : Hereditary C) {G H : Type u} [Group G] [Group H]
439 (e : G ≃* H) (hH : C H) :
440 C G :=
441 hHer.of_injective hH e.toMonoidHom e.injective
443/--
444Membership in an isomorphism-closed finite-group class is invariant under a specified
445multiplicative equivalence.
446-/
447theorem Hereditary.iff_of_mulEquiv {C : FiniteGroupClass.{u}}
448 (hHer : Hereditary C) {G H : Type u} [Group G] [Group H]
449 (e : G ≃* H) :
450 C G ↔ C H :=
451 ⟨fun hG => hHer.of_mulEquiv e.symm hG, fun hH => hHer.of_mulEquiv e hH⟩
453/-- A Melnikov formation is closed under quotients. -/
454theorem MelnikovFormation.quotientClosed {C : FiniteGroupClass.{u}}
455 (hC : MelnikovFormation C) : QuotientClosed C :=
456 hC.formation.quotientClosed
458/--
459Every formation contains the trivial group. This is the standard trivial-object clause. In this
460version it is derived from the empty finite subdirect product, so no separate hypothesis
461asserting that the trivial group belongs to the class is needed.
462-/
463theorem MelnikovFormation.one_mem {C : FiniteGroupClass.{u}}
464 (hC : MelnikovFormation C) : C PUnit :=
465 hC.formation.one_mem
467/-- A Melnikov formation contains the trivial quotients. -/
468theorem MelnikovFormation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
469 (hC : MelnikovFormation C) :
470 ContainsTrivialQuotients C :=
471 hC.formation.containsTrivialQuotients
473/-- A Melnikov formation is closed under isomorphism. -/
474theorem MelnikovFormation.isomClosed {C : FiniteGroupClass.{u}}
475 (hC : MelnikovFormation C) : IsomClosed C :=
476 hC.formation.isomClosed
479/-- A full formation is closed under quotients. -/
480theorem FullFormation.quotientClosed {C : FiniteGroupClass.{u}}
481 (hC : FullFormation C) : QuotientClosed C :=
482 hC.melnikovFormation.quotientClosed
484/--
485Every formation contains the trivial group. This is the standard trivial-object clause. In this
486version it is derived from the empty finite subdirect product, so no separate hypothesis
487asserting that the trivial group belongs to the class is needed.
488-/
489theorem FullFormation.one_mem {C : FiniteGroupClass.{u}}
490 (hC : FullFormation C) : C PUnit :=
491 hC.melnikovFormation.one_mem
493/-- A full formation contains the trivial quotients. -/
494theorem FullFormation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
495 (hC : FullFormation C) :
496 ContainsTrivialQuotients C :=
497 hC.melnikovFormation.containsTrivialQuotients
499/-- A full formation is closed under isomorphism. -/
500theorem FullFormation.isomClosed {C : FiniteGroupClass.{u}}
501 (hC : FullFormation C) : IsomClosed C :=
502 hC.melnikovFormation.isomClosed
505/-- A full formation is closed under normal subgroups. -/
506theorem FullFormation.normalSubgroupClosed {C : FiniteGroupClass.{u}}
507 (hC : FullFormation C) : NormalSubgroupClosed C :=
508 hC.melnikovFormation.normalSubgroupClosed
510/-- A formation is closed under extensions. -/
511theorem FullFormation.extensionClosed {C : FiniteGroupClass.{u}}
512 (hC : FullFormation C) : ExtensionClosed C :=
513 hC.melnikovFormation.extensionClosed
515/--
516The subgroup-closed part of a full formation, in the injective-hom form used by finite quotient
517pullbacks.
518-/
519theorem FullFormation.hereditary {C : FiniteGroupClass.{u}}
520 (hC : FullFormation C) : Hereditary C :=
521 Hereditary.of_subgroupClosed_isomClosed hC.subgroupClosed hC.isomClosed
523/-- An isomorphism-closed variety is a formation in the unbundled FiniteGroupClass formulation. -/
524theorem variety_formation {C : FiniteGroupClass.{u}}
525 (hVar : Variety C) (hIso : IsomClosed C) :
526 Formation C := by
527 refine ⟨hVar.quotientClosed, ?_⟩
528 exact finiteSubdirectProductClosed_of_isomClosed_subgroupClosed_finiteProductClosed
529 hIso hVar.subgroupClosed hVar.finiteProductClosed
531/--
532A variety together with extension-closure packages the standard finite-class closure hypotheses
533used by the pro-\(C\) formulation.
534-/
535theorem Variety.closureBundle_of_isomClosed_extensionClosed {C : FiniteGroupClass.{u}}
536 (hVar : Variety C)
537 (hIso : IsomClosed C)
538 (hExt : ExtensionClosed C) :
539 Formation C ∧ SubgroupClosed C ∧ IsomClosed C ∧ QuotientClosed C ∧ ExtensionClosed C := by
540 exact ⟨variety_formation hVar hIso, hVar.subgroupClosed, hIso, hVar.quotientClosed, hExt⟩
542/--
543For a Melnikov formation, the quotients by two normal subgroups lying in the class force the
544quotient by their intersection to lie in the class as well.
545-/
546theorem MelnikovFormation.quotient_inf_mem {C : FiniteGroupClass.{u}}
547 (hC : MelnikovFormation C)
548 {G : Type u} [Group G]
549 (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal]
550 (h₁ : C (G ⧸ N₁)) (h₂ : C (G ⧸ N₂)) :
551 C (G ⧸ (N₁ ⊓ N₂)) := by
552 let E : Type u := G ⧸ (N₁ ⊓ N₂)
553 let L : Subgroup E := Subgroup.map (QuotientGroup.mk' (N₁ ⊓ N₂)) N₁
554 letI : L.Normal := by
555 dsimp [L]
556 exact Subgroup.Normal.map (show N₁.Normal by infer_instance)
557 (QuotientGroup.mk' (N₁ ⊓ N₂))
558 (QuotientGroup.mk'_surjective (N₁ ⊓ N₂))
559 have hQuotL : C (E ⧸ L) := by
560 let e : E ⧸ L ≃* G ⧸ N₁ :=
561 QuotientGroup.quotientQuotientEquivQuotient (N₁ ⊓ N₂) N₁ inf_le_left
562 exact hC.isomClosed ⟨e.symm⟩ h₁
563 let K₂ : Subgroup (G ⧸ N₂) := Subgroup.map (QuotientGroup.mk' N₂) N₁
564 letI : K₂.Normal := by
565 dsimp [K₂]
566 exact Subgroup.Normal.map (show N₁.Normal by infer_instance)
567 (QuotientGroup.mk' N₂)
568 (QuotientGroup.mk'_surjective N₂)
569 have hK₂ : C K₂ := hC.normalSubgroupClosed K₂ h₂
570 let ψ₂ : N₁ →* G ⧸ N₂ := (QuotientGroup.mk' N₂).comp N₁.subtype
571 have hψ₂range : ψ₂.range = K₂ := by
572 ext x
573 constructor
574 · rintro ⟨y, rfl⟩
575 exact ⟨y.1, y.2, rfl⟩
576 · rintro ⟨y, hy, rfl⟩
577 exact ⟨⟨y, hy⟩, rfl⟩
578 have hψ₂ker : ψ₂.ker = N₂.subgroupOf N₁ := by
579 ext x
580 change QuotientGroup.mk' N₂ x.1 = 1 ↔ x.1 ∈ N₂
581 simp only [QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff (N := N₂) x.1]
582 have hQuotN₁ : C (N₁ ⧸ N₂.subgroupOf N₁) := by
583 let e₀ : N₁ ⧸ N₂.subgroupOf N₁ ≃* N₁ ⧸ ψ₂.ker :=
584 QuotientGroup.quotientMulEquivOfEq hψ₂ker.symm
585 let e₁ : N₁ ⧸ ψ₂.ker ≃* ψ₂.range := QuotientGroup.quotientKerEquivRange ψ₂
586 let e₂ : ψ₂.range ≃* K₂ := MulEquiv.subgroupCongr hψ₂range
587 exact hC.isomClosed ⟨((e₀.trans e₁).trans e₂).symm⟩ hK₂
588 let ψ₁ : N₁ →* E := (QuotientGroup.mk' (N₁ ⊓ N₂)).comp N₁.subtype
589 have hψ₁range : ψ₁.range = L := by
590 ext x
591 constructor
592 · rintro ⟨y, rfl⟩
593 exact ⟨y.1, y.2, rfl⟩
594 · rintro ⟨y, hy, rfl⟩
595 exact ⟨⟨y, hy⟩, rfl⟩
596 have hψ₁ker : ψ₁.ker = N₂.subgroupOf N₁ := by
597 ext x
598 change QuotientGroup.mk' (N₁ ⊓ N₂) x.1 = 1 ↔ x.1 ∈ N₂
599 constructor
600 · intro hx
601 exact (QuotientGroup.eq_one_iff (N := N₁ ⊓ N₂) x.1).1 hx |>.2
602 · intro hx
603 exact (QuotientGroup.eq_one_iff (N := N₁ ⊓ N₂) x.1).2 ⟨x.2, hx⟩
604 have hL : C L := by
605 let e₀ : N₁ ⧸ N₂.subgroupOf N₁ ≃* N₁ ⧸ ψ₁.ker :=
606 QuotientGroup.quotientMulEquivOfEq hψ₁ker.symm
607 let e₁ : N₁ ⧸ ψ₁.ker ≃* ψ₁.range := QuotientGroup.quotientKerEquivRange ψ₁
608 let e₂ : ψ₁.range ≃* L := MulEquiv.subgroupCongr hψ₁range
609 exact hC.isomClosed ⟨(e₀.trans e₁).trans e₂⟩ hQuotN₁
610 exact hC.extensionClosed L hL hQuotL
612/-- A Melnikov formation with subgroup closure gives the standard finite-class closure bundle. -/
613theorem MelnikovFormation.closureBundle_of_subgroupClosed {C : FiniteGroupClass.{u}}
614 (hC : MelnikovFormation C)
615 (hSub : SubgroupClosed C) :
616 Formation C ∧ SubgroupClosed C ∧ IsomClosed C ∧ QuotientClosed C ∧ ExtensionClosed C := by
617 exact ⟨hC.formation, hSub, hC.isomClosed, hC.quotientClosed, hC.extensionClosed⟩
619/--
620For a formation, the quotient by the intersection of two normal subgroups whose individual
621quotients lie in \(C\) also lies in \(C\). This is the two-factor form of (C4).
622-/
623theorem Formation.quotient_inf_mem {C : FiniteGroupClass.{u}}
624 (hC : Formation C) {G : Type u} [Group G]
625 (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal]
626 (h₁ : C (G ⧸ N₁)) (h₂ : C (G ⧸ N₂)) :
627 C (G ⧸ (N₁ ⊓ N₂)) := by
628 classical
629 let H : ULift Bool → Type u
630 | ⟨false⟩ => G ⧸ N₁
631 | ⟨true⟩ => G ⧸ N₂
632 letI : ∀ b : ULift Bool, Group (H b) := by
633 intro b
634 cases b with
635 | up b =>
636 cases b <;> infer_instance
637 let f : G ⧸ (N₁ ⊓ N₂) →* ∀ b : ULift Bool, H b :=
638 { toFun := fun x b =>
639 match b with
640 | ⟨false⟩ => QuotientGroup.map (N₁ ⊓ N₂) N₁ (MonoidHom.id G) inf_le_left x
641 | ⟨true⟩ => QuotientGroup.map (N₁ ⊓ N₂) N₂ (MonoidHom.id G) inf_le_right x
642 map_one' := by
643 funext b
644 cases b with
645 | up b =>
646 cases b <;> rfl
647 map_mul' := by
648 intro x y
649 funext b
650 cases b with
651 | up b =>
652 cases b with
653 | false =>
654 exact (QuotientGroup.map (N₁ ⊓ N₂) N₁ (MonoidHom.id G) inf_le_left).map_mul x y
655 | true =>
656 exact (QuotientGroup.map (N₁ ⊓ N₂) N₂ (MonoidHom.id G) inf_le_right).map_mul x y }
657 refine hC.finiteSubdirectProductClosed (ι := ULift Bool) (H := H) f ?_ ?_ ?_
658 · intro x y hxy
659 rcases QuotientGroup.mk'_surjective (N₁ ⊓ N₂) x with ⟨gx, rfl⟩
660 rcases QuotientGroup.mk'_surjective (N₁ ⊓ N₂) y with ⟨gy, rfl⟩
661 apply QuotientGroup.eq.2
662 constructor
663 · have hfalse :
664 f (QuotientGroup.mk' (N₁ ⊓ N₂) gx) ⟨false⟩ =
665 f (QuotientGroup.mk' (N₁ ⊓ N₂) gy) ⟨false⟩ :=
666 congrArg (fun z : ∀ b : ULift Bool, H b => z ⟨false⟩) hxy
667 exact QuotientGroup.eq.1 (by simpa [f, H] using hfalse)
668 · have htrue :
669 f (QuotientGroup.mk' (N₁ ⊓ N₂) gx) ⟨true⟩ =
670 f (QuotientGroup.mk' (N₁ ⊓ N₂) gy) ⟨true⟩ :=
671 congrArg (fun z : ∀ b : ULift Bool, H b => z ⟨true⟩) hxy
672 exact QuotientGroup.eq.1 (by simpa [f, H] using htrue)
673 · intro b
674 cases b with
675 | up b =>
676 cases b with
677 | false =>
678 intro x
679 rcases QuotientGroup.mk'_surjective N₁ x with ⟨g, rfl⟩
680 refine ⟨QuotientGroup.mk' (N₁ ⊓ N₂) g, ?_⟩
681 simp only [QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk,
682 QuotientGroup.map_mk, MonoidHom.id_apply,
683 H, f]
684 | true =>
685 intro x
686 rcases QuotientGroup.mk'_surjective N₂ x with ⟨g, rfl⟩
687 refine ⟨QuotientGroup.mk' (N₁ ⊓ N₂) g, ?_⟩
688 simp only [QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk,
689 QuotientGroup.map_mk, MonoidHom.id_apply,
690 H, f]
691 · intro b
692 cases b with
693 | up b =>
694 cases b with
695 | false =>
696 simpa [H] using h₁
697 | true =>
698 simpa [H] using h₂
700end FiniteGroupClass
702end ProCGroups