A transcribed presentation of the Lyons group

This file carries the Ly row of the sporadic presentation data TauCeti.SporadicName.presentation. It records Sims' presentation of the Lyons sporadic group, in the amended form published by Havas and Sims, as a TauCeti.GroupPresentation, together with its source, conventions, expected counts, and decidable checks.

The source presents Ly on the five generators a, b, c, d, z together with thirty-four auxiliary generators, all of them words in a, b, c, d, by eighty-six relators and relations (14.1) to (14.86). Following the source's own recipe for coset enumeration, this row keeps the six generators a, b, c, d, e, z, substitutes the auxiliary generators c₁, ..., c₅, a₁, ..., a₄, u and x₂₃, ..., x₃₇₁ by their defining words (14.6) to (14.10) and (14.45) to (14.72), and keeps the remaining fifty-three relators in the source's order: (14.1) to (14.5), (14.11) to (14.28), (14.29) to (14.44), and (14.73) to (14.86). The generator e is retained because the source retains it, defined by (14.29). This is the fifty-three-relator presentation on a, b, c, d, e, z that Section 14.4 of the source describes and enumerates.

The source writes x^y for y⁻¹xy, which is TauCeti.Relator.conj, and (x, y) for x⁻¹y⁻¹xy, which is TauCeti.Relator.commInvInv; a displayed equation r = s is compiled as the relator r s⁻¹, which is TauCeti.Relator.div. Each auxiliary word is a named abbreviation, so that every relator is displayed in the source's own shape.

Source-to-Lean read-through

The relators were read from a 300 dpi rendering of the published PDF of the chapter, whose SHA-256 digest is recorded in presentation. Every relator and every auxiliary definition was compared with the print letter for letter.

Verification outside Lean

The source proves that this presentation defines Ly by a coset enumeration of the 8835156 cosets of the subgroup generated by a, b, c, d, together with the identification of that subgroup with G₂(5); that the permutation representation this enumeration produces is the Lyons group is shown by Gollan and Havas, to whom the source refers after its Lemma 14.6. That enumeration was reproduced with the coset enumerator ACE on the relators exactly as compiled from this file: the enumeration closes at index 8835156 with the maximum number of cosets defined equal to the index, and the subgroup generated by a, b, c has index 3906 in the group presented by the z-free relators. This is provenance rather than a Lean theorem: the file asserts no order, finiteness, simplicity, or identification result.

Three of the fifty-three relators are not cyclically reduced after free reduction: the commutator relations (14.14), (14.18), and (14.19) freely reduce to words that begin and end with a cancelling pair of letters, because their two sides share a conjugating prefix. The cyclic-reducedness check stated by other rows is therefore not stated here; it exists to compare a reduced letter count with a published presentation length, and this source prints none.

Gebhardt's shorter twenty-five-relator presentation (Experimental Mathematics 9 (2000), 333--338) is not used: the paper's fourth R_G relator is misprinted, and the coset enumeration underlying the present source is reproducible.

Main definitions and results

• TauCeti.Sporadic.Lyons.presentation: the Havas--Sims finite presentation of Ly.
• TauCeti.Sporadic.Lyons.presentation_transcribed and the equations for the remaining fields: the characterization of the sealed row, with the source's auxiliary words as let-bound abbreviations.
• TauCeti.Sporadic.Lyons.matchesMetadata_presentation, TauCeti.Sporadic.Lyons.map_length_relators_presentation and TauCeti.Sporadic.Lyons.reducedTotalLength_presentation: the transcription checks.

References

• G. Havas and C. C. Sims, A presentation for the Lyons simple group, in: Computational Methods for Representations of Groups and Algebras (Essen, 1997), Progress in Mathematics 173, Birkhäuser, Basel, 1999, 241--249, https://doi.org/10.1007/978-3-0348-8716-8_14.
• C. C. Sims, The existence and uniqueness of Lyons' group, in: Finite Groups '72, North-Holland Mathematics Studies 7, 1973, 138--141.
• H. W. Gollan and G. Havas, On Sims' presentation for Lyons' simple group, in: Computational Methods for Representations of Groups and Algebras (Essen, 1997), Progress in Mathematics 173, Birkhäuser, Basel, 1999, Chapter 13.
• V. Gebhardt, Two Short Presentations for Lyons' Sporadic Simple Group, Experimental Mathematics 9 (2000), 333--338, https://doi.org/10.1080/10586458.2000.10504410.

def TauCeti.Sporadic.Lyons.presentation : GroupPresentation

Sims' presentation of the Lyons sporadic group Ly, as amended by Havas and Sims, on the six generators a, b, c, d, e, z.

