Source: ProCGroups.FiniteGroups.AllFinite
1import Mathlib.GroupTheory.QuotientGroup.Finite
2import ProCGroups.FiniteGroups.Classes
4/-!
5# The class of all finite groups
7This module defines `FiniteGroupClass.allFinite` and proves its standard closure properties:
8formation, subgroup, normal-subgroup, quotient, finite-subdirect-product, extension, and
9hereditary closure. It also supplies the trivial-quotient instance used by pro-\(C\)
10constructions when no restriction beyond finiteness is intended.
11-/
13namespace ProCGroups
15universe u
17namespace FiniteGroupClass
19/-- The class of all finite groups. -/
20def allFinite : FiniteGroupClass.{u} where
21 pred := fun G [_] => Finite G
22 finite_of_mem := fun hG => hG
23 mem_of_mulEquiv := by
24 intro G H _ _ e hG
25 letI : Finite G := hG
26 exact Finite.of_equiv G e.toEquiv
28/-- The class of all finite groups is an extension-closed formation. -/
29theorem allFinite_formation : Formation allFinite := by
30 refine ⟨?_, ?_⟩
31 · intro G _ N _ hG
32 letI : Finite G := hG
33 exact Finite.of_surjective (QuotientGroup.mk' N) (QuotientGroup.mk'_surjective N)
34 · intro ι _ G _ H _ f hf _ hH
35 letI : ∀ i, Finite (H i) := hH
36 letI : Finite ((i : ι) → H i) := inferInstance
37 exact Finite.of_injective f hf
39/-- The class of all finite groups contains the trivial quotients. -/
40instance allFinite_containsTrivialQuotients :
41 ContainsTrivialQuotients (allFinite : FiniteGroupClass.{u}) :=
42 allFinite_formation.containsTrivialQuotients
44/-- The class of all finite groups is closed under isomorphism. -/
45theorem allFinite_isomClosed : IsomClosed allFinite := by
46 exact allFinite.isomClosed
48/-- The class of all finite groups is closed under subgroups. -/
49theorem allFinite_subgroupClosed : SubgroupClosed allFinite := by
50 intro G _ H hG
51 letI : Finite G := hG
52 exact Finite.of_injective H.subtype Subtype.val_injective
54/-- The class of all finite groups is closed under normal subgroups. -/
55theorem allFinite_normalSubgroupClosed : NormalSubgroupClosed allFinite := by
56 intro G _ N _ hG
57 exact allFinite_subgroupClosed N hG
59/-- The class of all finite groups is closed under quotients. -/
60theorem allFinite_quotientClosed : QuotientClosed allFinite :=
61 allFinite_formation.quotientClosed
63/-- The class of all finite groups is closed under finite subdirect products. -/
64theorem allFinite_finiteSubdirectProductClosed : FiniteSubdirectProductClosed allFinite :=
65 allFinite_formation.finiteSubdirectProductClosed
67/-- The class of all finite groups is extension closed. -/
68theorem allFinite_extensionClosed : ExtensionClosed allFinite := by
69 intro E _ N _ hN hQ
70 letI : Finite N := hN
71 letI : Finite (E ⧸ N) := hQ
72 exact Finite.of_subgroup_quotient N
74/-- The class of all finite groups is hereditary. -/
75theorem allFinite_hereditary : Hereditary allFinite := by
76 refine ⟨?_⟩
77 intro G H _ _ hH f hf
78 letI : Finite H := hH
79 exact Finite.of_injective f hf
81end FiniteGroupClass
83end ProCGroups