A transcribed presentation of the Monster group

This file records the Y₄₄₃ presentation of the Monster as a TauCeti.GroupPresentation, together with the exact diagram, source conventions, expected counts, and decidable transcription checks.

The twelve involutory generators are the central node a and the nodes on three arms of lengths four, four, and three:

e₁ -- d₁ -- c₁ -- b₁ -- a -- b₂ -- c₂ -- d₂ -- e₂
                        |
                        b₃ -- c₃ -- d₃

The Coxeter relations contribute 12 square relations, 11 order-three edge relations, and 55 order-two nonedge relations. The spider relation

(a b₁ c₁ a b₂ c₂ a b₃ c₃)¹⁰ = 1

gives the 79-relator presentation of M × 2 displayed by Bray. Ivanov defines

f₃₁₂ = (a b₃ c₃ d₃ b₁ c₁ b₂)⁹,

proves that it is central, and in Section 3.9 identifies the quotient Y₄₄₃ / ⟨f₃₁₂⟩ with the Monster. Appending f₃₁₂ = 1 therefore gives the required 80-relator presentation of M.

The source records length 400 for the M × 2 presentation. The Coxeter words and spider word below reproduce that figure; the final central relator has length 63, giving total length 463.

Where each piece of the data comes from

Ivanov defines Y_pqr on p. 413, states the centrality of f₃₁₂ in Lemma 3.2 on p. 419, and identifies the quotient in Section 3.9 on pp. 430--431.

Ivanov's definition on p. 413 takes the Coxeter group on the central node a together with the first p, q, and r of b₁ c₁ d₁ e₁ f₁, b₂ c₂ d₂ e₂ f₂, and b₃ c₃ d₃ e₃ f₃, with the Coxeter relations of the induced subdiagram of Y₅₅₅, and quotients it by the spider relation (a b₁ c₁ a b₂ c₂ a b₃ c₃)¹⁰ = 1 displayed in the introduction on p. 412. At (p,q,r) = (4,4,3) those generators are a, b₁ c₁ d₁ e₁, b₂ c₂ d₂ e₂, and b₃ c₃ d₃, which is the twelve-node alphabet documented for presentation, and the induced subdiagram is the arm structure edges records: eleven edges, four along each of the first two arms and three along the third, so the simply laced coxeterMatrix built from them is the source's Coxeter data. spiderRelator is the displayed spider word letter for letter.

The M × 2 figures Bray records, twelve generators, seventy-nine relators, and length 400, are the ones the Coxeter data yields: twelve involutions of length two, eleven order-three edge relations of length six, and fifty-five commuting non-edge relations of length four give 24 + 66 + 220 = 310, and the spider word of length ninety brings the total to 400. Those counts are length_coxeterRelators and coxeterAndSpider_totalLength below.

For the final relator, Ivanov's p. 419 defines, for {i,j,k} = {1,2,3}, f_ijk = (a bᵢ cᵢ dᵢ b_j c_j b_k)⁹, the generator of the centre of the Sp₆(2) × 2 Coxeter group on the spherical E₇ subdiagram a, bᵢ, cᵢ, dᵢ, b_j, c_j, b_k. Instantiating (i,j,k) = (3,1,2) gives (a b₃ c₃ d₃ b₁ c₁ b₂)⁹, which is centralInvolutionRelator letter for letter, and its seven-letter word repeated nine times is the length 63 checked below. Section 3.9 concludes on p. 431 that Y₄₄₃ / ⟨f₃₁₂⟩ ≅ M, and hence that Y₄₄₃ ≅ 2 × M, so appending this one relator to Bray's seventy-nine is exactly the passage from M × 2 to M.

This file asserts no order, finiteness, or simplicity result for the presented group.

Main definitions

• TauCeti.Sporadic.Monster.coxeterMatrix: the explicitly numbered Y₄₄₃ Coxeter matrix.
• TauCeti.Sporadic.Monster.spiderRelator: the Y₄₄₃ spider relation.
• TauCeti.Sporadic.Monster.centralInvolutionRelator: Ivanov's element f₃₁₂.
• TauCeti.Sporadic.Monster.adjoinedRelators: the two relators the sources adjoin to the Y₄₄₃ Coxeter relations.
• TauCeti.Sporadic.Monster.presentation: the resulting finite presentation of M.

Main results

