A transcribed presentation of the Baby Monster

This file records the Y₄₃₃ presentation of the Baby Monster as a TauCeti.GroupPresentation, together with the diagram it expands, the exact source, the generator convention, the transcription notes, and decidable checks on the transcribed data.

The eleven involutory generators are the nodes of a Y-shaped Coxeter diagram: a chain of eight nodes with a further arm of three nodes attached to its fifth node,

t₁ -- t₂ -- t₃ -- t₄ -- t₅ -- t₆ -- t₇ -- t₈
                        |
                        t₉ -- t₁₀ -- t₁₁

so that the branch node t₅ carries three arms, of lengths four, three and three; this is what the name Y₄₃₃ records. The Coxeter relations contribute 11 square relators and one relator (tᵢ tⱼ) ^ m for each of the 55 unordered pairs of distinct nodes, with m = 3 on the ten edges and m = 2 off them. Adjoining the spider relation

(t₅ t₄ t₃ t₅ t₆ t₇ t₅ t₉ t₁₀) ^ 10 = 1

presents 2 × 2·B, and adjoining the two further relations

(t₅ t₄ t₃ t₆ t₇ t₈ t₉) ^ 9 = 1,      (t₅ t₄ t₃ t₆ t₉ t₁₀ t₁₁) ^ 9 = 1

presents the Baby Monster itself. The 69 relators are therefore 66 + 1 + 2.

The source presents the abstract group rather than recognizing generators inside a group constructed elsewhere. The presentation was conjectured in the ATLAS of Finite Groups and proved by Ivanov, subject to the Monster having no proper double cover; that hypothesis is Griess's determination of the Schur multiplier of the Monster. The row below records that chain of attributions rather than reproving any part of it.

Nothing here asserts that the presented group is nontrivial, finite or simple, that it has any particular order, or that it is isomorphic to any other construction of the Baby Monster.

Source-to-Lean read-through

The transcription was compared with Breuer--Magaard--Wilson, Section 3.1, in arXiv:1902.07758v2. The source numbers eleven involutions t₁ through t₁₁ and lists the exponent-three pairs

(1,2), (2,3), (3,4), (4,5), (5,6), (6,7), (7,8), (5,9), (9,10), (10,11).

After the source's one-based numbering is shifted to Fin 11, these are exactly the ten undirected pairs in edges_eq. The source assigns exponent two to every other pair i < j, which is exactly the complement selected by coxeterMatrix_apply; the diagonal entries supply the eleven square relations. Thus the Coxeter list contains the source's 11 + 10 + 45 = 66 relations, with none dropped or duplicated.

The source next displays the spider word

(t₅ t₄ t₃ t₅ t₆ t₇ t₅ t₉ t₁₀)^10

and the two words

(t₅ t₄ t₃ t₆ t₇ t₈ t₉)^9,  (t₅ t₄ t₃ t₆ t₉ t₁₀ t₁₁)^9.

Their letters, order, and exponents agree exactly with spiderRelator_def, extraRelatorOne_def, and extraRelatorTwo_def. The source states that the Coxeter relations plus the spider relation present 2 × 2·B, and that adjoining the last two relations presents B. adjoinedRelators_def lists precisely those three words in that order, and relatorList_def appends them to the Coxeter relators, giving the checked total 66 + 3 = 69.

Main definitions

• TauCeti.Sporadic.BabyMonster.arms and TauCeti.Sporadic.BabyMonster.edges: the three arms of the Y₄₃₃ diagram and the edges they contribute.
• TauCeti.Sporadic.BabyMonster.coxeterMatrix: the Coxeter matrix of the numbered diagram.
• TauCeti.Sporadic.BabyMonster.spiderRelator: the spider relation of the source.
• TauCeti.Sporadic.BabyMonster.extraRelatorOne and TauCeti.Sporadic.BabyMonster.extraRelatorTwo: the two further relations the source adjoins to pass from 2 × 2·B to B.
• TauCeti.Sporadic.BabyMonster.presentation: the transcribed row.

Main results

