Stating the classification of finite simple groups

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionClassification of finite simple groups, statement only#

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

TauCeti.ClassificationStatement.{u} : Prop

Lean

Formalized in Tau Ceti as TauCeti.ClassificationStatement.

Sources

• Tau Ceti documentation: TauCeti.ClassificationStatement
• Source of TauCeti.ClassificationStatement in TauCeti/GroupTheory/SpecificGroups/CFSG/Classification.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.ClassificationStatement

Uses 4

Statement usesTauCeti.SporadicName.presentation · TauCeti.ValidLieTypeIndex.Group

Proof usesThe ambient group of a valid Lie-type index · Cauchy--Binet for 2 × 2 minors

AbbreviationTauCeti.ValidLieTypeIndex.Group#

The Lie-type candidate is the derived subgroup of the fixed points modulo its own centre. No finiteness or simplicity instance is assumed or supplied.

TauCeti.ValidLieTypeIndex.Group (d : TauCeti.ValidLieTypeIndex) : Type

Lean

Formalized in Tau Ceti as TauCeti.ValidLieTypeIndex.Group.

Sources

• Tau Ceti documentation: TauCeti.ValidLieTypeIndex.Group
• Source of TauCeti.ValidLieTypeIndex.Group in TauCeti/GroupTheory/SpecificGroups/CFSG/Assembly/LieType.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.ValidLieTypeIndex.Group

Uses 2 · Used by 1

Statement usesThe ambient group of a valid Lie-type index

Proof usesCauchy--Binet for 2 × 2 minors

Used byClassification of finite simple groups, statement only

TheoremThe Steinberg endomorphism is the graph automorphism composed with the Frobenius#

The Steinberg endomorphism is the graph automorphism composed with the Frobenius, uniformly in the thirteen ordinary and graph-twisted families. On the nine untwisted ones the graph factor is trivial and the composite is the Frobenius itself, which is TauCeti.GraphTwistedIndex.steinberg_eq_frobenius.

TauCeti.GraphTwistedIndex.steinberg_eq_graphAut_comp_frobenius (d : TauCeti.GraphTwistedIndex) :
  d.steinberg = (MulEquiv.toMonoidHom d.graphAut).comp d.frobenius

Lean

Formalized in Tau Ceti as TauCeti.GraphTwistedIndex.steinberg_eq_graphAut_comp_frobenius.

Sources

• Tau Ceti documentation: TauCeti.GraphTwistedIndex.steinberg_eq_graphAut_comp_frobenius
• Source of TauCeti.GraphTwistedIndex.steinberg_eq_graphAut_comp_frobenius in TauCeti/GroupTheory/SpecificGroups/CFSG/Assembly/GraphTwisted.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.GraphTwistedIndex.steinberg_eq_graphAut_comp_frobenius

TheoremTauCeti.F4ShortRoot.PrimeField.specialIsogeny_specialIsogeny#

Squaring the special endomorphism gives the prime-field Frobenius on all carrier points.

TauCeti.F4ShortRoot.PrimeField.specialIsogeny_specialIsogeny.{u_1} (A : Type u_1) [CommRing A]
  [Algebra (ZMod 2) A] (g : ↥(TauCeti.F4ShortRoot.PrimeField.points A)) :
  (TauCeti.F4ShortRoot.PrimeField.specialIsogeny A)
      ((TauCeti.F4ShortRoot.PrimeField.specialIsogeny A) g) =
    (TauCeti.F4ShortRoot.PrimeField.frobenius 1 A) g

Lean

Formalized in Tau Ceti as TauCeti.F4ShortRoot.PrimeField.specialIsogeny_specialIsogeny.

Sources

• Tau Ceti documentation: TauCeti.F4ShortRoot.PrimeField.specialIsogeny_specialIsogeny
• Source of TauCeti.F4ShortRoot.PrimeField.specialIsogeny_specialIsogeny in TauCeti/Algebra/Lie/F4/ShortRoot/PrimeField/QuotientSpecialIsogeny.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.F4ShortRoot.PrimeField.specialIsogeny_specialIsogeny

DefinitionTauCeti.SporadicName.presentation#

The explicit, cited finite presentation attached to each sporadic-group name.

TauCeti.SporadicName.presentation : TauCeti.SporadicName → TauCeti.GroupPresentation

Lean

Formalized in Tau Ceti as TauCeti.SporadicName.presentation.

Sources

• Tau Ceti documentation: TauCeti.SporadicName.presentation
• Source of TauCeti.SporadicName.presentation in TauCeti/GroupTheory/SpecificGroups/CFSG/Sporadic/Presentation.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.SporadicName.presentation

Used by 1

Used byClassification of finite simple groups, statement only

DefinitionThe explicit type-A carrier is equivalent to the points of the pinned SL_{r+1}/ℤ group scheme#

TauCeti.TypeALieIndex.carrierEquivPinned (d : TauCeti.TypeALieIndex) :
  d.AmbientGroup ≃* d.PinnedGroup

Lean

Formalized in Tau Ceti as TauCeti.TypeALieIndex.carrierEquivPinned.

Sources

• Tau Ceti documentation: TauCeti.TypeALieIndex.carrierEquivPinned
• Source of TauCeti.TypeALieIndex.carrierEquivPinned in TauCeti/GroupTheory/SpecificGroups/CFSG/TypeA/Agreement.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.TypeALieIndex.carrierEquivPinned

DefinitionThe ambient group of a valid Lie-type index#