The source proves that these relators present Ly (Theorem 14.2): a coset enumeration of the 8835156 cosets of the subgroup generated by a, b, c, d yields a permutation representation, which Gollan and Havas identify with the Lyons group. No structural property of the resulting PresentedGroup is asserted here; the definition records only the generators and relators.

Generator order (starting at index zero): a, b, c, d, e, z.

Source: G. Havas and C. C. Sims, A presentation for the Lyons simple group, in Computational Methods for Representations of Groups and Algebras (Essen, 1997), Progress in Mathematics 173, Birkhauser, Basel, 1999, 241-249.

Source locator: Section 14.2, relators and relations (14.1) to (14.86), pp. 242-244; doi:10.1007/978-3-0348-8716-8_14; SHA-256 of the chapter PDF db0f8a96b79392b590982505ab32224890e548cc957239d03fc3f8f68949e1df

Generator convention: The source's generators a, b, c, d, e, z, in that order, so indices 0 to 5 denote a, b, c, d, e, z. The source writes x^y for y^-1*x*y and (x, y) for x^-1*y^-1*x*y, and products are read left to right.

Transcription notes: The source presents Ly on a, b, c, d, z and thirty-four auxiliary generators, all words in a, b, c, d, by relators (14.1) to (14.86). This row follows the source's Section 14.4: it keeps the six generators a, b, c, d, e, z, substitutes the auxiliary generators c1 to c5, a1 to a4, u and x23 to x371 by their defining relations (14.6) to (14.10) and (14.45) to (14.72), and keeps the remaining fifty-three relators in source order, namely (14.1) to (14.5), (14.11) to (14.28), (14.29) to (14.44) and (14.73) to (14.86). An equation r = s is compiled as r*s^-1. Free reduction gives total length 975; the source prints no length. Coset enumeration with ACE on these compiled relators closes at index 8835156 over the subgroup generated by a, b, c, d, with maximum cosets equal to the index.

@[simp]

theorem TauCeti.Sporadic.Lyons.presentation_generatorCount : presentation.generatorCount = 6

The number of generators in the presentation of Ly.

@[simp]

theorem TauCeti.Sporadic.Lyons.presentation_expectedRelatorCount : presentation.expectedRelatorCount = 53

The relator count recorded for Ly.

@[simp]

