Yamaguchi Lean 4 Library
ProCGroups/FiniteGroups/Classes.lean
ProCGroups/FiniteGroups/Classes/Source

ProCGroups/FiniteGroups/Classes.lean

1import Mathlib.Algebra.Group.PUnit
2import Mathlib.GroupTheory.QuotientGroup.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FiniteGroups/Classes.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Finite group classes
15Defines finite group classes and their standard closure properties: quotients, finite subdirect products, subgroups, extensions, formations, and standard examples.
16-/
18namespace ProCGroups
20universe u v
22/-- A class of groups, implemented as an unbundled predicate on group carriers. -/
23abbrev GroupClass := ∀ (G : Type u) [Group G], Prop
25/-- A class of finite groups.
27The public API bundles the predicate with the proof that every member is finite. The coercion
28below keeps the usual `C G` spelling for membership. -/
29structure FiniteGroupClass where
30 pred : GroupClass.{u}
31 finite_of_mem : ∀ {G : Type u} [Group G], pred G → Finite G
33instance instCoeFunFiniteGroupClass : CoeFun FiniteGroupClass (fun _ => GroupClass.{u}) where
34 coe C := C.pred
38/-- The class only contains finite groups. -/
39def FiniteOnly (C : FiniteGroupClass.{u}) : Prop :=
40 ∀ {G : Type u} [Group G], C G → Finite G
42/-- Members of a bundled finite-group class are finite. -/
43theorem finite {C : FiniteGroupClass.{u}} {G : Type u} [Group G] (hG : C G) : Finite G :=
44 C.finite_of_mem hG
46/-- The finite-only predicate follows from the bundled class data. -/
47theorem finiteOnly (C : FiniteGroupClass.{u}) : FiniteOnly C :=
48 fun hG => C.finite hG
50/-- The finite-group class contains all trivial groups.
52This is the class-level form needed when a construction indexes over quotients and must include
53the terminal quotient. Formations provide this automatically via `Formation.one_mem`; users of a
54formation should not add a separate hypothesis. -/
55class ContainsTrivialQuotients (C : FiniteGroupClass.{u}) : Prop where
56 of_subsingleton : ∀ {Q : Type u} [Group Q], Subsingleton Q → C Q
58/-- 1 (closure under isomorphism). -/
59def IsomClosed (C : FiniteGroupClass.{u}) : Prop :=
60 ∀ {G H : Type u} [Group G] [Group H], Nonempty (G ≃* H) → C G → C H
62/-- Closed under taking subgroups. -/
63def SubgroupClosed (C : FiniteGroupClass.{u}) : Prop :=
64 ∀ {G : Type u} [Group G] (H : Subgroup G), C G → C H
66/-- Closed under taking normal subgroups. -/
67def NormalSubgroupClosed (C : FiniteGroupClass.{u}) : Prop :=
68 ∀ {G : Type u} [Group G] (N : Subgroup G) [N.Normal], C G → C N
70/-- Closed under taking quotients. -/
71def QuotientClosed (C : FiniteGroupClass.{u}) : Prop :=
72 ∀ {G : Type u} [Group G] (N : Subgroup G) [N.Normal], C G → C (G ⧸ N)
74/-- Closed under forming finite direct products. -/
75def FiniteProductClosed (C : FiniteGroupClass.{u}) : Prop :=
76 ∀ {ι : Type u} [Fintype ι] {G : ι → Type u} [∀ i, Group (G i)],
77 (∀ i, C (G i)) → C (∀ i, G i)
79/-- Closed under forming finite subdirect products.
81We package a finite subdirect product as an injective homomorphism into a finite product whose
82coordinate maps are all surjective.
83-/
84def FiniteSubdirectProductClosed (C : FiniteGroupClass.{u}) : Prop :=
85 ∀ {ι : Type u} [Fintype ι] {G : Type u} [Group G]
86 {H : ι → Type u} [∀ i, Group (H i)],
87 (f : G →* ∀ i, H i) →
88 Function.Injective f →
89 (∀ i, Function.Surjective fun g : G => f g i) →
90 (∀ i, C (H i)) →
91 C G
93/-- Closed under extensions. -/
94def ExtensionClosed (C : FiniteGroupClass.{u}) : Prop :=
95 ∀ {E : Type u} [Group E] (N : Subgroup E) [N.Normal],
96 C N → C (E ⧸ N) → C E
98/-- A formation of finite groups.
100Standard formation terminology starts with a family of finite groups containing the trivial group and then asks for
101closure under quotients and finite fiber/subdirect products. In this unbundled predicate API the
102trivial group condition is a theorem, `Formation.one_mem`, because it follows from the empty finite
103subdirect product. -/
104structure Formation (C : FiniteGroupClass.{u}) : Prop where
105 quotientClosed : QuotientClosed C
106 finiteSubdirectProductClosed : FiniteSubdirectProductClosed C
108/-- A variety of finite groups. -/
109structure Variety (C : FiniteGroupClass.{u}) : Prop where
111 quotientClosed : QuotientClosed C
114/-- A Melnikov formation of finite groups.
116A Melnikov formation includes the underlying formation field directly, rather than
117re-proving it at every use site, so the standard formation API (including `Formation.one_mem`) is
118available immediately. -/
119structure MelnikovFormation (C : FiniteGroupClass.{u}) : Prop where
124/-- A finite-group class is hereditary when it is closed under injective homomorphisms.
126This is the form used by finite-quotient comap constructions: a pullback quotient embeds into the
127target finite quotient, so membership descends along injections. -/
128structure Hereditary (C : FiniteGroupClass.{u}) : Prop where
130 ∀ {G H : Type u} [Group G] [Group H],
131 C H → (f : G →* H) → Function.Injective f → C G
133/-- A full formation of finite groups.
135Equivalently, this is a Melnikov formation whose finite groups are closed under subgroups. The
136`Hereditary` injective-hom formulation is derived as `FullFormation.hereditary`. -/
137structure FullFormation (C : FiniteGroupClass.{u}) : Prop where
138 melnikovFormation : MelnikovFormation C
141/-- Typeclass wrapper for a finite-group formation.
143Use this when a theorem only needs the closure package for a fixed finite class and should not
144carry a separate `hForm : Formation C` argument everywhere. -/
145class IsFormation (C : FiniteGroupClass.{u}) : Prop where
148/-- Typeclass wrapper for a Melnikov formation. -/
149class IsMelnikovFormation (C : FiniteGroupClass.{u}) : Prop where
150 melnikovFormation : MelnikovFormation C
152/-- Typeclass wrapper for a full formation. -/
153class IsFullFormation (C : FiniteGroupClass.{u}) : Prop where
154 fullFormation : FullFormation C
156/-- Bundled finite-group formation data, useful when the class itself should travel as data. -/
157structure FiniteFormation where
158 C : FiniteGroupClass.{u}
161/-- Bundled full finite-group formation data. -/
162structure FullFiniteFormation where
163 C : FiniteGroupClass.{u}
164 fullFormation : FullFormation C
166/-- A Melnikov formation typeclass supplies the underlying formation typeclass. -/
167@[instance 100]
169 (C : FiniteGroupClass.{u}) [hC : IsMelnikovFormation C] :
171 formation := hC.melnikovFormation.formation
173/-- A full formation typeclass supplies the underlying Melnikov formation typeclass. -/
174@[instance 100]
176 (C : FiniteGroupClass.{u}) [hC : IsFullFormation C] :
178 melnikovFormation := hC.fullFormation.melnikovFormation
180/-- Formation members are finite because the underlying class is bundled as finite-only. -/
181theorem Formation.finiteOnly {C : FiniteGroupClass.{u}} (_hForm : Formation C) :
183 C.finiteOnly
185/-- Variety members are finite because the underlying class is bundled as finite-only. -/
186theorem Variety.finiteOnly {C : FiniteGroupClass.{u}} (_hVar : Variety C) :
188 C.finiteOnly
190/-- Every formation is closed under isomorphisms. -/
191theorem Formation.isomClosed {C : FiniteGroupClass.{u}} (hForm : Formation C) :
192 IsomClosed C := by
193 intro G H _ _ hGH hCG
194 rcases hGH with ⟨e⟩
195 let f : H →* (PUnit → G) :=
196 { toFun := fun h _ => e.symm h
197 map_one' := by
198 ext i
199 cases i
200 simp only [map_one, Pi.one_apply]
201 map_mul' := by
202 intro x y
203 ext i
204 cases i
205 simp only [map_mul, Pi.mul_apply]}
206 have hf : Function.Injective f := by
207 intro x y hxy
208 exact e.symm.injective (by simpa [f] using congrFun hxy PUnit.unit)
209 have hsurj : ∀ i : PUnit, Function.Surjective fun h : H => f h i := by
210 intro i g
211 refine ⟨e g, ?_⟩
212 cases i
213 simp only [MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.symm_apply_apply, f]
214 exact hForm.finiteSubdirectProductClosed f hf hsurj (fun _ => hCG)
216/-- Every formation is closed under finite direct products. -/
217theorem Formation.finiteProductClosed {C : FiniteGroupClass.{u}}
218 (hForm : Formation C) : FiniteProductClosed C := by
219 classical
220 intro ι _ G _ hG
221 let f : (∀ i, G i) →* ∀ i, G i := MonoidHom.id _
222 refine hForm.finiteSubdirectProductClosed f ?_ ?_ hG
223 · intro x y hxy
224 simpa [f] using hxy
225 · intro i y
226 refine ⟨Function.update 1 i y, ?_⟩
227 simp only [MonoidHom.id_apply, Function.update_self, f]
229/-- Every formation contains the trivial group.
231This is the standard `containing the trivial group` clause. In this API it is derived from the empty
232finite subdirect product, so users should pass only `Formation C`, not a separate `C PUnit`
233hypothesis. -/
234theorem Formation.one_mem {C : FiniteGroupClass.{u}} (hForm : Formation C) :
235 C PUnit := by
236 let G : PEmpty → Type u := fun _ => PUnit
237 letI : ∀ i : PEmpty, Group (G i) := by
238 intro i
239 cases i
240 let e : ((i : PEmpty) → G i) ≃* PUnit := by
241 refine
242 { toFun := fun _ => PUnit.unit
243 invFun := fun _ i => nomatch i
244 left_inv := ?_
245 right_inv := ?_
246 map_mul' := ?_ }
247 · intro x
248 ext i
249 · intro x
250 cases x
251 rfl
252 · intro x y
253 rfl
254 have hProd : C ((i : PEmpty) → G i) :=
255 hForm.finiteProductClosed (ι := PEmpty) (G := G) (fun i => by cases i)
256 exact hForm.isomClosed ⟨e⟩ hProd
258/-- Use a specified multiplicative equivalence to transport membership in an isomorphism-closed
259finite-group class. -/
260theorem IsomClosed.of_mulEquiv {C : FiniteGroupClass.{u}}
261 (hIso : IsomClosed C) {G H : Type u} [Group G] [Group H]
262 (e : G ≃* H) (hG : C G) :
263 C H :=
264 hIso ⟨e⟩ hG
266/-- Membership in an isomorphism-closed finite-group class is invariant under a specified
267multiplicative equivalence. -/
268theorem IsomClosed.iff_of_mulEquiv {C : FiniteGroupClass.{u}}
269 (hIso : IsomClosed C) {G H : Type u} [Group G] [Group H]
270 (e : G ≃* H) :
271 C G ↔ C H :=
272 ⟨hIso.of_mulEquiv e, hIso.of_mulEquiv e.symm⟩
274/-- An isomorphism-closed class containing the trivial group contains every trivial group. -/
275theorem containsTrivialQuotients_of_isomClosed_one_mem {C : FiniteGroupClass.{u}}
276 (hIso : IsomClosed C) (hOne : C PUnit) :
278 refine ⟨?_⟩
279 intro Q _ hQ
280 letI : Subsingleton Q := hQ
281 let e : PUnit ≃* Q :=
282 { toFun := fun _ => 1
283 invFun := fun _ => PUnit.unit
284 left_inv := by
285 intro x
286 cases x
287 rfl
288 right_inv := by
289 intro q
290 exact Subsingleton.elim _ _
291 map_mul' := by
292 intro x y
293 exact Subsingleton.elim _ _ }
294 exact hIso ⟨e⟩ hOne
296/-- Every formation contains the trivial quotients. -/
297theorem Formation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
298 (hForm : Formation C) :
302/-- Any isomorphism-closed subgroup-closed class that is closed under finite direct products is
303also closed under finite subdirect products. -/
305 {C : FiniteGroupClass.{u}}
306 (hIso : IsomClosed C)
307 (hSub : SubgroupClosed C)
308 (hProd : FiniteProductClosed C) :
310 intro ι _ G _ H _ f hf _hsurj hH
311 have hPi : C (∀ i, H i) := hProd hH
312 have hRange : C f.range := hSub f.range hPi
313 have hRangeRestrictInj : Function.Injective f.rangeRestrict := by
314 intro x y hxy
315 exact hf (by simpa using congrArg Subtype.val hxy)
316 let e : G ≃* f.range := MulEquiv.ofBijective f.rangeRestrict
317 ⟨hRangeRestrictInj, f.rangeRestrict_surjective⟩
318 exact hIso ⟨e.symm⟩ hRange
320/-- An isomorphism-closed variety contains the trivial group. -/
321theorem variety_one_mem_of_isomClosed {C : FiniteGroupClass.{u}}
322 (hVar : Variety C) (hIso : IsomClosed C) :
323 C PUnit := by
324 let G : PEmpty → Type u := fun _ => PUnit
325 letI : ∀ i : PEmpty, Group (G i) := by
326 intro i
327 cases i
328 let e : ((i : PEmpty) → G i) ≃* PUnit := by
329 classical
330 refine
331 { toFun := fun _ => PUnit.unit
332 invFun := fun _ i => nomatch i
333 left_inv := ?_
334 right_inv := ?_
335 map_mul' := ?_ }
336 · intro x
337 ext i
338 · intro x
339 cases x
340 rfl
341 · intro x y
342 rfl
343 have hProd : C ((i : PEmpty) → G i) :=
344 hVar.finiteProductClosed (ι := PEmpty) (G := G) (fun i => by cases i)
345 exact hIso ⟨e⟩ hProd
347/-- Any subgroup-closed isomorphism-closed class that contains one group also contains the trivial
348group. -/
349theorem one_mem_of_subgroupClosed_isomClosed {C : FiniteGroupClass.{u}}
350 (hSub : SubgroupClosed C) (hIso : IsomClosed C)
351 {G : Type u} [Group G] (hG : C G) :
352 C PUnit := by
353 let eBot : (⊥ : Subgroup G) ≃* PUnit :=
354 { toFun := fun _ => PUnit.unit
355 invFun := fun _ => 1
356 left_inv := by
357 intro x
358 exact Subsingleton.elim _ _
359 right_inv := by
360 intro x
361 cases x
362 rfl
363 map_mul' := by
364 intro x y
365 rfl }
366 exact hIso ⟨eBot⟩ (hSub (⊥ : Subgroup G) hG)
368/-- Subgroup- and isomorphism-closure imply the injective-hom hereditary form. -/
369theorem Hereditary.of_subgroupClosed_isomClosed {C : FiniteGroupClass.{u}}
370 (hSub : SubgroupClosed C) (hIso : IsomClosed C) :
371 Hereditary C := by
372 refine ⟨?_⟩
373 intro G H _ _ hH f hf
374 have hRange : C f.range := hSub f.range hH
375 let e : G ≃* f.range := MulEquiv.ofBijective f.rangeRestrict
376 ⟨by
377 intro x y hxy
378 exact hf (by simpa using congrArg Subtype.val hxy),
379 f.rangeRestrict_surjective⟩
380 exact hIso ⟨e.symm⟩ hRange
382/-- Hereditary classes are subgroup-closed. -/
383theorem Hereditary.subgroupClosed {C : FiniteGroupClass.{u}}
384 (hHer : Hereditary C) :
386 intro G _ H hG
387 exact hHer.of_injective hG H.subtype Subtype.val_injective
389/-- Hereditary finite-group classes are invariant under multiplicative equivalence. -/
390theorem Hereditary.of_mulEquiv {C : FiniteGroupClass.{u}}
391 (hHer : Hereditary C) {G H : Type u} [Group G] [Group H]
392 (e : G ≃* H) (hH : C H) :
393 C G :=
394 hHer.of_injective hH e.toMonoidHom e.injective
396/-- Membership in a hereditary finite-group class is invariant under a specified multiplicative
397equivalence. -/
398theorem Hereditary.iff_of_mulEquiv {C : FiniteGroupClass.{u}}
399 (hHer : Hereditary C) {G H : Type u} [Group G] [Group H]
400 (e : G ≃* H) :
401 C G ↔ C H :=
402 ⟨fun hG => hHer.of_mulEquiv e.symm hG, fun hH => hHer.of_mulEquiv e hH⟩
404/-- Members of a Melnikov formation are finite. -/
405theorem MelnikovFormation.finiteOnly {C : FiniteGroupClass.{u}}
407 hC.formation.finiteOnly
409/-- A Melnikov formation is quotient-closed. -/
410theorem MelnikovFormation.quotientClosed {C : FiniteGroupClass.{u}}
412 hC.formation.quotientClosed
414/-- A Melnikov formation contains the trivial group. -/
415theorem MelnikovFormation.one_mem {C : FiniteGroupClass.{u}}
416 (hC : MelnikovFormation C) : C PUnit :=
417 hC.formation.one_mem
419/-- A Melnikov formation contains the trivial quotients. -/
420theorem MelnikovFormation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
423 hC.formation.containsTrivialQuotients
425/-- A Melnikov formation is isomorphism-closed. -/
426theorem MelnikovFormation.isomClosed {C : FiniteGroupClass.{u}}
428 hC.formation.isomClosed
430/-- Members of a full formation are finite. -/
431theorem FullFormation.finiteOnly {C : FiniteGroupClass.{u}}
432 (hC : FullFormation C) : FiniteOnly C :=
433 hC.melnikovFormation.finiteOnly
435/-- A full formation is quotient-closed. -/
436theorem FullFormation.quotientClosed {C : FiniteGroupClass.{u}}
438 hC.melnikovFormation.quotientClosed
440/-- A full formation contains the trivial group. -/
441theorem FullFormation.one_mem {C : FiniteGroupClass.{u}}
442 (hC : FullFormation C) : C PUnit :=
443 hC.melnikovFormation.one_mem
445/-- A full formation contains the trivial quotients. -/
446theorem FullFormation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
447 (hC : FullFormation C) :
449 hC.melnikovFormation.containsTrivialQuotients
451/-- A full formation is isomorphism-closed. -/
452theorem FullFormation.isomClosed {C : FiniteGroupClass.{u}}
453 (hC : FullFormation C) : IsomClosed C :=
454 hC.melnikovFormation.isomClosed
456/-- A full formation is closed under normal subgroups. -/
457theorem FullFormation.normalSubgroupClosed {C : FiniteGroupClass.{u}}
459 hC.melnikovFormation.normalSubgroupClosed
461/-- A full formation is extension-closed. -/
462theorem FullFormation.extensionClosed {C : FiniteGroupClass.{u}}
464 hC.melnikovFormation.extensionClosed
466/-- The subgroup-closed part of a full formation, in the injective-hom form used by finite
467quotient pullbacks. -/
468theorem FullFormation.hereditary {C : FiniteGroupClass.{u}}
469 (hC : FullFormation C) : Hereditary C :=
470 Hereditary.of_subgroupClosed_isomClosed hC.subgroupClosed hC.isomClosed
472/-- An isomorphism-closed variety is a formation in the unbundled `FiniteGroupClass` API. -/
473theorem variety_formation {C : FiniteGroupClass.{u}}
474 (hVar : Variety C) (hIso : IsomClosed C) :
475 Formation C := by
476 refine ⟨hVar.quotientClosed, ?_⟩
478 hIso hVar.subgroupClosed hVar.finiteProductClosed
480/-- A variety together with extension-closure packages the standard finite-class closure
481hypotheses used by the pro-`C` API. -/
482theorem Variety.closureBundle_of_isomClosed_extensionClosed {C : FiniteGroupClass.{u}}
483 (hVar : Variety C)
484 (hIso : IsomClosed C)
485 (hExt : ExtensionClosed C) :
487 exact ⟨variety_formation hVar hIso, hVar.subgroupClosed, hIso, hVar.quotientClosed, hExt⟩
489/-- For a Melnikov formation, the quotients by two normal subgroups lying in the
490class force the quotient by their intersection to lie in the class as well. -/
491theorem MelnikovFormation.quotient_inf_mem {C : FiniteGroupClass.{u}}
493 {G : Type u} [Group G]
494 (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal]
495 (h₁ : C (G ⧸ N₁)) (h₂ : C (G ⧸ N₂)) :
496 C (G ⧸ (N₁ ⊓ N₂)) := by
497 let E : Type u := G ⧸ (N₁ ⊓ N₂)
498 let L : Subgroup E := Subgroup.map (QuotientGroup.mk' (N₁ ⊓ N₂)) N₁
499 letI : L.Normal := by
500 dsimp [L]
501 exact Subgroup.Normal.map (show N₁.Normal by infer_instance)
502 (QuotientGroup.mk' (N₁ ⊓ N₂))
503 (QuotientGroup.mk'_surjective (N₁ ⊓ N₂))
504 have hQuotL : C (E ⧸ L) := by
505 let e : E ⧸ L ≃* G ⧸ N₁ :=
506 QuotientGroup.quotientQuotientEquivQuotient (N₁ ⊓ N₂) N₁ inf_le_left
507 exact hC.isomClosed ⟨e.symm⟩ h₁
508 let K₂ : Subgroup (G ⧸ N₂) := Subgroup.map (QuotientGroup.mk' N₂) N₁
509 letI : K₂.Normal := by
510 dsimp [K₂]
511 exact Subgroup.Normal.map (show N₁.Normal by infer_instance)
512 (QuotientGroup.mk' N₂)
513 (QuotientGroup.mk'_surjective N₂)
514 have hK₂ : C K₂ := hC.normalSubgroupClosed K₂ h₂
515 let ψ₂ : N₁ →* G ⧸ N₂ := (QuotientGroup.mk' N₂).comp N₁.subtype
516 have hψ₂range : ψ₂.range = K₂ := by
517 ext x
518 constructor
519 · rintro ⟨y, rfl⟩
520 exact ⟨y.1, y.2, rfl⟩
521 · rintro ⟨y, hy, rfl⟩
522 exact ⟨⟨y, hy⟩, rfl⟩
523 have hψ₂ker : ψ₂.ker = N₂.subgroupOf N₁ := by
524 ext x
525 change QuotientGroup.mk' N₂ x.1 = 1 ↔ x.1 ∈ N₂
526 simp only [QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff (N := N₂) x.1]
527 have hQuotN₁ : C (N₁ ⧸ N₂.subgroupOf N₁) := by
528 let e₀ : N₁ ⧸ N₂.subgroupOf N₁ ≃* N₁ ⧸ ψ₂.ker :=
529 QuotientGroup.quotientMulEquivOfEq hψ₂ker.symm
530 let e₁ : N₁ ⧸ ψ₂.ker ≃* ψ₂.range := QuotientGroup.quotientKerEquivRange ψ₂
531 let e₂ : ψ₂.range ≃* K₂ := MulEquiv.subgroupCongr hψ₂range
532 exact hC.isomClosed ⟨((e₀.trans e₁).trans e₂).symm⟩ hK₂
533 let ψ₁ : N₁ →* E := (QuotientGroup.mk' (N₁ ⊓ N₂)).comp N₁.subtype
534 have hψ₁range : ψ₁.range = L := by
535 ext x
536 constructor
537 · rintro ⟨y, rfl⟩
538 exact ⟨y.1, y.2, rfl⟩
539 · rintro ⟨y, hy, rfl⟩
540 exact ⟨⟨y, hy⟩, rfl⟩
541 have hψ₁ker : ψ₁.ker = N₂.subgroupOf N₁ := by
542 ext x
543 change QuotientGroup.mk' (N₁ ⊓ N₂) x.1 = 1 ↔ x.1 ∈ N₂
544 constructor
545 · intro hx
546 exact (QuotientGroup.eq_one_iff (N := N₁ ⊓ N₂) x.1).1 hx |>.2
547 · intro hx
548 exact (QuotientGroup.eq_one_iff (N := N₁ ⊓ N₂) x.1).2 ⟨x.2, hx⟩
549 have hL : C L := by
550 let e₀ : N₁ ⧸ N₂.subgroupOf N₁ ≃* N₁ ⧸ ψ₁.ker :=
551 QuotientGroup.quotientMulEquivOfEq hψ₁ker.symm
552 let e₁ : N₁ ⧸ ψ₁.ker ≃* ψ₁.range := QuotientGroup.quotientKerEquivRange ψ₁
553 let e₂ : ψ₁.range ≃* L := MulEquiv.subgroupCongr hψ₁range
554 exact hC.isomClosed ⟨(e₀.trans e₁).trans e₂⟩ hQuotN₁
555 exact hC.extensionClosed L hL hQuotL
557/-- A Melnikov formation with subgroup closure gives the standard finite-class closure bundle. -/
558theorem MelnikovFormation.closureBundle_of_subgroupClosed {C : FiniteGroupClass.{u}}
560 (hSub : SubgroupClosed C) :
562 exact ⟨hC.formation, hSub, hC.isomClosed, hC.quotientClosed, hC.extensionClosed⟩
564/-- For a formation, the quotient by the intersection of two normal subgroups whose
565individual quotients lie in `C` also lies in `C`. This is the two-factor form of (C4). -/
566theorem Formation.quotient_inf_mem {C : FiniteGroupClass.{u}}
567 (hC : Formation C) {G : Type u} [Group G]
568 (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal]
569 (h₁ : C (G ⧸ N₁)) (h₂ : C (G ⧸ N₂)) :
570 C (G ⧸ (N₁ ⊓ N₂)) := by
571 classical
572 let H : ULift Bool → Type u
573 | ⟨false⟩ => G ⧸ N₁
574 | ⟨true⟩ => G ⧸ N₂
575 letI : ∀ b : ULift Bool, Group (H b) := by
576 intro b
577 cases b with
578 | up b =>
579 cases b <;> infer_instance
580 let f : G ⧸ (N₁ ⊓ N₂) →* ∀ b : ULift Bool, H b :=
581 { toFun := fun x b =>
582 match b with
583 | ⟨false⟩ => QuotientGroup.map (N₁ ⊓ N₂) N₁ (MonoidHom.id G) inf_le_left x
584 | ⟨true⟩ => QuotientGroup.map (N₁ ⊓ N₂) N₂ (MonoidHom.id G) inf_le_right x
585 map_one' := by
586 funext b
587 cases b with
588 | up b =>
589 cases b <;> rfl
590 map_mul' := by
591 intro x y
592 funext b
593 cases b with
594 | up b =>
595 cases b with
596 | false =>
597 exact (QuotientGroup.map (N₁ ⊓ N₂) N₁ (MonoidHom.id G) inf_le_left).map_mul x y
598 | true =>
599 exact (QuotientGroup.map (N₁ ⊓ N₂) N₂ (MonoidHom.id G) inf_le_right).map_mul x y }
600 refine hC.finiteSubdirectProductClosed (ι := ULift Bool) (H := H) f ?_ ?_ ?_
601 · intro x y hxy
602 rcases QuotientGroup.mk'_surjective (N₁ ⊓ N₂) x with ⟨gx, rfl⟩
603 rcases QuotientGroup.mk'_surjective (N₁ ⊓ N₂) y with ⟨gy, rfl⟩
604 apply QuotientGroup.eq.2
605 constructor
606 · have hfalse :
607 f (QuotientGroup.mk' (N₁ ⊓ N₂) gx) ⟨false⟩ =
608 f (QuotientGroup.mk' (N₁ ⊓ N₂) gy) ⟨false⟩ :=
609 congrArg (fun z : ∀ b : ULift Bool, H b => z ⟨false⟩) hxy
610 exact QuotientGroup.eq.1 (by simpa [f, H] using hfalse)
611 · have htrue :
612 f (QuotientGroup.mk' (N₁ ⊓ N₂) gx) ⟨true⟩ =
613 f (QuotientGroup.mk' (N₁ ⊓ N₂) gy) ⟨true⟩ :=
614 congrArg (fun z : ∀ b : ULift Bool, H b => z ⟨true⟩) hxy
615 exact QuotientGroup.eq.1 (by simpa [f, H] using htrue)
616 · intro b
617 cases b with
618 | up b =>
619 cases b with
620 | false =>
621 intro x
622 rcases QuotientGroup.mk'_surjective N₁ x with ⟨g, rfl⟩
623 refine ⟨QuotientGroup.mk' (N₁ ⊓ N₂) g, ?_⟩
624 simp only [QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk, QuotientGroup.map_mk, MonoidHom.id_apply,
625 H, f]
626 | true =>
627 intro x
628 rcases QuotientGroup.mk'_surjective N₂ x with ⟨g, rfl⟩
629 refine ⟨QuotientGroup.mk' (N₁ ⊓ N₂) g, ?_⟩
630 simp only [QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk, QuotientGroup.map_mk, MonoidHom.id_apply,
631 H, f]
632 · intro b
633 cases b with
634 | up b =>
635 cases b with
636 | false =>
637 simpa [H] using h₁
638 | true =>
639 simpa [H] using h₂
643end ProCGroups