ProCGroups/FiniteGroups/AllFinite.lean
1import Mathlib.GroupTheory.QuotientGroup.Finite
2import ProCGroups.FiniteGroups.Classes
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FiniteGroups/AllFinite.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
22namespace FiniteGroupClass
24/-- The class of all finite groups. -/
26 pred := fun G [_] => Finite G
27 finite_of_mem := fun hG => hG
29/-- The class of all finite groups is an extension-closed formation. -/
30theorem allFinite_formation : Formation allFinite := by
31 refine ⟨?_, ?_⟩
32 · intro G _ N _ hG
33 letI : Finite G := hG
34 exact Finite.of_surjective (QuotientGroup.mk' N) (QuotientGroup.mk'_surjective N)
35 · intro ι _ G _ H _ f hf _ hH
36 letI : ∀ i, Finite (H i) := hH
37 letI : Finite ((i : ι) → H i) := inferInstance
38 exact Finite.of_injective f hf
40/-- The class of all finite groups contains the trivial quotients. -/
41instance allFinite_containsTrivialQuotients :
42 ContainsTrivialQuotients (allFinite : FiniteGroupClass.{u}) :=
43 allFinite_formation.containsTrivialQuotients
45/-- The class of all finite groups is closed under isomorphism. -/
46theorem allFinite_isomClosed : IsomClosed allFinite := by
47 intro G H _ _ hGH hG
48 rcases hGH with ⟨e⟩
49 letI : Finite G := hG
50 exact Finite.of_equiv G e.toEquiv
52/-- The class of all finite groups is closed under subgroups. -/
53theorem allFinite_subgroupClosed : SubgroupClosed allFinite := by
54 intro G _ H hG
55 letI : Finite G := hG
56 exact Finite.of_injective H.subtype Subtype.val_injective
58/-- The class of all finite groups is closed under normal subgroups. -/
59theorem allFinite_normalSubgroupClosed : NormalSubgroupClosed allFinite := by
60 intro G _ N _ hG
61 exact allFinite_subgroupClosed N hG
63/-- The class of all finite groups is quotient closed. -/
64theorem allFinite_quotientClosed : QuotientClosed allFinite :=
65 allFinite_formation.quotientClosed
67/-- The class of all finite groups is closed under finite subdirect products. -/
69 allFinite_formation.finiteSubdirectProductClosed
71/-- The class of all finite groups is extension closed. -/
72theorem allFinite_extensionClosed : ExtensionClosed allFinite := by
73 intro E _ N _ hN hQ
74 letI : Finite N := hN
75 letI : Finite (E ⧸ N) := hQ
76 exact Finite.of_subgroup_quotient N
78/-- The class of all finite groups is hereditary. -/
79theorem allFinite_hereditary : Hereditary allFinite := by
80 refine ⟨?_⟩
81 intro G H _ _ hH f hf
82 letI : Finite H := hH
83 exact Finite.of_injective f hf
87end ProCGroups