A transcribed presentation of the first Conway group #
This file carries the Co₁ row of the sporadic presentation data required by milestone S1 of
TauCetiRoadmap/CFSGStatement/README.md. It records presentation GPLTable.Co1.1 from Roderik
Lindenbergh's Group Presentations Library as a TauCeti.GroupPresentation, together with the exact
source, generator convention, transcription notes, expected counts, and decidable checks on the
transcription.
The presentation uses the Coxeter graph encoded by
b4h3a3b5c3d3f4c3e4a, b4g4f, e6f6h.
All eight generators are involutions and every omitted edge has label two. Thus the graph contributes eight square relations, thirteen labeled-edge relations, and fifteen omitted-edge relations. The source then appends
a = (cf)², e = (bg)², b = (ef)³, d = (bh)², d = (eah)³,
(adfh)³, (baefg)³, (cef)⁷, (adefcefgh)³⁹.
An equality x = y in the source is the relator x⁻¹y. The complete presentation therefore has
45 relators, whose compiled words have 611 signed letters. The theorems below check both figures
from the transcribed expressions.
The library identifies this record as a presentation of Co₁ originating in Praeger--Soicher,
whose construction uses low-rank representations and graphs for sporadic groups. The stored data
is a full presentation of the abstract group, not a semi-presentation for recognizing generators
in an already constructed group. This file asserts no order, finiteness, simplicity, or
identification result.
Independent source-to-Lean read-through #
An independent read-through used the bytes of gpl.g whose SHA-256 digest is
8b90a7a65317a585b5b74d015083bd2fa3db8a969c117a220d00d7e8773103c8. The exact source record is
presdef := [ "b4h3a3b5c3d3f4c3e4a,b4g4f,e6f6h", ,
"a=(cf)^2,e=(bg)^2,b=(ef)^3,d=(bh)^2,d=(eah)^3,\
(adfh)^3,(baefg)^3,(cef)^7,(adefcefgh)^(39)",, ],
GetGenerators gives the decoder's first-occurrence order b,h,a,c,d,f,e,g; the Lean row instead
uses the alphabetical order a,b,c,d,e,f,g,h. After that explicit renaming, DeCoxList and its
calls to AddTrivialRelations and AddNonEdgeRelations give the same relation multiset recorded by
co1Presentation_relatorLetters, regrouped by kind. Entries 1--8 are the eight generator squares;
entries 9--21 are
(ab)^3,(ae)^4,(ah)^3,(bc)^5,(bg)^4,(bh)^4,(cd)^3,
(ce)^3,(cf)^4,(df)^3,(ef)^6,(fg)^4,(fh)^6;
and entries 22--36 are the exponent-two nonedges
ac,ad,af,ag, bd,be,bf, cg,ch, de,dg,dh, eg,eh, gh.
MakeWordList compiles an equality x = y as x⁻¹y. Entries 37--45 are therefore, in source
order, a⁻¹(cf)², e⁻¹(bg)², b⁻¹(ef)³, d⁻¹(bh)², d⁻¹(eah)³, (adfh)³, (baefg)³,
(cef)⁷, and (adefcefgh)³⁹. There is no change to any word or exponent and no dropped or
duplicated relation, only the presentation-irrelevant renaming and regrouping just described. This
closes the row's S1 source-to-Lean read-through.
The independent FiniteSimpleGroups comparison does not apply: at commit
7f09e33a9ceef6b59ce03e34cd4f0558c763e325, that development has sporadic constructions for
Co₂ and Co₃ but not Co₁.
The row is a sealed definition, so it publishes an equation for each of its fields: the transcribed
relator expressions with their generator indices written out and this file's three private relator
lists concatenated, and the provenance a manifest row exists to record. Together with
TauCeti.GroupPresentation.relators_def and TauCeti.GroupPresentation.mem_relatorSet_iff the
first of those determines the compiled words and the relations defining the presented group, so a
consumer reasons about the row without unfolding it.
These field equations and the decidable checks beside them follow the shape that the
TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.Janko modules established for a manifest row.
Main definitions and results #
TauCeti.Sporadic.co1Presentation: the GPL finite presentation of the first Conway groupCo₁.TauCeti.Sporadic.co1Presentation_transcribedand the equations for the remaining fields: the characterization of the sealed row.TauCeti.Sporadic.co1Presentation_relatorLetters: the forty-five compiled words checked against the decoder output in the independent source-to-Lean read-through.TauCeti.Sporadic.co1Presentation_map_length_relators,TauCeti.Sporadic.co1Presentation_totalLengthandTauCeti.Sporadic.co1Presentation_relatorsCyclicallyReduced: the three checks on the compiled words.
References #
- R. Lindenbergh, Group Presentations Library, version 1.0, record
GPLTable.Co1.1, https://doris.tudelft.nl/~rlindenbergh/GPL/gpl.g. - C. E. Praeger and L. H. Soicher, Low Rank Representations and Graphs for Sporadic Groups, Cambridge University Press, 1997, Chapter 4, doi:10.1017/CBO9780511526039.005.
- KitaKen1,
finite-simple-groups-lean, commit7f09e33a9ceef6b59ce03e34cd4f0558c763e325, https://github.com/KitaKen1/finite-simple-groups-lean/tree/7f09e33a9ceef6b59ce03e34cd4f0558c763e325/FiniteSimpleGroups/Sporadic.
The Group Presentations Library finite presentation GPLTable.Co1.1 of the first Conway
group Co₁ on generators a, b, c, d, e, f, g, and h.
The source describes this as a full presentation of the abstract group and identifies its origin as Praeger--Soicher. No structural property of the presented group is asserted here: this definition records only the cited generators and relations.
Generator order (starting at index zero): a, b, c, d, e, f, g, h.
Source: R. Lindenbergh, Group Presentations Library, version 1.0; presentation attributed there to C. E. Praeger and L. H. Soicher, Low Rank Representations and Graphs for Sporadic Groups, Cambridge University Press, 1997.
Source locator: GPLTable.Co1.1 in https://doris.tudelft.nl/~rlindenbergh/GPL/gpl.g; Praeger--Soicher, Chapter 4, doi:10.1017/CBO9780511526039.005
Generator convention: The source generators are indexed alphabetically in Lean: indices 0 through
7 are a,b,c,d,e,f,g,h. This is a relabeling of the GPL decoder's first-occurrence map
b,h,a,c,d,f,e,g and preserves every named relation. A Coxeter path declares each node to be an
involution, a labeled edge x-m-y declares (x*y)^m = 1, and an omitted edge declares (x*y)^2 =
- An equality x = y compiles to
x^-1*y, and products are read left to right.
Transcription notes: Expand the paths b4h3a3b5c3d3f4c3e4a, b4g4f, and e6f6h to eight square relations, thirteen labeled-edge relations, and fifteen omitted-edge relations. Append the nine words in presdef[3], interpreting each equality as left-hand inverse times right-hand side, and reindex the named generators alphabetically. The expected relator count and total length are derived from this exact expansion. The module documentation records the completed itemized source-to-Lean read-through. FiniteSimpleGroups does not cover Co1, so its separate permutation-group comparison does not apply.
Instances For
The number of generators in the presentation of Co₁. The row's body is sealed, so this is
what lets a
consumer see that it is an eight-generator presentation.
The relator count Co₁'s source states; see
TauCeti.Sporadic.co1Presentation_generatorCount.
The relator expressions transcribed for Co₁, with their generator indices written out and the
three private relator lists of this file concatenated.
The row's body is sealed, so this is the equation that characterizes it: with
TauCeti.GroupPresentation.relators_def it determines the compiled words, and with
TauCeti.GroupPresentation.mem_relatorSet_iff it determines the relations defining
TauCeti.GroupPresentation.Group, so a consumer never has to unfold the row. Indices 0 through
7 are the involutions a through h, and the bounds come from
TauCeti.Sporadic.co1Presentation_generatorCount.
The compiled relator words of Co₁, generated from the nodes, edges, nonedges, and nine
additional words of GPLTable.Co1.1. A letter (i, true) is generator i, while (i, false) is
its inverse.
The relator count recorded for Co₁ agrees with the transcribed data.
The lengths of the forty-five compiled relator words for Co₁, in the order in which the three
Coxeter paths and the nine trailing words are decoded.
Reading the counts off one relator at a time is what lets a reviewer locate a discrepancy, rather
than only observe one in the total of TauCeti.Sporadic.co1Presentation_totalLength, which sums
exactly this list. The lengths are computed through TauCeti.Relator.length_toWord, which
multiplies rather than repeats, so the thirty-ninth power at the end never has to be expanded.
The compiled relators of the Co₁ presentation contain 611 signed letters in total: the sum
of the per-relator lengths of TauCeti.Sporadic.co1Presentation_map_length_relators.
Every compiled Co₁ relator is cyclically reduced, hence by
FreeGroup.IsCyclicallyReduced.isReduced freely reduced, so the letter count recorded by
TauCeti.Sporadic.co1Presentation_totalLength is comparable with a published presentation length,
which is normally measured on freely reduced relators.