theorem TauCeti.Sporadic.Lyons.presentation_transcribed : presentation.transcribed = have a := Relator.gen ⟨0, presentation_transcribed._proof_2⟩; have b := Relator.gen ⟨1, presentation_transcribed._proof_3⟩; have c := Relator.gen ⟨2, presentation_transcribed._proof_4⟩; have d := Relator.gen ⟨3, presentation_transcribed._proof_5⟩; have e := Relator.gen ⟨4, presentation_transcribed._proof_6⟩; have z := Relator.gen ⟨5, presentation_transcribed._proof_7⟩; have cOne := c; have cTwo := c.conj a; have cThree := c.conj b; have cFour := c.conj b.inv; have cFive := cOne.commInvInv cTwo; have aOne := a; have aTwo := a.conj b.inv; have aThree := a.conj (b.inv.pow 2); have aFour := a.conj (b.pow 2); have u := a.pow 2; have x23 := d; have x24 := d.inv; have x25 := (((((((((((((((b.pow 2).mul a.inv).mul b.inv).mul a.inv).mul (b.pow 2)).mul c.inv).mul a).mul c).mul a.inv).mul c.inv).mul d).mul c.inv).mul (b.pow 2)).mul a.inv).mul c).mul b; have x29 := (((((((((((((((((a.mul b).mul a.inv).mul (b.pow 2)).mul a.inv).mul (b.pow 2)).mul c.inv).mul a).mul c).mul b).mul c).mul b.inv).mul d).mul c).mul (b.inv.pow 2)).mul d).mul c).mul b).mul c; have x47 := ((((((c.inv.mul d.inv).mul a.inv).mul c.inv).mul a.inv).mul b).mul c.inv).mul d.inv; have x96 := b.mul d; have x129 := d.inv.mul b.inv; have x162 := ((((((((a.inv.mul b.inv).mul a.inv).mul b).mul c.inv).mul b.inv).mul a).mul c.inv).mul b).mul a; have x163 := ((((((b.inv.pow 2).mul a).mul c).mul a.inv).mul b).mul c).mul b; have x164 := (((((a.inv.mul b.inv).mul a.inv).mul c).mul a).mul b).mul a; have x165 := (((((b.inv.mul a.inv).mul b).mul c).mul b.inv).mul a).mul b; have x166 := ((((((((b.pow 2).mul a.inv).mul b.inv).mul c).mul b).mul a).mul c).mul (b.inv.pow 2)).mul c.inv; have x167 := a.inv.pow 3; have x168 := ((b.mul a.inv).mul b.inv).mul (a.inv.pow 2); have x169 := (((a.mul (b.pow 2)).mul a).mul (b.inv.pow 2)).mul a.inv; have x364 := (((((((((((((((((a.inv.mul d).mul b.inv).mul c.inv).mul a.inv).mul b).mul c.inv).mul d.inv).mul b).mul c.inv).mul b.inv).mul a.inv).mul c.inv).mul a).mul b.inv).mul a).mul b).mul a).mul b.inv; have x365 := (((((((((((((((a.mul (b.inv.pow 2)).mul a.inv).mul c).mul b).mul c.inv).mul b).mul a.inv).mul (c.inv.pow 2)).mul d).mul c).mul a).mul c).mul a.inv).mul c).mul b.inv).mul d.inv; have x366 := ((((((((((((((((b.mul a).mul b.inv).mul a.inv).mul (b.inv.pow 2)).mul a.inv).mul b.inv).mul c).mul (b.pow 2)).mul c).mul b).mul d).mul c).mul (b.inv.pow 2)).mul d).mul c).mul b).mul c; have x367 := ((((((((((((((((c.inv.mul b.inv).mul c.inv).mul d.inv).mul (b.pow 2)).mul c.inv).mul d.inv).mul b.inv).mul c.inv).mul (b.inv.pow 2)).mul c.inv).mul b).mul a).mul (b.pow 2)).mul a).mul b).mul a.inv).mul b.inv; have x368 := ((((((((((((((((a.inv.mul c.inv).mul d.inv).mul a).mul c.inv).mul b.inv).mul a).mul c.inv).mul d.inv).mul a.inv).mul c.inv).mul a).mul c).mul (b.inv.pow 2)).mul c.inv).mul b.inv).mul a.inv).mul (b.inv.pow 2); have x369 := (((((((((((((((a.inv.mul c.inv).mul d.inv).mul b).mul a.inv).mul b.inv).mul c.inv).mul d.inv).mul b).mul a.inv).mul b.inv).mul c.inv).mul b.inv).mul a).mul (b.inv.pow 2)).mul a).mul b.inv; have x370 := (((((((((((⋯.mul a.inv).mul c.inv).mul d.inv).mul a).mul b.inv).mul a.inv).mul c).mul a.inv).mul (b.inv.pow 2)).mul a.inv).mul b).mul a.inv; have x371 := ((((((((((⋯.mul d.inv).mul c).mul a.inv).mul c).mul a).mul c).mul b.inv).mul a.inv).mul b.inv).mul a.inv).mul b; have y := have y := have y := [(aThree.conj z).div x169, (z.pow 2).div u, ((aFour.mul z).pow 3).mul u, ((((x47.mul z).mul x364).mul z).mul x368).mul z, ((⋯.mul x23).mul z).mul x29, (⋯.mul z.inv).mul x370, ⋯.mul x371]; (cOne.conj z).div x162 :: (cTwo.conj z).div x163 :: (cThree.conj z).div x164 :: (cFour.conj z).div x165 :: (cFive.conj z).div x166 :: (aOne.conj z).div x167 :: (aTwo.conj z).div x168 :: y; have y := ((((((((e.mul cTwo).mul e).mul cTwo.inv).mul e).mul cTwo).mul cFour.inv).mul a).mul cThree).mul (a.pow 3) :: d.div (((((⋯.mul e).mul a).mul cTwo.inv).mul b).mul e) :: (d.pow 2).div (a.pow 4) :: b.commInvInv d :: (a.conj d).div (a.pow 3) :: (d.mul cFive).pow 5 :: ⋯.mul (a.inv.pow 2) :: y; (cThree.conj e).div ((((((b.pow 2).mul a).mul cTwo).mul cOne.inv).mul cFour.inv).mul a.inv) :: (cFour.conj e).div (((b.pow 2).mul cThree.inv).mul cFour) :: (cFive.conj e).div (((cOne.mul cThree.inv).mul cOne).mul cFour.inv) :: ((e.mul (a.pow 2)).mul e).div (((⋯.mul cOne).mul cFive).mul cFour.inv) :: (b.conj e).div ((cOne.mul cThree.inv).mul (cFour.inv.pow 2)) :: (⋯.mul e).div ((((a.pow 2).mul cOne).mul cFive).mul cFour.inv) :: y; have y := have y := (cFive.conj a).div (cFive.pow 2) :: (cTwo.conj b).div ((((cTwo.mul cThree).mul cFour.inv).mul cOne.inv).mul cFour.inv) :: (cThree.conj b).div (((cOne.pow 2).mul cFour).mul (cThree.inv.pow 2)) :: (cFive.conj b).div cFive :: e.div ((⋯.mul cOne).mul d) :: e.pow 2 :: (cOne.conj e).div (((b.mul cThree).mul b).mul cOne.inv) :: y; (cTwo.commInvInv cThree).div cFive.inv :: cTwo.commInvInv cFour :: (cThree.commInvInv cFour).div cFive.inv :: (cTwo.conj a).div (cOne.inv.pow 2) :: (cThree.conj a).div (((cThree.inv.pow 2).mul cOne).mul cFour) :: (cFour.conj a).div (((((cOne.mul cTwo.inv).mul cThree.inv).mul cFour).mul cOne).mul cFour) :: y; have y := cFive.pow 5 :: cOne.commInvInv cFive :: cTwo.commInvInv cFive :: cThree.commInvInv cFive :: cFour.commInvInv cFive :: (cOne.commInvInv cThree).div (cFive.inv.pow 2) :: (cOne.commInvInv cFour).div (cFive.pow 2) :: y; a.pow 8 :: b.pow 5 :: (a.mul b).pow 4 :: (a.pow 2).commInvInv b :: (a.commInvInv b).pow 3 :: cOne.pow 5 :: y

