A transcribed presentation of the second Fischer group #
This file records presentation GPLTable.Fi23.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
a --3-- b --3-- c --3-- d --3-- e --3-- f --3-- g --3-- j
|
3
|
h --3-- i
where all ten generators are involutions and every omitted edge has label 2. The source encodes
this graph by the two paths a3b3c3d3e3f3g3j,d3h3i. It then appends
(d c b d e f d h i)^10, (a b c d e f h)^9.
Thus the graph contributes ten square relations, nine label-three relations, and thirty-six
omitted-edge relations. With the two appended words, the presentation has 57 relators and its
compiled words have 371 signed letters. The theorems below check those figures and cyclic
reduction from the transcribed data.
The library identifies this record as a presentation of Fi₂₃ originating in Praeger--Soicher,
whose construction uses low-rank representations and graphs for sporadic groups. As a separate
computational check, GAP 4.15.1 enumerates 31671 cosets of the subgroup generated by a through
i; the source identifies that subgroup as 2·Fi₂₂, and 31671 is its index in Fi₂₃. This
computation is provenance rather than a Lean theorem: this file asserts no order, finiteness,
simplicity, or identification result.
The source record #
The record is taken from the bytes of gpl.g with SHA-256 digest
8b90a7a65317a585b5b74d015083bd2fa3db8a969c117a220d00d7e8773103c8:
presdef := [ "a3b3c3d3e3f3g3j,d3h3i", ,
"(dcbdefdhi)^(10),(abcdefh)^9",, ],
With GPL_PCE := true, DeCoxList and its calls to AddTrivialRelations and
AddNonEdgeRelations expand that record. The theorem below records the same relations regrouped
by kind: entries 1--10 are the squares of a,b,c,d,e,f,g,h,i,j; entries 11--19 are
(ab)³,(bc)³,(cd)³,(de)³,(ef)³,(fg)³,(gj)³,(dh)³,(hi)³; and entries 20--55 are the exponent-two
pairs
ac,ad,ae,af,ag,ah,ai,aj, bd,be,bf,bg,bh,bi,bj, ce,cf,cg,ch,ci,cj,
df,dg,di,dj, eg,eh,ei,ej, fh,fi,fj, gh,gi, hj,ij.
Entries 56 and 57 are (dcbdefdhi)¹⁰ and (abcdefh)⁹. Translating source letters to zero-based
generator indices in alphabetical order gives exactly fi23Presentation_relatorLetters: there is
no change to any word or exponent and no dropped or duplicated relation, only the
presentation-irrelevant regrouping by kind just described.
The row publishes an equation for each of its fields: the transcribed relator expressions with
their generator indices written out, 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.
The graph itself, and not only its expansion #
The graph is recorded directly as the edge list TauCeti.Sporadic.fi23Edges and the simply laced
Coxeter matrix it determines. The generated Coxeter relations are compared with the transcribed
relations by compiled-word membership, accounting for their different expressions and ordering.
The row presents the quotient of the Coxeter group of its graph obtained by imposing the two additional relations from the source.
Main definitions and results #
TauCeti.Sporadic.fi23Presentation: the GPL finite presentation of the Fischer groupFi₂₃.TauCeti.Sporadic.fi23Presentation_transcribedand the equations for the remaining fields: the characterization of the row.TauCeti.Sporadic.fi23Presentation_relatorLetters: the fifty-seven compiled words, in the form the source record expands to (see "The source record").TauCeti.Sporadic.fi23Presentation_map_length_relators,TauCeti.Sporadic.fi23Presentation_totalLengthandTauCeti.Sporadic.fi23Presentation_relatorsCyclicallyReduced: the three checks on the compiled words.TauCeti.Sporadic.fi23EdgesandTauCeti.Sporadic.fi23CoxeterMatrix: the graph the source's two paths encode, and its Coxeter matrix.TauCeti.Sporadic.fi23Presentation_mem_map_toWord_iff: the transcribed relations are the ones that matrix generates, together with the two appended words.TauCeti.Sporadic.fi23MulEquivPresentedGroupCoxeterAppend: the row presents the Coxeter group of the graph cut down by those two words.
References #
- R. Lindenbergh, Group Presentations Library, version 1.0, record
GPLTable.Fi23.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.
- The presentation-row characterization and audit theorem scaffold is adapted from the Janko-row formalization in https://github.com/TauCetiProject/TauCeti/pull/5283.
The nine edges, in source order. The body is sealed, so this equation is what lets a consumer
reduce the graph — and with it the membership test of
TauCeti.Sporadic.fi23CoxeterMatrix_apply — to the pairs the source's two paths draw.
The Coxeter matrix of the Fi₂₃ graph, the simply laced matrix of its edge list: diagonal
entries are one, an edge has label three, and every other pair has label two. This is the
m-labelled data the source's two paths encode, before any expansion into relations.
Instances For
The two words following the Coxeter paths in GPLTable.Fi23.1: the source appends them to the
relations its diagram encodes.
Instances For
The two appended words, with their generator indices written out. The body is sealed and is
written with this file's private letter abbreviations, so this equation is what publishes the two
words (dcbdefdhi)¹⁰ and (abcdefh)⁹ themselves.
The Group Presentations Library finite presentation GPLTable.Fi23.1 of the Fischer group
Fi₂₃ on generators a, b, c, d, e, f, g, h, i, and j.
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, i, j.
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.Fi23.1 in https://doris.tudelft.nl/~rlindenbergh/GPL/gpl.g; Praeger--Soicher, Chapter 4, doi:10.1017/CBO9780511526039.005
Generator convention: Generators are indexed alphabetically, a,b,c,d,e,f,g,h,i,j as 0 through 9,
the order of the generator set that DeCoxList builds; GPL's FpGroupViaStrings instead numbers them
by first occurrence, a,b,c,d,e,f,g,j,h,i. 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 = 1. Products
are read left to right.
Transcription notes: Expand the paths a3b3c3d3e3f3g3j and d3h3i to ten square relations, nine labeled-edge relations, and thirty-six omitted-edge relations. Append the two words in presdef[3]. The expected relator count and total length are derived from this exact expansion. The module documentation lists the expansion relation by relation. GAP 4.15.1 enumerates 31671 cosets of the subgroup generated by a through i, which the source labels 2.Fi22.
Instances For
The number of generators in the presentation of Fi₂₃. This is what lets a consumer see that
it is a
ten-generator presentation, and it is what bounds the generator indices of
TauCeti.Sporadic.fi23Presentation_transcribed.
The relator count derived from Fi₂₃'s source expansion. With
TauCeti.Sporadic.fi23Presentation_transcribed this is what makes
TauCeti.Sporadic.fi23Presentation_matchesMetadata an equation between two visible numbers.
The relator expressions transcribed for Fi₂₃, with their generator indices written out and
the local abbreviations and grouping lists of this file expanded.
This is the equation that characterizes the row: 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
9 are the generators a through j, and the bounds come from
TauCeti.Sporadic.fi23Presentation_generatorCount.
The compiled relator words of Fi₂₃, generated from the nodes, edges, nonedges, and two
additional words of GPLTable.Fi23.1. A letter (i, true) is generator i; all source letters
are positive.
The lengths of the fifty-seven compiled relator words for Fi₂₃, in the transcription's order,
which groups the expansion by kind: ten involutions, nine labeled edges, thirty-six omitted edges,
and the two appended relators.
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.fi23Presentation_totalLength.
The relator count recorded for Fi₂₃ agrees with the transcribed data.
The compiled relators of the Fi₂₃ presentation contain 371 signed letters in total.
Every compiled relator of the Fi₂₃ presentation is cyclically reduced.
The row against the Coxeter group of its graph #
The transcribed relations are exactly the ones the source's Coxeter graph encodes, together with the two appended words.
The row transcribes the source's two paths by hand, as ten square relations, nine labelled-edge
relations and thirty-six omitted-edge relations. This compares that expansion, letter by letter,
with the relations generated from TauCeti.Sporadic.fi23CoxeterMatrix, so the expansion is
checked against the graph rather than only read against it. The comparison is of compiled-word
membership rather than expressions or multiplicities, because the row writes an involution
relation as sᵢ ^ 2 where the generated list writes (sᵢ sᵢ) ^ 1 and groups its relations by
kind.
The row presents the Coxeter group of its graph cut down by the two appended relations, which is the shape in which the source states the presentation: a Coxeter graph, given by two paths, followed by two words.
This is an identification of the presented group with a quotient built from Mathlib's
CoxeterMatrix.relationsSet; it asserts nothing about the order or the structure of either
side.
Instances For
The Coxeter equivalence sends each canonical generator to the corresponding canonical generator.