Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.Presentation

Presentations of the sporadic groups #

This file assembles the twenty-six independently transcribed sporadic-group presentations into the total function TauCeti.SporadicName.presentation. Each branch is the explicit, cited TauCeti.GroupPresentation defined in its group-specific module. The theorem TauCeti.presentation_matchesMetadata combines the individual relator-count checks, while TauCeti.SporadicName.Group is the concrete group defined by the selected presentation.

This is milestone S1 of TauCetiRoadmap/CFSGStatement/README.md. The dispatcher and its interface follow the target signatures in the human-authored roadmap's CFSGStatement/Suggested.lean; the mathematical and bibliographic sources for each presentation are recorded in the corresponding imported module.

Main definitions #

Main results #

source
def TauCeti.SporadicName.presentation :
SporadicName → GroupPresentation

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

Instances For
    source
    @[simp]
    theorem TauCeti.SporadicName.presentation_J1 :
    J1.presentation = Sporadic.j1Presentation

    The presentation selected for the first Janko group is the transcribed ATLAS presentation.

    source
    @[simp]
    theorem TauCeti.SporadicName.presentation_HS :
    HS.presentation = Sporadic.hsPresentation

    The selected Higman--Sims presentation is the transcribed ATLAS presentation HSG1-P1.

    source
    theorem TauCeti.presentation_matchesMetadata (s : SporadicName) :
    s.presentation.matchesMetadata

    Every sporadic presentation has the relator count stated in its metadata.

    This is deliberately not @[simp]: GroupPresentation.matchesMetadata_iff is itself a simp lemma, so the left-hand side s.presentation.matchesMetadata simplifies to the count equation and is not in simp normal form, which the simpNF linter rejects. Apply the theorem directly, or pass it to simp as an argument.

    source
    @[simp]
    theorem TauCeti.SporadicName.presentation_M11 :
    M11.presentation = Sporadic.m11Presentation

    The presentation selected for M₁₁ is the transcribed presentation TauCeti.Sporadic.m11Presentation. The body of TauCeti.SporadicName.presentation is not exposed to importing modules, so this equation is how they reach it.

    source
    @[simp]
    theorem TauCeti.SporadicName.presentation_M12 :
    M12.presentation = Sporadic.m12Presentation

    The presentation selected for M₁₂ is the transcribed presentation TauCeti.Sporadic.m12Presentation. The body of TauCeti.SporadicName.presentation is not exposed to importing modules, so this equation is how they reach it.

    source
    @[simp]
    theorem TauCeti.SporadicName.presentation_M22 :
    M22.presentation = Sporadic.m22Presentation

    The presentation selected for M₂₂ is the transcribed Conder–Havas–Ramsay presentation TauCeti.Sporadic.m22Presentation.

    source
    @[reducible, inline]
    abbrev TauCeti.SporadicName.Group (s : SporadicName) :
    Type

    The sporadic group concretely defined by its selected finite presentation.

    Instances For
      source
      @[simp]
      theorem TauCeti.SporadicName.presentation_M24 :
      M24.presentation = Sporadic.m24Presentation

      The presentation selected for M₂₄ is the transcribed ATLAS presentation TauCeti.Sporadic.m24Presentation. The body of TauCeti.SporadicName.presentation is not exposed to importing modules, so this equation is how they reach it.

      source
      @[simp]
      theorem TauCeti.SporadicName.presentation_McL :
      McL.presentation = Sporadic.mclPresentation

      The presentation selected for McL is the transcribed ATLAS presentation TauCeti.Sporadic.mclPresentation.

      source
      @[simp]
      theorem TauCeti.SporadicName.presentation_J2 :
      J2.presentation = Sporadic.j2Presentation

      The presentation selected for J₂ is Stoytchev's transcribed presentation TauCeti.Sporadic.j2Presentation.