• TauCeti.Sporadic.BabyMonster.map_length_neighbors: the degree sequence of the transcribed diagram, a check consistent with the published Y-shape; edges_eq and map_length_arms pin the shape itself.
• TauCeti.Sporadic.BabyMonster.length_relatorList and TauCeti.Sporadic.BabyMonster.matchesMetadata_presentation: the transcription count checks.
• TauCeti.Sporadic.BabyMonster.presentation_totalLength: the compiled relator words contain 478 letters, of which 262 come from the Coxeter relators, by TauCeti.Sporadic.BabyMonster.sum_map_length_coxeterRelators, and the rest from the three adjoined relators. The source records no presentation length, so this is transcribed data stated for comparison with the source rather than a check against a published figure.
• TauCeti.Sporadic.BabyMonster.presentation_relatorsCyclicallyReduced: every compiled word is cyclically reduced, which is what makes that letter count comparable with a published presentation length at all.
• TauCeti.Sporadic.BabyMonster.mulEquivPresentedGroupCoxeterAppend: the row presents the Coxeter group of the diagram cut down by the three adjoined relations, which is the shape of the source's statement.

References

• T. Breuer, K. Magaard, and R. A. Wilson, Verification of the ordinary character table of the Baby Monster, Journal of Algebra 561 (2020), 111--130, https://doi.org/10.1016/j.jalgebra.2019.06.047, also https://arxiv.org/abs/1902.07758. Section 3.1 states the Y₄₃₃ presentation used here.
• A. A. Ivanov, Presenting the Baby Monster, Journal of Algebra 163 (1994), 88--108, https://doi.org/10.1006/jabr.1994.1005, which proves that the diagram with the spider relation presents 2 × 2·B. This is the work Breuer--Magaard--Wilson cite for the proof.
• R. L. Griess, Jr., The Schur multipliers of the known finite simple groups, III, in Proceedings of the Rutgers Group Theory Year, 1983--1984, Cambridge University Press, 1985, 69--80, which is the work Breuer--Magaard--Wilson cite for the Schur multiplier of the Monster.
• J. H. Conway, R. T. Curtis, S. P. Norton, R. A. Parker, and R. A. Wilson, Atlas of Finite Groups, Clarendon Press, Oxford, 1985, where the presentation was conjectured.

The numbered Y₄₃₃ diagram

The source numbers its involutions t₁ to t₁₁; the relator index Fin 11 follows that numbering with the customary offset, so tᵢ is index i - 1.

def TauCeti.Sporadic.BabyMonster.branchNode : Fin 11

The branch node of the diagram, the source's t₅.

theorem TauCeti.Sporadic.BabyMonster.branchNode_def : branchNode = 4

The branch node is index four, corresponding to the source's t₅.

def TauCeti.Sporadic.BabyMonster.arms : List (List (Fin 11))

The three arms of the diagram, each listed outwards from the branch node: t₄ t₃ t₂ t₁, then t₆ t₇ t₈, then t₉ t₁₀ t₁₁.

theorem TauCeti.Sporadic.BabyMonster.arms_def : arms = [[3, 2, 1, 0], [5, 6, 7], [8, 9, 10]]

The three arms, spelled out in the numbered alphabet.

theorem TauCeti.Sporadic.BabyMonster.map_length_arms : List.map List.length arms = [4, 3, 3]

The three arms have lengths four, three and three, which is what the name Y₄₃₃ records.

theorem TauCeti.Sporadic.BabyMonster.nodup_branchNode_cons_flatten_arms : (branchNode :: arms.flatten).Nodup

The branch node and the arms use each of the eleven nodes at most once.

theorem TauCeti.Sporadic.BabyMonster.mem_branchNode_cons_flatten_arms (i : Fin 11) : i ∈ branchNode :: arms.flatten

The branch node and the arms use every node, so with TauCeti.Sporadic.BabyMonster.nodup_branchNode_cons_flatten_arms each generator of the presentation occupies exactly one position of the diagram.

def TauCeti.Sporadic.BabyMonster.edges : List (Fin 11 × Fin 11)