the group of algebraic-closure-valued points of the explicit carrier assigned to its family. It is generally infinite, and it is not identified with the points of the pinned simply connected group scheme of the diagram. On the thirteen ordinary and graph-twisted constructors it is TauCeti.GraphTwistedIndex.AmbientGroup; the Suzuki family runs on the rank-two symplectic carrier, the Ree family of type G₂ on the short-root G₂ carrier over 𝔽₃, and the Ree family of type F₄ and the Tits construction on the short-root F₄ carrier over 𝔽₂.

TauCeti.ValidLieTypeIndex.AmbientGroup : TauCeti.ValidLieTypeIndex → Type

Lean

Formalized in Tau Ceti as TauCeti.ValidLieTypeIndex.AmbientGroup.

Sources

• Tau Ceti documentation: TauCeti.ValidLieTypeIndex.AmbientGroup
• Source of TauCeti.ValidLieTypeIndex.AmbientGroup in TauCeti/GroupTheory/SpecificGroups/CFSG/Assembly/AmbientGroup.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.ValidLieTypeIndex.AmbientGroup

Used by 2

Used byClassification of finite simple groups, statement only · TauCeti.ValidLieTypeIndex.Group

DefinitionTauCeti.FixedPointCandidate.congrOfFiniteKer#

Transport the candidate through an equivariant surjection with finite kernel whose only fixed point is the identity.

TauCeti.FixedPointCandidate.congrOfFiniteKer.{u_1, u_2} {G : Type u_1} {H : Type u_2} [Group G]
  [Group H] {F : G →* G} {F' : H →* H} (ψ : G →* H) [Finite ↥ψ.ker] (hψ : ψ.comp F = F'.comp ψ)
  (hsurj : Function.Surjective ⇑ψ) (hker : Disjoint ψ.ker (TauCeti.fixedSubgroup F)) :
  TauCeti.FixedPointCandidate F ≃* TauCeti.FixedPointCandidate F'

Lean

Formalized in Tau Ceti as TauCeti.FixedPointCandidate.congrOfFiniteKer.

Sources

• Tau Ceti documentation: TauCeti.FixedPointCandidate.congrOfFiniteKer
• Source of TauCeti.FixedPointCandidate.congrOfFiniteKer in TauCeti/GroupTheory/FixedPointCandidate/FiniteKernel.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.FixedPointCandidate.congrOfFiniteKer

TheoremTwo morphisms out of the short-root type-F₄ carrier agree as soon as they agree on its eight numbered root subgroups#

This drops the weight-torus hypothesis of TauCeti.F4ShortRoot.groupScheme_hom_ext, which root generation of the carrier makes redundant.

TauCeti.F4ShortRoot.groupScheme_hom_ext_of_rootSubgroup {Y : CommHopfAlgCat ℤ}
  (f g : TauCeti.F4ShortRoot.groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y))
  (hroot :
    ∀ (k : Fin 4 ⊕ Fin 4),
      CategoryTheory.CategoryStruct.comp (TauCeti.F4ShortRoot.rootSubgroup k) f =
        CategoryTheory.CategoryStruct.comp (TauCeti.F4ShortRoot.rootSubgroup k) g) :
  f = g

Lean

Formalized in Tau Ceti as TauCeti.F4ShortRoot.groupScheme_hom_ext_of_rootSubgroup.

Sources

• Tau Ceti documentation: TauCeti.F4ShortRoot.groupScheme_hom_ext_of_rootSubgroup
• Source of TauCeti.F4ShortRoot.groupScheme_hom_ext_of_rootSubgroup in TauCeti/Algebra/Lie/F4/ShortRoot/Generation.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.F4ShortRoot.groupScheme_hom_ext_of_rootSubgroup

Uses 1

Proof usesChevalley's rank-one identity

TheoremThe compiled word denotes the direct interpretation of the relator expression#

Consequently, a reviewer may check the structured Relator against a published presentation while the eventual PresentedGroup safely uses FreeGroup.mk r.toWord as its defining relation.

TauCeti.Relator.toWord_toFreeGroup.{u_1} {α : Type u_1} (r : TauCeti.Relator α) :
  FreeGroup.mk r.toWord = r.toFreeGroup

Lean

Formalized in Tau Ceti as TauCeti.Relator.toWord_toFreeGroup.

Sources

• Tau Ceti documentation: TauCeti.Relator.toWord_toFreeGroup
• Source of TauCeti.Relator.toWord_toFreeGroup in TauCeti/GroupTheory/Presentation/Relator.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.Relator.toWord_toFreeGroup

Used by 1

Used byTauCeti.GroupPresentation.homEquiv

DefinitionTauCeti.GroupPresentation.homEquiv#

Homomorphisms from a finite presentation correspond to generator assignments satisfying its transcribed relators. No generation or injectivity condition is imposed on the assignment.

TauCeti.GroupPresentation.homEquiv.{u_1} (P : TauCeti.GroupPresentation) {G : Type u_1} [Group G] :
  (P.Group →* G) ≃ { f // ∀ t ∈ P.transcribed, (FreeGroup.lift f) t.toFreeGroup = 1 }

Lean

Formalized in Tau Ceti as TauCeti.GroupPresentation.homEquiv.

Sources

• Tau Ceti documentation: TauCeti.GroupPresentation.homEquiv
• Source of TauCeti.GroupPresentation.homEquiv in TauCeti/GroupTheory/Presentation/GroupPresentation.lean
• Tau Ceti roadmap status: Stating the classification of finite simple groups

LeanTauCeti.GroupPresentation.homEquiv

Uses 1

Proof usesThe compiled word denotes the direct interpretation of the relator expression

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.