FiniteGroupClass bundles an isomorphism-invariant predicate whose members are finite. The module provides universe-independent membership through finite-group representatives and defines the closure conditions used throughout the pro-\(C\) library, including formations, varieties, Melnikov formations, hereditary classes, and full formations.
A class of groups, implemented as an unbundled predicate on group carriers.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v wabbrev GroupClassA finite-group class is a predicate on group carriers together with a certificate that every member is finite.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v wstructure FiniteGroupClass where
/-- The membership predicate selecting the group carriers that belong to the class. -/
pred : GroupClass.{u}
/-- Membership supplies a `Finite` instance for the selected group. -/
finite_of_mem : ∀ {G : Type u} [Group G], pred G → Finite G
/--
Membership transports forward across a multiplicative equivalence, making the predicate
independent of the chosen carrier for a finite group.
-/
mem_of_mulEquiv :
∀ {G H : Type u} [Group G] [Group H], (G ≃* H) → pred G → pred HA finite group class coerces to its underlying predicate on finite groups.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v winstance instCoeFunFiniteGroupClass : CoeFun FiniteGroupClass (fun _ => GroupClass.{u}) where
coe C := C.predMembers of a bundled finite-group class are finite.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem finite {C : FiniteGroupClass.{u}} {G : Type u} [Group G] (hG : C G) : Finite GCross-universe membership in a finite-group class: G belongs when it is multiplicatively equivalent to a member represented in the carrier universe of C.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef MemAcrossUniverses (C : FiniteGroupClass.{u}) (G : Type v) [Group G] : PropCross-universe membership still certifies that the represented group is finite.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem finite_of_memAcrossUniverses {C : FiniteGroupClass.{u}}
{G : Type v} [Group G] (hG : C.MemAcrossUniverses G) : Finite GNative membership gives cross-universe membership in the class's own universe.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem memAcrossUniverses_of_mem {C : FiniteGroupClass.{u}}
{G : Type u} [Group G] (hG : C G) : C.MemAcrossUniverses GIn the class's own universe, cross-universe membership reduces to native membership.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem mem_of_memAcrossUniverses {C : FiniteGroupClass.{u}}
{G : Type u} [Group G] (hG : C.MemAcrossUniverses G) : C GCross-universe membership agrees with the original predicate in the original universe.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem memAcrossUniverses_iff (C : FiniteGroupClass.{u})
{G : Type u} [Group G] : C.MemAcrossUniverses G ↔ C GCross-universe membership is invariant under a multiplicative equivalence, even when the two carriers live in different universes.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem memAcrossUniverses_iff_of_mulEquiv (C : FiniteGroupClass.{u})
{G : Type v} {K : Type w} [Group G] [Group K] (e : G ≃* K) :
C.MemAcrossUniverses G ↔ C.MemAcrossUniverses KULift does not affect cross-universe membership. This is the preferred public replacement for ad hoc Type-0 lowering lemmas.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem memAcrossUniverses_ulift_iff (C : FiniteGroupClass.{u})
(G : Type v) [Group G] :
C.MemAcrossUniverses (ULift.{w} G) ↔ C.MemAcrossUniverses GIn the native universe, ULift invariance also holds for the original predicate.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem ulift_mem_iff (C : FiniteGroupClass.{u}) (G : Type u) [Group G] :
C (ULift.{u} G) ↔ C GThe object property represented by C on finite groups in any target universe.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef objectPropertyAcrossUniverses (C : FiniteGroupClass.{u}) :
CategoryTheory.ObjectProperty FiniteGrp.{v}The cross-universe categorical object property is closed under isomorphisms.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassinstance objectPropertyAcrossUniverses_isClosedUnderIsomorphisms
(C : FiniteGroupClass.{u}) :
C.objectPropertyAcrossUniverses.IsClosedUnderIsomorphisms where
of_iso {G H} e hG := by
let eGrp : G.toGrp ≅ H.toGrp :=
(CategoryTheory.inducedFunctor FiniteGrp.toGrp).mapIso e
exact (C.memAcrossUniverses_iff_of_mulEquiv eGrp.groupIsoToMulEquiv).1 hGThe 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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassclass ContainsTrivialQuotients (C : FiniteGroupClass.{u}) : Prop where
/-- Every group with at most one element belongs to `C`, regardless of its chosen carrier. -/
of_subsingleton : ∀ {Q : Type u} [Group Q], Subsingleton Q → C QThe finite group class is closed under isomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef IsomClosed (C : FiniteGroupClass.{u}) : PropEvery finite-group class is invariant under multiplicative equivalence by construction.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem isomClosed (C : FiniteGroupClass.{u}) : IsomClosed CThe canonical categorical object property attached to a finite-group class.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef objectProperty (C : FiniteGroupClass.{u}) : CategoryTheory.ObjectProperty FiniteGrp.{u}The categorical object property of a finite-group class is closed under isomorphisms.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassinstance objectProperty_isClosedUnderIsomorphisms (C : FiniteGroupClass.{u}) :
C.objectProperty.IsClosedUnderIsomorphisms where
of_iso {G H} e hG := by
let eGrp : G.toGrp ≅ H.toGrp :=
(CategoryTheory.inducedFunctor FiniteGrp.toGrp).mapIso e
exact C.mem_of_mulEquiv eGrp.groupIsoToMulEquiv hGThe finite group class is closed under taking subgroups.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef SubgroupClosed (C : FiniteGroupClass.{u}) : PropA finite-group class is closed under taking normal subgroups.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef NormalSubgroupClosed (C : FiniteGroupClass.{u}) : PropThe finite group class is closed under quotients.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef QuotientClosed (C : FiniteGroupClass.{u}) : PropClosed under forming finite direct products.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef FiniteProductClosed (C : FiniteGroupClass.{u}) : PropClosed under forming finite subdirect products. We package a finite subdirect product as an injective homomorphism into a finite product whose coordinate maps are all surjective.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef FiniteSubdirectProductClosed (C : FiniteGroupClass.{u}) : PropThe finite group class is closed under extensions.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassdef ExtensionClosed (C : FiniteGroupClass.{u}) : PropA formation is a family of finite groups closed under quotients and finite fiber or subdirect products; the empty finite subdirect product supplies membership of the trivial group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassstructure Formation (C : FiniteGroupClass.{u}) : Prop where
/-- Membership in `C` descends to quotients by arbitrary normal subgroups. -/
quotientClosed : QuotientClosed C
/--
A finite group belongs to `C` when it embeds as a subdirect product of finitely many members
of `C`.
-/
finiteSubdirectProductClosed : FiniteSubdirectProductClosed CA variety of finite groups.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassstructure Variety (C : FiniteGroupClass.{u}) : Prop where
/-- Membership in `C` descends to subgroups. -/
subgroupClosed : SubgroupClosed C
/-- Membership in `C` descends to quotients by normal subgroups. -/
quotientClosed : QuotientClosed C
/-- Finite direct products of members of `C` again belong to `C`. -/
finiteProductClosed : FiniteProductClosed CA Melnikov formation includes the underlying formation data directly, so the standard formulation, including unit membership, is immediately available.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassstructure MelnikovFormation (C : FiniteGroupClass.{u}) : Prop where
/-- The quotient and finite-subdirect-product closure axioms of the underlying formation. -/
formation : Formation C
/-- Normal subgroups of members of `C` again belong to `C`. -/
normalSubgroupClosed : NormalSubgroupClosed C
/--
A finite group belongs to `C` whenever a normal subgroup and the corresponding quotient both
belong to `C`.
-/
extensionClosed : ExtensionClosed CA 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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassstructure Hereditary (C : FiniteGroupClass.{u}) : Prop where
/--
Membership pulls back along injective homomorphisms: a group embedded in a member of `C`
itself belongs to `C`.
-/
of_injective :
∀ {G H : Type u} [Group G] [Group H],
C H → (f : G →* H) → Function.Injective f → C GA 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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClassstructure FullFormation (C : FiniteGroupClass.{u}) : Prop where
/--
The formation, normal-subgroup, and extension closure data supplied by a Melnikov formation.
-/
melnikovFormation : MelnikovFormation C
/-- Arbitrary subgroups of members of `C` again belong to `C`. -/
subgroupClosed : SubgroupClosed CA formation is closed under isomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem Formation.isomClosed {C : FiniteGroupClass.{u}} (_hForm : Formation C) :
IsomClosed CEvery formation is closed under finite direct products.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem Formation.finiteProductClosed {C : FiniteGroupClass.{u}}
(hForm : Formation C) : FiniteProductClosed CEvery formation contains the trivial group. This is the standard trivial-object clause. In this version it is derived from the empty finite subdirect product, so no separate hypothesis asserting that the trivial group belongs to the class is needed.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem Formation.one_mem {C : FiniteGroupClass.{u}} (hForm : Formation C) :
C PUnitUse a specified multiplicative equivalence to transport membership in an isomorphism-closed finite-group class.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem IsomClosed.of_mulEquiv {C : FiniteGroupClass.{u}}
(hIso : IsomClosed C) {G H : Type u} [Group G] [Group H]
(e : G ≃* H) (hG : C G) :
C HMembership in an isomorphism-closed finite-group class is invariant under a specified multiplicative equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem IsomClosed.iff_of_mulEquiv {C : FiniteGroupClass.{u}}
(hIso : IsomClosed C) {G H : Type u} [Group G] [Group H]
(e : G ≃* H) :
C G ↔ C HAn isomorphism-closed class containing the trivial group contains every trivial group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem containsTrivialQuotients_of_isomClosed_one_mem {C : FiniteGroupClass.{u}}
(hIso : IsomClosed C) (hOne : C PUnit) :
ContainsTrivialQuotients CA formation contains the trivial quotients required by the pro-\(C\) construction.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem Formation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
(hForm : Formation C) :
ContainsTrivialQuotients CAny isomorphism-closed subgroup-closed class that is closed under finite direct products is also closed under finite subdirect products.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem finiteSubdirectProductClosed_of_isomClosed_subgroupClosed_finiteProductClosed
{C : FiniteGroupClass.{u}}
(hIso : IsomClosed C)
(hSub : SubgroupClosed C)
(hProd : FiniteProductClosed C) :
FiniteSubdirectProductClosed CAn isomorphism-closed variety contains the trivial group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem variety_one_mem_of_isomClosed {C : FiniteGroupClass.{u}}
(hVar : Variety C) (hIso : IsomClosed C) :
C PUnitAny subgroup-closed, isomorphism-closed class that contains at least one group also contains the trivial group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem one_mem_of_subgroupClosed_isomClosed {C : FiniteGroupClass.{u}}
(hSub : SubgroupClosed C) (hIso : IsomClosed C)
{G : Type u} [Group G] (hG : C G) :
C PUnitSubgroup- and isomorphism-closure imply the injective-hom hereditary form.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem Hereditary.of_subgroupClosed_isomClosed {C : FiniteGroupClass.{u}}
(hSub : SubgroupClosed C) (hIso : IsomClosed C) :
Hereditary CThe finite group class is closed under taking subgroups.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem Hereditary.subgroupClosed {C : FiniteGroupClass.{u}}
(hHer : Hereditary C) :
SubgroupClosed CUse a specified multiplicative equivalence to transport membership in an isomorphism-closed finite-group class.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem Hereditary.of_mulEquiv {C : FiniteGroupClass.{u}}
(hHer : Hereditary C) {G H : Type u} [Group G] [Group H]
(e : G ≃* H) (hH : C H) :
C GMembership in an isomorphism-closed finite-group class is invariant under a specified multiplicative equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem Hereditary.iff_of_mulEquiv {C : FiniteGroupClass.{u}}
(hHer : Hereditary C) {G H : Type u} [Group G] [Group H]
(e : G ≃* H) :
C G ↔ C HA Melnikov formation is closed under quotients.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem MelnikovFormation.quotientClosed {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) : QuotientClosed CEvery formation contains the trivial group. This is the standard trivial-object clause. In this version it is derived from the empty finite subdirect product, so no separate hypothesis asserting that the trivial group belongs to the class is needed.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem MelnikovFormation.one_mem {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) : C PUnitA Melnikov formation contains the trivial quotients.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem MelnikovFormation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) :
ContainsTrivialQuotients CA Melnikov formation is closed under isomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem MelnikovFormation.isomClosed {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C) : IsomClosed CA full formation is closed under quotients.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem FullFormation.quotientClosed {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : QuotientClosed CEvery formation contains the trivial group. This is the standard trivial-object clause. In this version it is derived from the empty finite subdirect product, so no separate hypothesis asserting that the trivial group belongs to the class is needed.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem FullFormation.one_mem {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : C PUnitA full formation contains the trivial quotients.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem FullFormation.containsTrivialQuotients {C : FiniteGroupClass.{u}}
(hC : FullFormation C) :
ContainsTrivialQuotients CA full formation is closed under isomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem FullFormation.isomClosed {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : IsomClosed CA full formation is closed under normal subgroups.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem FullFormation.normalSubgroupClosed {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : NormalSubgroupClosed CA formation is closed under extensions.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem FullFormation.extensionClosed {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : ExtensionClosed CThe subgroup-closed part of a full formation, in the injective-hom form used by finite quotient pullbacks.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem FullFormation.hereditary {C : FiniteGroupClass.{u}}
(hC : FullFormation C) : Hereditary CAn isomorphism-closed variety is a formation in the unbundled FiniteGroupClass formulation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem variety_formation {C : FiniteGroupClass.{u}}
(hVar : Variety C) (hIso : IsomClosed C) :
Formation CA variety together with extension-closure packages the standard finite-class closure hypotheses used by the pro-\(C\) formulation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem 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 CFor 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.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem 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₂))A Melnikov formation with subgroup closure gives the standard finite-class closure bundle.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem MelnikovFormation.closureBundle_of_subgroupClosed {C : FiniteGroupClass.{u}}
(hC : MelnikovFormation C)
(hSub : SubgroupClosed C) :
Formation C ∧ SubgroupClosed C ∧ IsomClosed C ∧ QuotientClosed C ∧ ExtensionClosed CFor 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).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
universe u v w
namespace FiniteGroupClasstheorem 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₂))