• TauCeti.Sporadic.Monster.length_relatorList, TauCeti.Sporadic.Monster.presentation_matchesMetadata, TauCeti.Sporadic.Monster.presentation_totalLength and TauCeti.Sporadic.Monster.presentation_relatorsCyclicallyReduced: the transcription checks.
• TauCeti.Sporadic.Monster.mulEquivPresentedGroupCoxeterAppend: the row presents the Coxeter group of the Y₄₄₃ diagram cut down by the spider and central relations.

References

• J. N. Bray, Sporadic (Fischer--Griess) Monster group M = F₁, especially the Y₄₄₃ presentation of M × 2, https://webspace.maths.qmul.ac.uk/j.n.bray/web/Pres/Mnst.html.
• A. A. Ivanov, Y-groups via Transitive Extension, Journal of Algebra 218 (1999), 412--435, especially the definition of Y_pqr on p. 413, Lemma 3.2 on p. 419, and Section 3.9 on pp. 430--431, https://doi.org/10.1006/jabr.1999.7882.

The numbered Y₄₄₃ diagram

def TauCeti.Sporadic.Monster.edges : List (Fin 12 × Fin 12)

The eleven edges of the Y₄₄₃ diagram. The numbering is a = 0, b₁,c₁,d₁,e₁ = 1,2,3,4, b₂,c₂,d₂,e₂ = 5,6,7,8, and b₃,c₃,d₃ = 9,10,11. Each pair is oriented away from the central node.

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

The explicit edge list of the numbered Y₄₄₃ diagram. This is the unfolding lemma for the sealed body.

def TauCeti.Sporadic.Monster.coxeterMatrix : CoxeterMatrix (Fin 12)

The Coxeter matrix of Y₄₄₃, the simply laced matrix of its edge list: diagonal entries are one, an edge has label three, and every other pair has label two.

@[simp]

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

Evaluation of the Y₄₄₃ Coxeter matrix directly from its edge list.

The two non-Coxeter relators

def TauCeti.Sporadic.Monster.spiderRelator : Relator (Fin 12)

The spider relator (a b₁ c₁ a b₂ c₂ a b₃ c₃)¹⁰ of the Y₄₄₃ presentation.

theorem TauCeti.Sporadic.Monster.spiderRelator_def : spiderRelator = (((((((((Relator.gen 0).mul (Relator.gen 1)).mul (Relator.gen 2)).mul (Relator.gen 0)).mul (Relator.gen 5)).mul (Relator.gen 6)).mul (Relator.gen 0)).mul (Relator.gen 9)).mul (Relator.gen 10)).pow 10

The spider relator spelled out in the numbered alphabet. This is the unfolding lemma for the sealed body.

def TauCeti.Sporadic.Monster.centralInvolutionRelator : Relator (Fin 12)

Ivanov's central element f₃₁₂ = (a b₃ c₃ d₃ b₁ c₁ b₂)⁹, imposed as a relator to pass from Y₄₄₃ ≅ M × 2 to the Monster group M.

theorem TauCeti.Sporadic.Monster.centralInvolutionRelator_def : centralInvolutionRelator = (((((((Relator.gen 0).mul (Relator.gen 9)).mul (Relator.gen 10)).mul (Relator.gen 11)).mul (Relator.gen 1)).mul (Relator.gen 2)).mul (Relator.gen 5)).pow 9

Ivanov's element f₃₁₂ spelled out in the numbered alphabet. This is the unfolding lemma for the sealed body.

def TauCeti.Sporadic.Monster.adjoinedRelators : List (Relator (Fin 12))

The two relators the sources adjoin to the Y₄₄₃ Coxeter relations: Bray's spider relator, which cuts the Coxeter group down to M × 2, and Ivanov's central relator, which cuts that down to M.

@[simp]

theorem TauCeti.Sporadic.Monster.adjoinedRelators_def : adjoinedRelators = [spiderRelator, centralInvolutionRelator]

The adjoined-relator list, in source order. The body is sealed, so this equation is what lets a consumer see that the two words adjoined to the Coxeter relations are exactly Bray's spider relator and Ivanov's central relator.

def TauCeti.Sporadic.Monster.relatorList : List (Relator (Fin 12))

The eighty relators of the Monster presentation: the Y₄₄₃ Coxeter relations, followed by the spider and central-involution relators.

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

The relator list decomposes into the Y₄₄₃ Coxeter relations and the two adjoined relators. This is the unfolding lemma for the sealed body.

