import
- Mathlib.GroupTheory.QuotientGroup.Finite
- ProCGroups.FiniteGroups.Classes
def allFinite : FiniteGroupClass.{u} where
pred := fun G [_] => Finite G
finite_of_mem := fun hG => hGThe class of all finite groups.
Show proof
by
refine ⟨?_, ?_⟩
· intro G _ N _ hG
letI : Finite G := hG
exact Finite.of_surjective (QuotientGroup.mk' N) (QuotientGroup.mk'_surjective N)
· intro ι _ G _ H _ f hf _ hH
letI : ∀ i, Finite (H i) := hH
letI : Finite ((i : ι) → H i) := inferInstance
exact Finite.of_injective f hfProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□instance allFinite_containsTrivialQuotients :
ContainsTrivialQuotients (allFinite : FiniteGroupClass.{u}) :=
allFinite_formation.containsTrivialQuotientsThe class of all finite groups contains the trivial quotients.
theorem allFinite_isomClosed : IsomClosed allFiniteThe class of all finite groups is closed under isomorphism.
Show proof
by
intro G H _ _ hGH hG
rcases hGH with ⟨e⟩
letI : Finite G := hG
exact Finite.of_equiv G e.toEquivProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem allFinite_subgroupClosed : SubgroupClosed allFiniteThe class of all finite groups is closed under subgroups.
Show proof
by
intro G _ H hG
letI : Finite G := hG
exact Finite.of_injective H.subtype Subtype.val_injectiveProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem allFinite_normalSubgroupClosed : NormalSubgroupClosed allFiniteThe class of all finite groups is closed under normal subgroups.
Show proof
by
intro G _ N _ hG
exact allFinite_subgroupClosed N hGProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem allFinite_quotientClosed : QuotientClosed allFiniteThe class of all finite groups is closed under quotients.
Show proof
allFinite_formation.quotientClosedProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem allFinite_finiteSubdirectProductClosed : FiniteSubdirectProductClosed allFiniteShow proof
allFinite_formation.finiteSubdirectProductClosedProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem allFinite_extensionClosed : ExtensionClosed allFiniteShow proof
by
intro E _ N _ hN hQ
letI : Finite N := hN
letI : Finite (E ⧸ N) := hQ
exact Finite.of_subgroup_quotient NProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem allFinite_hereditary : Hereditary allFiniteThe class of all finite groups is hereditary.
Show proof
by
refine ⟨?_⟩
intro G H _ _ hH f hf
letI : Finite H := hH
exact Finite.of_injective f hfProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□