The edges of the diagram: each arm contributes the edge joining it to the branch node and an edge between each pair of nodes consecutive along it. Pairs are oriented outwards; the Coxeter matrix below reads them symmetrically.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.edges_eq : edges = [(4, 3), (3, 2), (2, 1), (1, 0), (4, 5), (5, 6), (6, 7), (4, 8), (8, 9), (9, 10)]

The ten edges of the numbered diagram, written out.

Read with the offset tᵢ ↦ i - 1, these are the source's ten adjacent pairs (1,2), (2,3), (3,4), (4,5), (5,6), (6,7), (7,8), (5,9), (9,10), (10,11). The first arm's four edges appear in reverse order and reverse orientation because that arm is listed outwards from the branch node.

theorem TauCeti.Sporadic.BabyMonster.length_edges : edges.length = 10

The diagram has ten edges.

def TauCeti.Sporadic.BabyMonster.coxeterMatrix : CoxeterMatrix (Fin 11)

The Coxeter matrix of the numbered Y₄₃₃ diagram, the simply laced matrix of its edge list: a node with itself has entry one, an edge has entry three, and every other pair of nodes has entry two.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.coxeterMatrix_apply (i j : Fin 11) : coxeterMatrix.M i j = if i = j then 1 else if (i, j) ∈ edges ∨ (j, i) ∈ edges then 3 else 2

Evaluation of the Coxeter matrix directly from the edge list.

def TauCeti.Sporadic.BabyMonster.neighbors (i : Fin 11) : List (Fin 11)

The nodes joined to a given node by an edge, read off the Coxeter matrix rather than off the edge list, so that a comparison with the diagram sees the matrix that the relators are built from.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.mem_neighbors_iff (i j : Fin 11) : j ∈ neighbors i ↔ coxeterMatrix.M i j = 3

Membership in neighbors i is characterized by the corresponding Coxeter-matrix entry.

theorem TauCeti.Sporadic.BabyMonster.neighbors_branchNode : neighbors branchNode = [3, 5, 8]

The branch node is joined to the first node of each of the three arms.

theorem TauCeti.Sporadic.BabyMonster.map_length_neighbors : List.map (fun (i : Fin 11) => (neighbors i).length) (List.finRange 11) = [1, 2, 2, 2, 3, 2, 2, 1, 2, 2, 1]

The degree sequence of the transcribed diagram. Node t₅, that is index 4, has three neighbors; the three arm ends t₁, t₈ and t₁₁, that is indices 0, 7 and 10, have one each; and the remaining seven nodes have two each. Thus the matrix that the relators are built from has a degree sequence consistent with the Y-shape. The shape itself is pinned by edges_eq together with map_length_arms and nodup_branchNode_cons_flatten_arms, from which the edges are built.

The three adjoined relations

def TauCeti.Sporadic.BabyMonster.spiderRelator : Relator (Fin 11)

The spider relator (t₅ t₄ t₃ t₅ t₆ t₇ t₅ t₉ t₁₀) ^ 10 of the source. Adjoining it to the Coxeter relations of the diagram gives a presentation of 2 × 2·B.

theorem TauCeti.Sporadic.BabyMonster.spiderRelator_def : spiderRelator = (((((((((Relator.gen 4).mul (Relator.gen 3)).mul (Relator.gen 2)).mul (Relator.gen 4)).mul (Relator.gen 5)).mul (Relator.gen 6)).mul (Relator.gen 4)).mul (Relator.gen 8)).mul (Relator.gen 9)).pow 10

The spider relator spelled out in the numbered alphabet.

def TauCeti.Sporadic.BabyMonster.extraRelatorOne : Relator (Fin 11)

The first of the two relators (t₅ t₄ t₃ t₆ t₇ t₈ t₉) ^ 9 that the source adjoins to the spider relation to pass from 2 × 2·B to B.