The presentation row and its audit interface

def TauCeti.Sporadic.Monster.presentation : GroupPresentation

The Y₄₄₃ finite presentation of the Fischer--Griess Monster group M on twelve involutions.

Ivanov proves that Y₄₄₃ is M × 2 and that quotienting by the central element f₃₁₂ gives M. No structural property of the resulting PresentedGroup is asserted here; this definition records only the cited generators and complete relator data.

Generator order (starting at index zero): a, b1, c1, d1, e1, b2, c2, d2, e2, b3, c3, d3.

Source: J. N. Bray, Sporadic (Fischer-Griess) Monster group M = F1; A. A. Ivanov, Y-groups via Transitive Extension, Journal of Algebra 218 (1999), 412-435.

Source locator: Bray's Y443 presentation at https://webspace.maths.qmul.ac.uk/j.n.bray/web/Pres/Mnst.html; Ivanov, definition on p. 413, Lemma 3.2 on p. 419, and Section 3.9 on pp. 430-431; doi:10.1006/jabr.1999.7882

Generator convention: Indices 0 through 11 are a,b1,c1,d1,e1,b2,c2,d2,e2,b3,c3,d3. Every node is an involution, adjacent nodes have product of order dividing three, and nonadjacent nodes commute. Products are read left to right. Ivanov writes f_ijk = (a*b_i*c_i*d_i*b_j*c_j*b_k)^9.

Transcription notes: The Coxeter matrix expands the displayed Y443 diagram to 78 relators. Append Bray's spider relator to present M x 2, then Ivanov's f_312 to quotient its central factor and present M. The first 79 relators have the source's length 400; f_312 has length 63.

@[simp]

theorem TauCeti.Sporadic.Monster.presentation_generatorCount : presentation.generatorCount = 12

The number of generators in the Monster presentation.

@[simp]

theorem TauCeti.Sporadic.Monster.presentation_expectedRelatorCount : presentation.expectedRelatorCount = 80

The expected relator count recorded for the Monster presentation.

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

The relator expressions carried by the Monster presentation are exactly the transcribed relator list, whose decomposition is relatorList_def.

theorem TauCeti.Sporadic.Monster.presentation_relatorLetters : presentation.relatorLetters = List.map (fun (r : Relator (Fin 12)) => List.map (fun (letter : Fin 12 × Bool) => (↑letter.1, letter.2)) r.toWord) relatorList

The compiled relators carried by the Monster presentation, with generator bounds forgotten.

Decidable transcription checks

theorem TauCeti.Sporadic.Monster.length_coxeterRelators : (coxeterRelators coxeterMatrix).length = 78

The Y₄₄₃ Coxeter diagram contributes seventy-eight relators.

theorem TauCeti.Sporadic.Monster.length_relatorList : relatorList.length = 80

The full Monster presentation has eighty relators.

@[simp]

theorem TauCeti.Sporadic.Monster.presentation_transcribed_length : presentation.transcribed.length = 80

The Monster presentation carries eighty relator expressions.

theorem TauCeti.Sporadic.Monster.presentation_matchesMetadata : presentation.matchesMetadata

The relator count recorded for the Monster agrees with the transcribed data.

@[simp]

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

The spider relator has ninety letters.

theorem TauCeti.Sporadic.Monster.coxeterAndSpider_totalLength : (List.map Relator.length (coxeterRelators coxeterMatrix ++ [spiderRelator])).sum = 400

The seventy-nine relators presenting M × 2 have the source's total length 400.

@[simp]

theorem TauCeti.Sporadic.Monster.length_centralInvolutionRelator : centralInvolutionRelator.length = 63

The central-involution relator f₃₁₂ has sixty-three letters.

theorem TauCeti.Sporadic.Monster.presentation_totalLength : presentation.totalLength = 463

The compiled relators of the Monster presentation contain 463 signed letters in total.

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

Every expression in the Monster relator list compiles to a cyclically reduced word.

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

Every compiled Monster relator is cyclically reduced, so the letter counts above agree with the usual presentation-length convention.

The row against the Coxeter group of its diagram

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

The row presents the Coxeter group of the Y₄₄₃ diagram cut down by the spider and central relations, which is the shape in which Bray and Ivanov state the presentation.

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.Monster.mulEquivPresentedGroupCoxeterAppend_apply_of (i : Fin 12) : Monster.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.