The transcribed relators of the row, spelled out in the source's own shape: the six generators, the source's auxiliary words as let-bound abbreviations, and the fifty-three relators in the source's order (14.1) to (14.5), (14.11) to (14.28), (14.29) to (14.44), (14.73) to (14.86). Together with TauCeti.GroupPresentation.relators_def and TauCeti.GroupPresentation.mem_relatorSet_iff this determines the relations defining TauCeti.GroupPresentation.Group, so a consumer never has to unfold the row.

theorem TauCeti.Sporadic.Lyons.matchesMetadata_presentation : presentation.matchesMetadata

The recorded relator count agrees with the transcribed data.

theorem TauCeti.Sporadic.Lyons.map_length_relators_presentation : List.map List.length presentation.relators = have y := have y := have y := [14, 4, 20, 50, 46, 83, 43]; 13 :: 13 :: 12 :: 12 :: 21 :: 6 :: 10 :: y; have y := 22 :: 28 :: 6 :: 4 :: 6 :: 45 :: 29 :: y; 16 :: 13 :: 18 :: 22 :: 13 :: 22 :: y; have y := have y := 26 :: 18 :: 16 :: 18 :: 18 :: 2 :: 9 :: y; 20 :: 12 :: 20 :: 7 :: 15 :: 19 :: y; have y := 40 :: 18 :: 22 :: 22 :: 22 :: 24 :: 24 :: y; 8 :: 5 :: 8 :: 6 :: 12 :: 5 :: y

The lengths of the fifty-three compiled relator words, block by block in source order.

theorem TauCeti.Sporadic.Lyons.totalLength_presentation : presentation.totalLength = 1007

The compiled relator words have 1007 letters in total.

theorem TauCeti.Sporadic.Lyons.map_length_reduce_relators_presentation : List.map (fun (w : List (Fin presentation.generatorCount × Bool)) => (FreeGroup.reduce w).length) presentation.relators = have y := have y := have y := [14, 4, 20, 50, 46, 83, 43]; 13 :: 13 :: 12 :: 12 :: 21 :: 6 :: 10 :: y; have y := 22 :: 26 :: 6 :: 4 :: 6 :: 45 :: 27 :: y; 14 :: 11 :: 18 :: 18 :: 11 :: 18 :: y; have y := have y := 24 :: 18 :: 12 :: 18 :: 18 :: 2 :: 7 :: y; 20 :: 12 :: 20 :: 7 :: 13 :: 19 :: y; have y := 40 :: 16 :: 20 :: 22 :: 22 :: 24 :: 24 :: y; 8 :: 5 :: 8 :: 6 :: 12 :: 5 :: y

The lengths of the fifty-three compiled relator words after free reduction, block by block in source order.

theorem TauCeti.Sporadic.Lyons.reducedTotalLength_presentation : (List.map (fun (w : List (Fin presentation.generatorCount × Bool)) => (FreeGroup.reduce w).length) presentation.relators).sum = 975

The freely reduced relator words have 975 letters in total. The source prints no length for this presentation, so this figure states the transcribed data for a reviewer.