theorem TauCeti.Sporadic.BabyMonster.extraRelatorOne_def : extraRelatorOne = (((((((Relator.gen 4).mul (Relator.gen 3)).mul (Relator.gen 2)).mul (Relator.gen 5)).mul (Relator.gen 6)).mul (Relator.gen 7)).mul (Relator.gen 8)).pow 9

The first adjoined relator spelled out in the numbered alphabet.

def TauCeti.Sporadic.BabyMonster.extraRelatorTwo : Relator (Fin 11)

The second of the two relators (t₅ t₄ t₃ t₆ t₉ t₁₀ t₁₁) ^ 9 that the source adjoins to the spider relation to pass from 2 × 2·B to B.

theorem TauCeti.Sporadic.BabyMonster.extraRelatorTwo_def : extraRelatorTwo = (((((((Relator.gen 4).mul (Relator.gen 3)).mul (Relator.gen 2)).mul (Relator.gen 5)).mul (Relator.gen 8)).mul (Relator.gen 9)).mul (Relator.gen 10)).pow 9

The second adjoined relator spelled out in the numbered alphabet.

def TauCeti.Sporadic.BabyMonster.adjoinedRelators : List (Relator (Fin 11))

The three relators the source adjoins to the Coxeter relations of the diagram, in the order it introduces them.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.adjoinedRelators_def : adjoinedRelators = [spiderRelator, extraRelatorOne, extraRelatorTwo]

The adjoined-relator list, in source order.

def TauCeti.Sporadic.BabyMonster.relatorList : List (Relator (Fin 11))

The sixty-nine relators of the presentation: the Coxeter relations of the Y₄₃₃ diagram followed by the spider relator and the two further relators.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.relatorList_def : relatorList = coxeterRelators coxeterMatrix ++ adjoinedRelators

The relator list is the Coxeter list followed by the three adjoined relators.

The transcribed row and its checks

def TauCeti.Sporadic.BabyMonster.presentation : GroupPresentation

The Y₄₃₃ finite presentation of the Baby Monster B on eleven involutions.

Ivanov proves that the diagram with the spider relation presents 2 × 2·B; the source adjoins two further relations to present B. No structural property of the resulting PresentedGroup is asserted here: this definition records only the cited generators and the complete relator data.

Generator order (starting at index zero): t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11.

Source: T. Breuer, K. Magaard, and R. A. Wilson, Verification of the ordinary character table of the Baby Monster, Journal of Algebra 561 (2020), 111-130; A. A. Ivanov, Presenting the Baby Monster, Journal of Algebra 163 (1994), 88-108.

Source locator: Breuer-Magaard-Wilson, Section 3.1, doi:10.1016/j.jalgebra.2019.06.047, also arXiv:1902.07758v2; Ivanov, doi:10.1006/jabr.1994.1005. The presentation was conjectured in the Atlas of Finite Groups (Conway, Curtis, Norton, Parker, Wilson, 1985) and proved by Ivanov, subject to the Monster having no proper double cover, which is Griess's computation of the Schur multiplier of the Monster (The Schur multipliers of the known finite simple groups, III, Proceedings of the Rutgers Group Theory Year 1983-1984, Cambridge University Press, 1985, 69-80).

Generator convention: Indices 0 through 10 are the source's involutions t1 through t11, so t_i is index i-1. The Coxeter diagram is the chain t1-t2-t3-t4-t5-t6-t7-t8 together with the arm t5-t9-t10-t11, so t5 is the branch node and the three arms have lengths 4, 3 and 3. Products are read left to right.

Transcription notes: The Coxeter matrix expands the diagram into 66 relators: eleven squares t_i^2, one relator (t_i t_j)^3 for each of the ten edges, and one relator (t_i t_j)^2 for each of the remaining 45 unordered pairs of distinct nodes. Appended to them are the source's spider relation, which presents 2 x 2.B, and then its two further relations, which present B. The source displays its relations by family rather than as a numbered list and records no total length, so the expected relator count is the sum 11 + 55 + 1 + 2 over those families.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.presentation_generatorCount : presentation.generatorCount = 11

The number of generators in the Baby Monster presentation.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.presentation_expectedRelatorCount : presentation.expectedRelatorCount = 69

