Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Classification

The statement of the classification of finite simple groups #

This file assembles the explicit cyclic, alternating, Lie-type, and sporadic carriers indexed by TauCeti.CFSGIndex. It then records the classification as a named proposition. No finiteness or simplicity property of a listed carrier is asserted here, and the classification proposition is not proved. The Lie-type branches use explicit carriers; their identification with the pinned simply connected group schemes remains separate. The sporadic branches use the recorded finite presentations, without assuming any recognition theorem for the presented groups.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev TauCeti.CFSGIndex.Group :
CFSGIndex → Type

The concrete carrier type represented by an index on the classification list.

Instances For
    source
    @[instance_reducible]
    noncomputable instance TauCeti.instGroupGroup (i : CFSGIndex) :
    Group i.Group
    source
    def TauCeti.ClassificationStatement :
    Prop

    Classification of finite simple groups, statement only. Every finite simple group is isomorphic to one of the explicitly constructed groups on the classification list.

    Instances For
      source
      theorem TauCeti.classificationStatement_iff :
      ClassificationStatement ↔ ∀ (G : Type u) [inst : Group G] [Finite G] [IsSimpleGroup G], ∃ (i : CFSGIndex), Nonempty (G ≃* i.Group)

      The classification statement holds exactly when every finite simple group is isomorphic to one of the indexed carriers.

      source
      theorem TauCeti.ClassificationStatement.of_universe (h : ClassificationStatement) :
      ClassificationStatement

      The classification statement in one universe implies the statement in every universe: a finite group can be transported to a carrier in any universe.