ProCGroups.FiniteGroups.Classes
This module studies classes for pro cgroups. A class of groups, implemented as an unbundled predicate on group carriers. A finite-group class is a predicate on group carriers together with a proof that every member is finite.
import
- Mathlib.Algebra.Group.PUnit
- Mathlib.GroupTheory.QuotientGroup.Basic
Imported by
abbrev GroupClass := ∀ (G : Type u) [Group G], PropA class of groups, implemented as an unbundled predicate on group carriers.
structure FiniteGroupClass where
pred : GroupClass.{u}
finite_of_mem : ∀ {G : Type u} [Group G], pred G → Finite GA finite-group class is a predicate on group carriers together with a proof that every member is finite.
instance instCoeFunFiniteGroupClass : CoeFun FiniteGroupClass (fun _ => GroupClass.{u}) where
coe C := C.predA finite group class coerces to its underlying predicate on finite groups.
def FiniteOnly (C : FiniteGroupClass.{u}) : Prop :=
∀ {G : Type u} [Group G], C G → Finite GThe class only contains finite groups.
theorem finite {C : FiniteGroupClass.{u}} {G : Type u} [Group G] (hG : C G) : Finite GMembers of a bundled finite-group class are finite.
Show proof
C.finite_of_mem 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 finiteOnly (C : FiniteGroupClass.{u}) : FiniteOnly CThe finite-quotient predicate follows from the bundled class data.
Show proof
fun hG => C.finite 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.
□class ContainsTrivialQuotients (C : FiniteGroupClass.{u}) : Prop where
of_subsingleton : ∀ {Q : Type u} [Group Q], Subsingleton Q → C QThe finite-group class contains all trivial groups. This is the class-level form needed when a construction indexes over quotients and must include the terminal quotient. Formations provide this automatically via \(\mathrm{Formation.one\_mem}\); users of a formation should not add a separate hypothesis.
def IsomClosed (C : FiniteGroupClass.{u}) : Prop :=
∀ {G H : Type u} [Group G] [Group H], Nonempty (G ≃* H) → C G → C HThe finite group class is closed under isomorphism.
def SubgroupClosed (C : FiniteGroupClass.{u}) : Prop :=
∀ {G : Type u} [Group G] (H : Subgroup G), C G → C HThe finite group class is closed under taking subgroups.
def NormalSubgroupClosed (C : FiniteGroupClass.{u}) : Prop :=
∀ {G : Type u} [Group G] (N : Subgroup G) [N.Normal], C G → C NA finite-group class is closed under taking normal subgroups.
def QuotientClosed (C : FiniteGroupClass.{u}) : Prop :=
∀ {G : Type u} [Group G] (N : Subgroup G) [N.Normal], C G → C (G ⧸ N)The finite group class is closed under quotients.
def FiniteProductClosed (C : FiniteGroupClass.{u}) : Prop :=
∀ {ι : Type u} [Fintype ι] {G : ι → Type u} [∀ i, Group (G i)],
(∀ i, C (G i)) → C (∀ i, G i)Closed under forming finite direct products.
def FiniteSubdirectProductClosed (C : FiniteGroupClass.{u}) : Prop :=
∀ {ι : Type u} [Fintype ι] {G : Type u} [Group G]
{H : ι → Type u} [∀ i, Group (H i)],
(f : G →* ∀ i, H i) →
Function.Injective f →
(∀ i, Function.Surjective fun g : G => f g i) →
(∀ i, C (H i)) →
C Gdef ExtensionClosed (C : FiniteGroupClass.{u}) : Prop :=
∀ {E : Type u} [Group E] (N : Subgroup E) [N.Normal],
C N → C (E ⧸ N) → C EThe finite group class is closed under extensions.
structure Formation (C : FiniteGroupClass.{u}) : Prop where
quotientClosed : QuotientClosed C
finiteSubdirectProductClosed : FiniteSubdirectProductClosed CA formation of finite groups. Standard formation terminology starts with a family of finite groups containing the trivial group and then asks for closure under quotients and finite fiber/subdirect products. In this unbundled predicate formulation the trivial group condition is a theorem, \(unit membership\), because it follows from the empty finite subdirect product.
structure Variety (C : FiniteGroupClass.{u}) : Prop where
subgroupClosed : SubgroupClosed C
quotientClosed : QuotientClosed C
finiteProductClosed : FiniteProductClosed Cstructure MelnikovFormation (C : FiniteGroupClass.{u}) : Prop where
formation : Formation C
normalSubgroupClosed : NormalSubgroupClosed C
extensionClosed : ExtensionClosed CA Melnikov formation of finite groups. A Melnikov formation includes the underlying formation field directly, rather than re-proving it at every use site, so the standard formation formulation (including \(unit membership\)) is available immediately.
structure Hereditary (C : FiniteGroupClass.{u}) : Prop where
of_injective :
∀ {G H : Type u} [Group G] [Group H],
C H → (f : G →* H) → Function.Injective f → C GA finite-group class is hereditary when it is closed under injective homomorphisms. This is the form used by finite-quotient comap constructions: a pullback quotient embeds into the target finite quotient, so membership descends along injections.
structure FullFormation (C : FiniteGroupClass.{u}) : Prop where
melnikovFormation : MelnikovFormation C
subgroupClosed : SubgroupClosed CA full formation of finite groups. Equivalently, this is a Melnikov formation whose finite groups are closed under subgroups. The \(Hereditary\) injective-hom formulation is derived as FullFormation.hereditary.
class IsMelnikovFormation (C : FiniteGroupClass.{u}) : Prop where
melnikovFormation : MelnikovFormation CTypeclass wrapper for a Melnikov formation.
class IsFullFormation (C : FiniteGroupClass.{u}) : Prop where
fullFormation : FullFormation CTypeclass wrapper for a full formation.
structure FullFiniteFormation where
C : FiniteGroupClass.{u}
fullFormation : FullFormation Cdef isFormation_of_isMelnikovFormation
(C : FiniteGroupClass.{u}) [hC : IsMelnikovFormation C] :
IsFormation C where
formation := hC.melnikovFormation.formationA Melnikov formation typeclass supplies the underlying formation typeclass.
def isMelnikovFormation_of_isFullFormation
(C : FiniteGroupClass.{u}) [hC : IsFullFormation C] :
IsMelnikovFormation C where
melnikovFormation := hC.fullFormation.melnikovFormationA full formation typeclass supplies the underlying Melnikov formation typeclass.
theorem Formation.finiteOnly {C : FiniteGroupClass.{u}} (_hForm : Formation C) :
FiniteOnly CShow proof
C.finiteOnlyProof. 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 Variety.finiteOnly {C : FiniteGroupClass.{u}} (_hVar : Variety C) :
FiniteOnly CShow proof
C.finiteOnlyProof. 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 Formation.isomClosed {C : FiniteGroupClass.{u}} (hForm : Formation C) :
IsomClosed CA formation is closed under isomorphism.
Show proof
by
intro G H _ _ hGH hCG
rcases hGH with ⟨e⟩
let f : H →* (PUnit → G) :=
{ toFun := fun h _ => e.symm h
map_one' := by
ext i
cases i
simp only [map_one, Pi.one_apply]
map_mul' := by
intro x y
ext i
cases i
simp only [map_mul, Pi.mul_apply]}
have hf : Function.Injective f := by
intro x y hxy
exact e.symm.injective (by simpa [f] using congrFun hxy PUnit.unit)
have hsurj : ∀ i : PUnit, Function.Surjective fun h : H => f h i := by
intro i g
refine ⟨e g, ?_⟩
cases i
simp only [MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.symm_apply_apply, f]
exact hForm.finiteSubdirectProductClosed f hf hsurj (fun _ => hCG)Proof. 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 Formation.finiteProductClosed {C : FiniteGroupClass.{u}}
(hForm : Formation C) : FiniteProductClosed CShow proof
by
classical
intro ι _ G _ hG
let f : (∀ i, G i) →* ∀ i, G i := MonoidHom.id _
refine hForm.finiteSubdirectProductClosed f ?_ ?_ hG
· intro x y hxy
simpa [f] using hxy
· intro i y
refine ⟨Function.update 1 i y, ?_⟩
simp only [MonoidHom.id_apply, Function.update_self, f]Proof. 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 Formation.one_mem {C : FiniteGroupClass.{u}} (hForm : Formation C) :
C PUnitShow proof
by
let G : PEmpty → Type u := fun _ => PUnit
letI : ∀ i : PEmpty, Group (G i) := by
intro i
cases i
let e : ((i : PEmpty) → G i) ≃* PUnit := by
refine
{ toFun := fun _ => PUnit.unit
invFun := fun _ i => nomatch i
left_inv := ?_
right_inv := ?_
map_mul' := ?_ }
· intro x
ext i
· intro x
cases x
rfl
· intro x y
rfl
have hProd : C ((i : PEmpty) → G i) :=
hForm.finiteProductClosed (ι := PEmpty) (G := G) (fun i => by cases i)
exact hForm.isomClosed ⟨e⟩ hProdProof. 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 IsomClosed.of_mulEquiv {C : FiniteGroupClass.{u}}
(hIso : IsomClosed C) {G H : Type u} [Group G] [Group H]
(e : G ≃* H) (hG : C G) :
C HUse a specified multiplicative equivalence to transport membership in an isomorphism-closed finite-group class.
Show proof
hIso ⟨e⟩ 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 IsomClosed.iff_of_mulEquiv {C : FiniteGroupClass.{u}}
(hIso : IsomClosed C) {G H : Type u} [Group G] [Group H]
(e : G ≃* H) :
C G ↔ C HMembership in an isomorphism-closed finite-group class is invariant under a specified multiplicative equivalence.
Show proof
⟨hIso.of_mulEquiv e, hIso.of_mulEquiv e.symm⟩Proof. 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 containsTrivialQuotients_of_isomClosed_one_mem {C : FiniteGroupClass.{u}}
(hIso : IsomClosed C) (hOne : C PUnit) :
ContainsTrivialQuotients CAn isomorphism-closed class containing the trivial group contains every trivial group.
Show proof
by
refine ⟨?_⟩
intro Q _ hQ
letI : Subsingleton Q := hQ
let e : PUnit ≃* Q :=
{ toFun := fun _ => 1
invFun := fun _ => PUnit.unit
left_inv := by
intro x
cases x
rfl
right_inv := by
intro q
exact Subsingleton.elim _ _
map_mul' := by
intro x y
exact Subsingleton.elim _ _ }
exact hIso ⟨e⟩ hOneProof. 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 Formation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
(hForm : Formation C) :
ContainsTrivialQuotients CA formation contains the trivial quotients required by the pro-\(C\) construction.
Show proof
containsTrivialQuotients_of_isomClosed_one_mem hForm.isomClosed hForm.one_memProof. 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 finiteSubdirectProductClosed_of_isomClosed_subgroupClosed_finiteProductClosed
{C : FiniteGroupClass.{u}}
(hIso : IsomClosed C)
(hSub : SubgroupClosed C)
(hProd : FiniteProductClosed C) :
FiniteSubdirectProductClosed CShow proof
by
intro ι _ G _ H _ f hf _hsurj hH
have hPi : C (∀ i, H i) := hProd hH
have hRange : C f.range := hSub f.range hPi
have hRangeRestrictInj : Function.Injective f.rangeRestrict := by
intro x y hxy
exact hf (by simpa using congrArg Subtype.val hxy)
let e : G ≃* f.range := MulEquiv.ofBijective f.rangeRestrict
⟨hRangeRestrictInj, f.rangeRestrict_surjective⟩
exact hIso ⟨e.symm⟩ hRangeProof. 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 variety_one_mem_of_isomClosed {C : FiniteGroupClass.{u}}
(hVar : Variety C) (hIso : IsomClosed C) :
C PUnitAn isomorphism-closed variety contains the trivial group.
Show proof
by
let G : PEmpty → Type u := fun _ => PUnit
letI : ∀ i : PEmpty, Group (G i) := by
intro i
cases i
let e : ((i : PEmpty) → G i) ≃* PUnit := by
classical
refine
{ toFun := fun _ => PUnit.unit
invFun := fun _ i => nomatch i
left_inv := ?_
right_inv := ?_
map_mul' := ?_ }
· intro x
ext i
· intro x
cases x
rfl
· intro x y
rfl
have hProd : C ((i : PEmpty) → G i) :=
hVar.finiteProductClosed (ι := PEmpty) (G := G) (fun i => by cases i)
exact hIso ⟨e⟩ hProdProof. 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 one_mem_of_subgroupClosed_isomClosed {C : FiniteGroupClass.{u}}
(hSub : SubgroupClosed C) (hIso : IsomClosed C)
{G : Type u} [Group G] (hG : C G) :
C PUnitAny subgroup-closed, isomorphism-closed class that contains at least one group also contains the trivial group.
Show proof
by
let eBot : (⊥ : Subgroup G) ≃* PUnit :=
{ toFun := fun _ => PUnit.unit
invFun := fun _ => 1
left_inv := by
intro x
exact Subsingleton.elim _ _
right_inv := by
intro x
cases x
rfl
map_mul' := by
intro x y
rfl }
exact hIso ⟨eBot⟩ (hSub (⊥ : Subgroup G) hG)Proof. 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 Hereditary.of_subgroupClosed_isomClosed {C : FiniteGroupClass.{u}}
(hSub : SubgroupClosed C) (hIso : IsomClosed C) :
Hereditary CSubgroup- and isomorphism-closure imply the injective-hom hereditary form.
Show proof
by
refine ⟨?_⟩
intro G H _ _ hH f hf
have hRange : C f.range := hSub f.range hH
let e : G ≃* f.range := MulEquiv.ofBijective f.rangeRestrict
⟨by
intro x y hxy
exact hf (by simpa using congrArg Subtype.val hxy),
f.rangeRestrict_surjective⟩
exact hIso ⟨e.symm⟩ hRangeProof. 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 Hereditary.subgroupClosed {C : FiniteGroupClass.{u}}
(hHer : Hereditary C) :
SubgroupClosed CThe finite group class is closed under taking subgroups.
Show proof
by
intro G _ H hG
exact hHer.of_injective hG 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 Hereditary.of_mulEquiv {C : FiniteGroupClass.{u}}
(hHer : Hereditary C) {G H : Type u} [Group G] [Group H]
(e : G ≃* H) (hH : C H) :
C GUse a specified multiplicative equivalence to transport membership in an isomorphism-closed finite-group class.
Show proof
hHer.of_injective hH e.toMonoidHom e.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 Hereditary.iff_of_mulEquiv {C : FiniteGroupClass.{u}}
(hHer : Hereditary C) {G H : Type u} [Group G] [Group H]
(e : G ≃* H) :
C G ↔ C HMembership in an isomorphism-closed finite-group class is invariant under a specified multiplicative equivalence.
Show proof
⟨fun hG => hHer.of_mulEquiv e.symm hG, fun hH => hHer.of_mulEquiv e hH⟩Proof. 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 MelnikovFormation.finiteOnly {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) : FiniteOnly CThe finite-quotient predicate follows from the bundled class data.
Show proof
hC.formation.finiteOnlyProof. 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 MelnikovFormation.quotientClosed {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) : QuotientClosed CA Melnikov formation is closed under quotients.
Show proof
hC.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 MelnikovFormation.one_mem {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) : C PUnitShow proof
hC.formation.one_memProof. 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 MelnikovFormation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) :
ContainsTrivialQuotients CA Melnikov formation contains the trivial quotients.
Show proof
hC.formation.containsTrivialQuotientsProof. 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 MelnikovFormation.isomClosed {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) : IsomClosed CA Melnikov formation is closed under isomorphism.
Show proof
hC.formation.isomClosedProof. 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 FullFormation.finiteOnly {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : FiniteOnly CThe finite-quotient predicate follows from the bundled class data.
Show proof
hC.melnikovFormation.finiteOnlyProof. 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 FullFormation.quotientClosed {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : QuotientClosed CA full formation is closed under quotients.
Show proof
hC.melnikovFormation.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 FullFormation.one_mem {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : C PUnitShow proof
hC.melnikovFormation.one_memProof. 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 FullFormation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
(hC : FullFormation C) :
ContainsTrivialQuotients CA full formation contains the trivial quotients.
Show proof
hC.melnikovFormation.containsTrivialQuotientsProof. 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 FullFormation.isomClosed {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : IsomClosed CA full formation is closed under isomorphism.
Show proof
hC.melnikovFormation.isomClosedProof. 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 FullFormation.normalSubgroupClosed {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : NormalSubgroupClosed CA full formation is closed under normal subgroups.
Show proof
hC.melnikovFormation.normalSubgroupClosedProof. 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 FullFormation.extensionClosed {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : ExtensionClosed CA formation is closed under extensions.
Show proof
hC.melnikovFormation.extensionClosedProof. 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 FullFormation.hereditary {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : Hereditary CThe subgroup-closed part of a full formation, in the injective-hom form used by finite quotient pullbacks.
Show proof
Hereditary.of_subgroupClosed_isomClosed hC.subgroupClosed hC.isomClosedProof. 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 variety_formation {C : FiniteGroupClass.{u}}
(hVar : Variety C) (hIso : IsomClosed C) :
Formation CAn isomorphism-closed variety is a formation in the unbundled FiniteGroupClass formulation.
Show proof
by
refine ⟨hVar.quotientClosed, ?_⟩
exact finiteSubdirectProductClosed_of_isomClosed_subgroupClosed_finiteProductClosed
hIso hVar.subgroupClosed hVar.finiteProductClosedProof. 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 Variety.closureBundle_of_isomClosed_extensionClosed {C : FiniteGroupClass.{u}}
(hVar : Variety C)
(hIso : IsomClosed C)
(hExt : ExtensionClosed C) :
Formation C ∧ SubgroupClosed C ∧ IsomClosed C ∧ QuotientClosed C ∧ ExtensionClosed CShow proof
by
exact ⟨variety_formation hVar hIso, hVar.subgroupClosed, hIso, hVar.quotientClosed, hExt⟩Proof. 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 MelnikovFormation.quotient_inf_mem {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C)
{G : Type u} [Group G]
(N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal]
(h₁ : C (G ⧸ N₁)) (h₂ : C (G ⧸ N₂)) :
C (G ⧸ (N₁ ⊓ N₂))For a Melnikov formation, the quotients by two normal subgroups lying in the class force the quotient by their intersection to lie in the class as well.
Show proof
by
let E : Type u := G ⧸ (N₁ ⊓ N₂)
let L : Subgroup E := Subgroup.map (QuotientGroup.mk' (N₁ ⊓ N₂)) N₁
letI : L.Normal := by
dsimp [L]
exact Subgroup.Normal.map (show N₁.Normal by infer_instance)
(QuotientGroup.mk' (N₁ ⊓ N₂))
(QuotientGroup.mk'_surjective (N₁ ⊓ N₂))
have hQuotL : C (E ⧸ L) := by
let e : E ⧸ L ≃* G ⧸ N₁ :=
QuotientGroup.quotientQuotientEquivQuotient (N₁ ⊓ N₂) N₁ inf_le_left
exact hC.isomClosed ⟨e.symm⟩ h₁
let K₂ : Subgroup (G ⧸ N₂) := Subgroup.map (QuotientGroup.mk' N₂) N₁
letI : K₂.Normal := by
dsimp [K₂]
exact Subgroup.Normal.map (show N₁.Normal by infer_instance)
(QuotientGroup.mk' N₂)
(QuotientGroup.mk'_surjective N₂)
have hK₂ : C K₂ := hC.normalSubgroupClosed K₂ h₂
let ψ₂ : N₁ →* G ⧸ N₂ := (QuotientGroup.mk' N₂).comp N₁.subtype
have hψ₂range : ψ₂.range = K₂ := by
ext x
constructor
· rintro ⟨y, rfl⟩
exact ⟨y.1, y.2, rfl⟩
· rintro ⟨y, hy, rfl⟩
exact ⟨⟨y, hy⟩, rfl⟩
have hψ₂ker : ψ₂.ker = N₂.subgroupOf N₁ := by
ext x
change QuotientGroup.mk' N₂ x.1 = 1 ↔ x.1 ∈ N₂
simp only [QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff (N := N₂) x.1]
have hQuotN₁ : C (N₁ ⧸ N₂.subgroupOf N₁) := by
let e₀ : N₁ ⧸ N₂.subgroupOf N₁ ≃* N₁ ⧸ ψ₂.ker :=
QuotientGroup.quotientMulEquivOfEq hψ₂ker.symm
let e₁ : N₁ ⧸ ψ₂.ker ≃* ψ₂.range := QuotientGroup.quotientKerEquivRange ψ₂
let e₂ : ψ₂.range ≃* K₂ := MulEquiv.subgroupCongr hψ₂range
exact hC.isomClosed ⟨((e₀.trans e₁).trans e₂).symm⟩ hK₂
let ψ₁ : N₁ →* E := (QuotientGroup.mk' (N₁ ⊓ N₂)).comp N₁.subtype
have hψ₁range : ψ₁.range = L := by
ext x
constructor
· rintro ⟨y, rfl⟩
exact ⟨y.1, y.2, rfl⟩
· rintro ⟨y, hy, rfl⟩
exact ⟨⟨y, hy⟩, rfl⟩
have hψ₁ker : ψ₁.ker = N₂.subgroupOf N₁ := by
ext x
change QuotientGroup.mk' (N₁ ⊓ N₂) x.1 = 1 ↔ x.1 ∈ N₂
constructor
· intro hx
exact (QuotientGroup.eq_one_iff (N := N₁ ⊓ N₂) x.1).1 hx |>.2
· intro hx
exact (QuotientGroup.eq_one_iff (N := N₁ ⊓ N₂) x.1).2 ⟨x.2, hx⟩
have hL : C L := by
let e₀ : N₁ ⧸ N₂.subgroupOf N₁ ≃* N₁ ⧸ ψ₁.ker :=
QuotientGroup.quotientMulEquivOfEq hψ₁ker.symm
let e₁ : N₁ ⧸ ψ₁.ker ≃* ψ₁.range := QuotientGroup.quotientKerEquivRange ψ₁
let e₂ : ψ₁.range ≃* L := MulEquiv.subgroupCongr hψ₁range
exact hC.isomClosed ⟨(e₀.trans e₁).trans e₂⟩ hQuotN₁
exact hC.extensionClosed L hL hQuotLProof. 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 MelnikovFormation.closureBundle_of_subgroupClosed {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C)
(hSub : SubgroupClosed C) :
Formation C ∧ SubgroupClosed C ∧ IsomClosed C ∧ QuotientClosed C ∧ ExtensionClosed CA Melnikov formation with subgroup closure gives the standard finite-class closure bundle.
Show proof
by
exact ⟨hC.formation, hSub, hC.isomClosed, hC.quotientClosed, hC.extensionClosed⟩Proof. 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 Formation.quotient_inf_mem {C : FiniteGroupClass.{u}}
(hC : Formation C) {G : Type u} [Group G]
(N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal]
(h₁ : C (G ⧸ N₁)) (h₂ : C (G ⧸ N₂)) :
C (G ⧸ (N₁ ⊓ N₂))For a formation, the quotient by the intersection of two normal subgroups whose individual quotients lie in \(C\) also lies in \(C\). This is the two-factor form of (C4).
Show proof
by
classical
let H : ULift Bool → Type u
| ⟨false⟩ => G ⧸ N₁
| ⟨true⟩ => G ⧸ N₂
letI : ∀ b : ULift Bool, Group (H b) := by
intro b
cases b with
| up b =>
cases b <;> infer_instance
let f : G ⧸ (N₁ ⊓ N₂) →* ∀ b : ULift Bool, H b :=
{ toFun := fun x b =>
match b with
| ⟨false⟩ => QuotientGroup.map (N₁ ⊓ N₂) N₁ (MonoidHom.id G) inf_le_left x
| ⟨true⟩ => QuotientGroup.map (N₁ ⊓ N₂) N₂ (MonoidHom.id G) inf_le_right x
map_one' := by
funext b
cases b with
| up b =>
cases b <;> rfl
map_mul' := by
intro x y
funext b
cases b with
| up b =>
cases b with
| false =>
exact (QuotientGroup.map (N₁ ⊓ N₂) N₁ (MonoidHom.id G) inf_le_left).map_mul x y
| true =>
exact (QuotientGroup.map (N₁ ⊓ N₂) N₂ (MonoidHom.id G) inf_le_right).map_mul x y }
refine hC.finiteSubdirectProductClosed (ι := ULift Bool) (H := H) f ?_ ?_ ?_
· intro x y hxy
rcases QuotientGroup.mk'_surjective (N₁ ⊓ N₂) x with ⟨gx, rfl⟩
rcases QuotientGroup.mk'_surjective (N₁ ⊓ N₂) y with ⟨gy, rfl⟩
apply QuotientGroup.eq.2
constructor
· have hfalse :
f (QuotientGroup.mk' (N₁ ⊓ N₂) gx) ⟨false⟩ =
f (QuotientGroup.mk' (N₁ ⊓ N₂) gy) ⟨false⟩ :=
congrArg (fun z : ∀ b : ULift Bool, H b => z ⟨false⟩) hxy
exact QuotientGroup.eq.1 (by simpa [f, H] using hfalse)
· have htrue :
f (QuotientGroup.mk' (N₁ ⊓ N₂) gx) ⟨true⟩ =
f (QuotientGroup.mk' (N₁ ⊓ N₂) gy) ⟨true⟩ :=
congrArg (fun z : ∀ b : ULift Bool, H b => z ⟨true⟩) hxy
exact QuotientGroup.eq.1 (by simpa [f, H] using htrue)
· intro b
cases b with
| up b =>
cases b with
| false =>
intro x
rcases QuotientGroup.mk'_surjective N₁ x with ⟨g, rfl⟩
refine ⟨QuotientGroup.mk' (N₁ ⊓ N₂) g, ?_⟩
simp only [QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk, QuotientGroup.map_mk, MonoidHom.id_apply,
H, f]
| true =>
intro x
rcases QuotientGroup.mk'_surjective N₂ x with ⟨g, rfl⟩
refine ⟨QuotientGroup.mk' (N₁ ⊓ N₂) g, ?_⟩
simp only [QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk, QuotientGroup.map_mk, MonoidHom.id_apply,
H, f]
· intro b
cases b with
| up b =>
cases b with
| false =>
simpa [H] using h₁
| true =>
simpa [H] using h₂Proof. 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.
□