The expected number of relators in the Baby Monster presentation.

theorem TauCeti.Sporadic.BabyMonster.presentation_transcribed : presentation.transcribed = cast presentation_transcribed._proof_1 relatorList

The relators of the row are TauCeti.Sporadic.BabyMonster.relatorList: the Coxeter relations of the diagram followed by the three adjoined relators (relatorList_def).

The cast transports the list along presentation_generatorCount. This is not @[simp] because simp cannot see through that cast; rewrite with it instead.

theorem TauCeti.Sporadic.BabyMonster.length_relatorList : relatorList.length = 69

The transcribed presentation has sixty-nine relators, the (11 + 1).choose 2 = 66 Coxeter relators of a diagram on eleven nodes together with the three adjoined relators.

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

The recorded relator count agrees with the transcribed data.

Letter counts

@[simp]

theorem TauCeti.Sporadic.BabyMonster.length_spiderRelator : spiderRelator.length = 90

The spider relator compiles to 10 · 9 = 90 letters.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.length_extraRelatorOne : extraRelatorOne.length = 63

The first adjoined relator compiles to 9 · 7 = 63 letters.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.length_extraRelatorTwo : extraRelatorTwo.length = 63

The second adjoined relator compiles to 9 · 7 = 63 letters.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.sum_map_length_coxeterRelators : (List.map (fun (r : Relator (Fin 11)) => r.length) (coxeterRelators coxeterMatrix)).sum = 262

The Coxeter relators of the Y₄₃₃ diagram contain 262 letters. A relator (tᵢ tⱼ) ^ m contributes 2m, so the eleven involution relators contribute 2 each, the ten edges 6 each, and the forty-five remaining pairs of distinct nodes 4 each: 22 + 60 + 180. Reading the count off the Coxeter matrix rather than off the expanded relators is what ties it to the transcribed edge list.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.presentation_totalLength : presentation.totalLength = 478

The compiled relator words of the row contain 478 letters in total, the 262 letters of the Coxeter relators together with the 90 + 63 + 63 letters of the three adjoined relators.

The source displays its relations by family and records no presentation length, so this figure states the transcribed data for a reviewer to compare with the source rather than checking it against a published number.

theorem TauCeti.Sporadic.BabyMonster.isCyclicallyReduced_toWord_of_mem_relatorList (r : Relator (Fin 11)) (hr : r ∈ relatorList) : FreeGroup.IsCyclicallyReduced r.toWord

Every expression in the Y₄₃₃ relator list compiles to a cyclically reduced word. The Coxeter relators are cyclically reduced for any Coxeter matrix, and each adjoined relator is a power whose base is a product of generators with no inverse, so no letter of it can cancel against its neighbour or against the last letter of the word.

theorem TauCeti.Sporadic.BabyMonster.presentation_relatorsCyclicallyReduced : presentation.relatorsCyclicallyReduced

Every compiled relator word of the row is cyclically reduced, which is what makes the letter count of TauCeti.Sporadic.BabyMonster.presentation_totalLength comparable with the usual presentation-length convention, under which a relator is measured after free and cyclic reduction.

def TauCeti.Sporadic.BabyMonster.mulEquivPresentedGroupCoxeterAppend : presentation.Group ≃* PresentedGroup (coxeterMatrix.relationsSet ∪ Relator.relatorSet adjoinedRelators)

The row presents the Coxeter group of the Y₄₃₃ diagram cut down by the three adjoined relations, which is the shape in which the source states the presentation: the Coxeter relations of the diagram, the spider relation, and the two further relations.

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.

@[simp]

theorem TauCeti.Sporadic.BabyMonster.mulEquivPresentedGroupCoxeterAppend_apply_of (i : Fin 11) : BabyMonster.mulEquivPresentedGroupCoxeterAppend (PresentedGroup.of (Fin.cast mulEquivPresentedGroupCoxeterAppend_apply_of._proof_2 i)) = PresentedGroup.of i

The Coxeter equivalence sends each canonical generator to the corresponding canonical generator.