A transcribed presentation of the third Fischer group

This file carries the Fi24Prime row of the sporadic presentation data. The cited source presents the 3-transposition group Fi₂₄'·2 and proves that its commutator subgroup is the simple group Fi₂₄'. It also gives the index-two subgroup generators

ab, ac, ad, ae, af, ag, ah, ai, aj, ak.

The presentation recorded here is the Reidemeister--Schreier presentation of that commutator subgroup. An eleventh Schreier generator al is retained instead of using the source relation l = (abcdefh)⁹ to eliminate it; retaining it keeps every derived relator a direct rewrite of one displayed source relator.

The source presentation has twelve involutory generators, indexed here as a,b,c,d,e,f,g,h,i,j,k,l. Its Coxeter graph is

l -- k -- a -- b -- c -- d -- e -- f -- g -- j
                         |
                         h -- i

and it has two further relations

l = (a b c d e f h)^9,
(d c b a k l d e f g j d h i)^17 = 1.

Sending every source generator to the nontrivial element of C₂ is the quotient onto Fi₂₄'·2 / Fi₂₄'. With transversal {1,a}, the Schreier generator attached to x is ax. Because all source generators are involutions, a source letter in an even position, counting positions from zero, rewrites as (ax)⁻¹ and one in an odd position as ax; conjugating a relator by a exchanges the two signs. Each off-diagonal Coxeter relator and each further relator therefore contributes those two rewrites. The square relators are precisely the relations used to eliminate the other half of the Schreier generators: after that elimination each rewrites to u⁻¹u or uu⁻¹, so none remains.

Thus the 66 off-diagonal Coxeter relators and two further relators yield 2 · (66 + 2) = 136 relators on eleven generators. TauCeti.Sporadic.fi24PrimePresentation_matchesMetadata checks this count, while TauCeti.Sporadic.even_length_of_mem_fi24AutomorphismRelators checks that every source relator does lie in the index-two subgroup before the rewrite is applied.

The rewrite drops exactly the source letters equal to a, which is TauCeti.Sporadic.length_fi24SchreierRewrite, so the letter count of the row is read off the source relators rather than off the rewritten ones: TauCeti.Sporadic.fi24PrimePresentation_totalLength records the 1076 letters they contribute. Neither source publishes a presentation length to check that figure against, and the row claims no cyclic reduction of its compiled words, so the count states the transcribed data for comparison with the source rather than checking it against a published number.

Nothing here asserts that the presented group is nontrivial, finite, simple, of any particular order, or isomorphic to another realization. Kim and Michler prove that the commutator subgroup of the displayed source presentation is Fi₂₄'; Reidemeister--Schreier rewriting transfers that presentation to the subgroup. That transfer is a theorem here: TauCeti.Sporadic.fi24PrimeGroupMulEquivCommutator identifies the group presented by the row with the commutator subgroup of the group TauCeti.Sporadic.Fi24AutomorphismGroup presented by the eighty source relators, through the general index-two rewriting theorem TauCeti.IsSchreierIndexTwoSource.mulEquivCommutator. The independent read-through below then checks the source relators, and only them, against the cited source.

Independent source-to-Lean read-through

An independent read-through used Kim--Michler, Lemma 6.2. The paper presents twelve involutions a,b,c,d,e,f,g,h,i,j,k,l. Its eleven exponent-three pairs are

lk, ka, ab, bc, cd, de, ef, fg, gj, dh, hi,

and its fifty-five exponent-two pairs are

la,lb,lc,ld,le,lf,lg,lj,lh,li,
kb,kc,kd,ke,kf,kg,kj,kh,ki,
ac,ad,ae,af,ag,aj,ah,ai,
bd,be,bf,bg,bj,bh,bi,
ce,cf,cg,cj,ch,ci, df,dg,dj,
eg,ej,eh,ei, fj,fh,fi, gh,gi, jh,ji,di.

These are exactly the eleven undirected pairs in fi24AutomorphismEdges and their complement; fi24AutomorphismCoxeterMatrix assigns the edges entry three, every other off-diagonal pair entry two, and the diagonal entry one. The two remaining source relations have exactly the letters and exponents recorded by fi24SourceEquationWord_def and fi24SourceLongWord_def:

l = (a b c d e f h)^9,
(d c b a k l d e f g j d h i)^17 = 1.

Thus the source's twelve squares, eleven exponent-three pairs, fifty-five exponent-two pairs, and two displayed relations account for all 80 entries of fi24AutomorphismRelators, with none dropped or duplicated.

Lemma 6.2(c) identifies the commutator subgroup and gives the generators ab through ak. The connected exponent-three graph makes all twelve source generators equal in the abelianization, TauCeti.Sporadic.abelianizationOf_fi24AutomorphismGroup_of, while sending each of them to the nontrivial element of C₂ kills all the source relators. Hence that parity map has the commutator subgroup as its index-two kernel, TauCeti.Sporadic.commutator_fi24AutomorphismGroup_eq_ker_fi24ParityHom. The rewrite was then checked definition by definition: fi24SchreierFactors toggles the transversal representative after every source letter, omits a, and records (ax)⁻¹ and ax in alternating positions. Starting in the two possible representatives gives the rewrites of r and a r a. The twelve square relations perform the standard elimination of the redundant Schreier generators; each of the remaining 66 + 2 source relators contributes both rewrites. This gives exactly the 136 relators generated by fi24PrimeRelators, retaining al so that the source equation for l remains visible. fi24PrimePresentation_relatorLetters exposes the resulting compiled words for kernel-checked inspection.

Main definitions

• TauCeti.Sporadic.fi24AutomorphismCoxeterMatrix: the source's numbered Coxeter diagram.
• TauCeti.Sporadic.fi24AutomorphismRelators: all eighty source relators for Fi₂₄'·2.
• TauCeti.Sporadic.fi24SchreierRewrite: the Reidemeister--Schreier rewrite of a source relator.
• TauCeti.Sporadic.fi24PrimePresentation: the Reidemeister--Schreier presentation of Fi₂₄'.
• TauCeti.Sporadic.Fi24AutomorphismGroup and TauCeti.Sporadic.fi24ParityHom: the group presented by the eighty source relators, and its parity homomorphism onto C₂.
• TauCeti.Sporadic.fi24PrimeGroupMulEquivCommutator: the group presented by the row is the commutator subgroup of TauCeti.Sporadic.Fi24AutomorphismGroup.

Main results

• TauCeti.Sporadic.isSchreierIndexTwoSource_fi24: the source presentation and the source relators selected for rewriting satisfy the hypotheses of index-two Reidemeister--Schreier rewriting.
• TauCeti.Sporadic.relatorSet_fi24PrimeRelators: the row's relations are the Reidemeister--Schreier relators of the source words.
• TauCeti.Sporadic.commutator_fi24AutomorphismGroup_eq_ker_fi24ParityHom: the commutator subgroup of the source presented group is the kernel of its parity homomorphism.

Every definition here except the abbreviation TauCeti.Sporadic.Fi24AutomorphismGroup has its body sealed, and each is pinned by a public characteristic equation named after it: the _def theorems below, the evaluation lemmas TauCeti.Sporadic.fi24AutomorphismCoxeterMatrix_apply and TauCeti.Sporadic.fi24SchreierFactors_nil/_cons, and the field equations of the presentation row ending in TauCeti.Sporadic.fi24PrimePresentation_relatorLetters, jointly determine every transcribed relation without unfolding a single body.

References

• H. K. Kim and G. O. Michler, Construction of Fischer's sporadic group Fi₂₄' inside GL₈₆₇₁(13), preprint (2009), https://arxiv.org/abs/0906.1064v1. Lemma 6.2 reproduces the full presentation, proves that its commutator subgroup is simple, and gives the ten subgroup generators above; Theorem 6.3 identifies that subgroup with Fi₂₄'.
• J. I. Hall and L. H. Soicher, Presentations of some 3-transposition groups, Communications in Algebra 23 (1995), 2517--2559, https://doi.org/10.1080/00927879508825358, the original source of the presentation reproduced by Kim and Michler.
• M. Hall, Jr., The Theory of Groups, Macmillan, 1959, Chapter 7, for the Reidemeister--Schreier rewriting process used to pass to the index-two subgroup.

The source presentation of Fi₂₄'·2

def TauCeti.Sporadic.fi24AutomorphismEdges : List (Fin 12 × Fin 12)

The eleven edges in the source's Coxeter diagram, using the generator order a,b,c,d,e,f,g,h,i,j,k,l.

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

The edges of the source diagram, spelled out. The body is sealed, so this equation is what publishes the transcribed diagram: with TauCeti.Sporadic.fi24AutomorphismCoxeterMatrix_apply it determines every entry of the source Coxeter matrix.

This is deliberately not @[simp]: the simp-normal fact about this list is TauCeti.Sporadic.length_fi24AutomorphismEdges, while this equation is available for an explicit audit of the transcribed edges.

def TauCeti.Sporadic.fi24AutomorphismCoxeterMatrix : CoxeterMatrix (Fin 12)

The Coxeter matrix of Hall--Soicher's twelve-generator presentation of Fi₂₄'·2. Adjacent nodes have entry three and all other distinct nodes have entry two.

@[simp]

theorem TauCeti.Sporadic.fi24AutomorphismCoxeterMatrix_apply (i j : Fin 12) : fi24AutomorphismCoxeterMatrix.M i j = if i = j then 1 else if (i, j) ∈ fi24AutomorphismEdges ∨ (j, i) ∈ fi24AutomorphismEdges then 3 else 2

Evaluation of the source Coxeter matrix directly from its edge list.

@[simp]

theorem TauCeti.Sporadic.length_fi24AutomorphismEdges : fi24AutomorphismEdges.length = 11

The source diagram has eleven edges.

def TauCeti.Sporadic.fi24SourcePairRelators : List (Relator (Fin 12))

The off-diagonal Coxeter relators in the order supplied by List.sym2.

theorem TauCeti.Sporadic.fi24SourcePairRelators_def : fi24SourcePairRelators = List.map (fun (z : Sym2 (Fin 12)) => coxeterRelator fi24AutomorphismCoxeterMatrix z.inf z.sup) (List.filter (fun (z : Sym2 (Fin 12)) => decide (z.inf ≠ z.sup)) (List.finRange 12).sym2)

The off-diagonal Coxeter relators, spelled out over Mathlib's unordered-pair list. The body is sealed, so this equation is what publishes which pairs are taken and in which order.

Like TauCeti.GroupPresentation.relators_def this is deliberately not @[simp]: the simp normal form of the list is the count TauCeti.Sporadic.length_fi24SourcePairRelators, not the enumeration of all sixty-six pairs.

def TauCeti.Sporadic.fi24SourceEquationWord : Relator (Fin 12)

The seven-letter right-hand side of the source equation for l, before taking its ninth power.

theorem TauCeti.Sporadic.fi24SourceEquationWord_def : fi24SourceEquationWord = ((((((Relator.gen 0).mul (Relator.gen 1)).mul (Relator.gen 2)).mul (Relator.gen 3)).mul (Relator.gen 4)).mul (Relator.gen 5)).mul (Relator.gen 7)

The letters of the source word a b c d e f h. The body is sealed, so this equation is what lets an audit read the transcribed word off against the source.

This equation and the ones from here to TauCeti.Sporadic.fi24AutomorphismRelators_def are deliberately not @[simp]. Unfolding a source word underneath its ninth or seventeenth power makes simp rebuild the compiled word letter by letter and exceed the recursion limit; the simp-normal facts about these definitions are the length lemmas below.

def TauCeti.Sporadic.fi24SourceLongWord : Relator (Fin 12)

The fourteen-letter word in the source's final relation.

theorem TauCeti.Sporadic.fi24SourceLongWord_def : fi24SourceLongWord = (((((((((((((Relator.gen 3).mul (Relator.gen 2)).mul (Relator.gen 1)).mul (Relator.gen 0)).mul (Relator.gen 10)).mul (Relator.gen 11)).mul (Relator.gen 3)).mul (Relator.gen 4)).mul (Relator.gen 5)).mul (Relator.gen 6)).mul (Relator.gen 9)).mul (Relator.gen 3)).mul (Relator.gen 7)).mul (Relator.gen 8)

The letters of the source word d c b a k l d e f g j d h i. The body is sealed, so this equation is what lets an audit read the transcribed word off against the source.

def TauCeti.Sporadic.fi24SourceEquationRelator : Relator (Fin 12)

The source relation l = (a b c d e f h)^9, stored as a relator.

theorem TauCeti.Sporadic.fi24SourceEquationRelator_def : fi24SourceEquationRelator = (Relator.gen 11).div (fi24SourceEquationWord.pow 9)

The source equation for l, compiled as the relator l · ((a b c d e f h)^9)⁻¹.

def TauCeti.Sporadic.fi24SourceLongRelator : Relator (Fin 12)

The source relation (d c b a k l d e f g j d h i)^17 = 1.

theorem TauCeti.Sporadic.fi24SourceLongRelator_def : fi24SourceLongRelator = fi24SourceLongWord.pow 17

The source's final relation, compiled as the seventeenth power of its fourteen-letter word.

def TauCeti.Sporadic.fi24AutomorphismAdditionalRelators : List (Relator (Fin 12))

The two non-Coxeter relators in the source presentation: the displayed equation for l, followed by the long relator.

theorem TauCeti.Sporadic.fi24AutomorphismAdditionalRelators_def : fi24AutomorphismAdditionalRelators = [fi24SourceEquationRelator, fi24SourceLongRelator]

The two additional source relators, in the order in which the source displays them.

def TauCeti.Sporadic.fi24AutomorphismRelators : List (Relator (Fin 12))

The complete eighty-relator Hall--Soicher presentation of Fi₂₄'·2: all Coxeter relations of the diagram, followed by the two additional source relations.

theorem TauCeti.Sporadic.fi24AutomorphismRelators_def : fi24AutomorphismRelators = coxeterRelators fi24AutomorphismCoxeterMatrix ++ fi24AutomorphismAdditionalRelators

The source relator list, spelled out as the diagram's Coxeter relators followed by the two displayed relations.

@[simp]

theorem TauCeti.Sporadic.length_fi24AutomorphismRelators : fi24AutomorphismRelators.length = 80

The source presentation has eighty relators: 78 Coxeter relators and two additional relators.

@[simp]

theorem TauCeti.Sporadic.length_fi24SourceEquationWord : fi24SourceEquationWord.length = 7

The source word a b c d e f h has seven letters.

@[simp]

theorem TauCeti.Sporadic.length_fi24SourceLongWord : fi24SourceLongWord.length = 14

The source word d c b a k l d e f g j d h i has fourteen letters.

@[simp]

theorem TauCeti.Sporadic.length_fi24SourceEquationRelator : fi24SourceEquationRelator.length = 64

The compiled source equation for l has 1 + 9 · 7 = 64 letters.

@[simp]

theorem TauCeti.Sporadic.length_fi24SourceLongRelator : fi24SourceLongRelator.length = 238

The compiled final source relation has 17 · 14 = 238 letters.

theorem TauCeti.Sporadic.even_length_of_mem_fi24AutomorphismRelators (r : Relator (Fin 12)) : r ∈ fi24AutomorphismRelators → Even (List.length r.toWord)

Every source relator has even length, so sending all twelve involutory generators to the nontrivial element of C₂ kills every relation. This is the parity check needed before applying the index-two Reidemeister--Schreier rewrite.

Reidemeister--Schreier rewriting

def TauCeti.Sporadic.fi24SchreierFactors : Bool → PresentationWord (Fin 12) → List (Relator (Fin 11))

Rewrite source letters into the Schreier generators ab through al.

The Boolean records whether the current transversal representative is a. Source signs are ignored because the source square relations make every generator an involution; inversion has already reversed the order of letters in Relator.toWord. Reading any letter switches the transversal representative, including the distinguished letter a, which contributes no factor.

@[simp]

theorem TauCeti.Sporadic.fi24SchreierFactors_nil (positive : Bool) : fi24SchreierFactors positive [] = []

The empty source word contributes no Schreier factor.

@[simp]

theorem TauCeti.Sporadic.fi24SchreierFactors_cons (positive : Bool) (i : Fin 12) (sign : Bool) (w : PresentationWord (Fin 12)) : fi24SchreierFactors positive ((i, sign) :: w) = if h : i = 0 then fi24SchreierFactors (!positive) w else (if positive = true then Relator.gen (i.pred h) else (Relator.gen (i.pred h)).inv) :: fi24SchreierFactors (!positive) w

One step of TauCeti.Sporadic.fi24SchreierFactors: the letter a contributes nothing and any other letter contributes the Schreier generator it names, inverted exactly when the current transversal representative is 1. With TauCeti.Sporadic.fi24SchreierFactors_nil this determines the rewrite of every source word.

def TauCeti.Sporadic.fi24SchreierRewrite (positive : Bool) (r : Relator (Fin 12)) : Relator (Fin 11)

Rewrite a source relator using the transversal representative selected by positive. Starting with false rewrites r; starting with true rewrites a r a.

theorem TauCeti.Sporadic.fi24SchreierRewrite_def (positive : Bool) (r : Relator (Fin 12)) : fi24SchreierRewrite positive r = List.foldr Relator.mul ((Relator.gen 0).pow 0) (fi24SchreierFactors positive r.toWord)

The rewrite of a source relator is the product of its Schreier factors, the empty product being the trivial relator. The body is sealed, so this equation is what publishes the rewrite.

@[simp]

theorem TauCeti.Sporadic.length_fi24SchreierRewrite (positive : Bool) (r : Relator (Fin 12)) : (fi24SchreierRewrite positive r).length = List.countP (fun (letter : Fin 12 × Bool) => decide (letter.1 ≠ 0)) r.toWord

The Reidemeister--Schreier rewrite keeps exactly the source letters other than a. The distinguished letter a is the transversal element, so it contributes no Schreier generator, while every other source letter contributes one, inverted or not according to the transversal representative reached so far. In particular the two rewrites r and a r a of one source relator have the same length, the right-hand side not mentioning positive.

def TauCeti.Sporadic.fi24PrimeRelators : List (Relator (Fin 11))

The 136 relators of the index-two subgroup. The square relations are omitted after their standard Tietze elimination of the redundant Schreier generators; the 66 off-diagonal Coxeter relations and the two additional relations each contribute a rewrite of r and of a r a.

theorem TauCeti.Sporadic.fi24PrimeRelators_def : fi24PrimeRelators = List.flatMap (fun (r : Relator (Fin 12)) => [fi24SchreierRewrite false r, fi24SchreierRewrite true r]) (fi24SourcePairRelators ++ fi24AutomorphismAdditionalRelators)

The rewritten relators, spelled out as the two rewrites of each source relator. The body is sealed, so this equation together with TauCeti.Sporadic.fi24SchreierRewrite_def, TauCeti.Sporadic.fi24SchreierFactors_cons, TauCeti.Sporadic.fi24SourcePairRelators_def and TauCeti.Sporadic.fi24AutomorphismAdditionalRelators_def determines every relation of the presentation.

@[simp]

theorem TauCeti.Sporadic.length_fi24SourcePairRelators : fi24SourcePairRelators.length = 66

The off-diagonal source relations consist of the sixty-six unordered pairs of distinct generators.

@[simp]

theorem TauCeti.Sporadic.length_fi24PrimeRelators : fi24PrimeRelators.length = 136

The Reidemeister--Schreier presentation has 136 relators.

def TauCeti.Sporadic.fi24PrimePresentation : GroupPresentation

Hall--Soicher's finite presentation of the third Fischer 3-transposition group, rewritten by Reidemeister--Schreier for its commutator subgroup Fi₂₄'.

Kim and Michler reproduce the source presentation, prove that its commutator subgroup is the simple group Fi₂₄', and give the first ten Schreier generators. The retained eleventh generator al makes the rewrite directly traceable to the displayed source relations. The recorded counts are those of this transcription, not figures quoted from the source: 11 generators, the ten displayed ones and al, and 136 relators, two rewrites of each of the 66 + 2 source relators. No structural property of the resulting PresentedGroup is asserted here.

Generator order (starting at index zero): ab, ac, ad, ae, af, ag, ah, ai, aj, ak, al.

Source: H. K. Kim and G. O. Michler, Construction of Fischer's sporadic group Fi24' inside GL_8671(13), arXiv:0906.1064v1 (2009); presentation originally due to J. I. Hall and L. H. Soicher.

Source locator: Kim--Michler, Lemma 6.2 and Theorem 6.3, arXiv:0906.1064v1; Hall--Soicher, Presentations of some 3-transposition groups, Communications in Algebra 23 (1995), 2517-2559, doi:10.1080/00927879508825358

Generator convention: Source generators are a,b,c,d,e,f,g,h,i,j,k,l. Target indices 0 through 10 denote ab,ac,ad,ae,af,ag,ah,ai,aj,ak,al. All source generators are involutions. With transversal {1,a}, an even-position source letter x rewrites as (a*x)^-1 and an odd-position source letter rewrites as a*x; the source letter a contributes no target letter.

Transcription notes: Expand the source diagram into 78 Coxeter relators and append its two displayed relations. The twelve square relations eliminate the redundant half of the Schreier generators and then rewrite trivially. Each of the 66 off-diagonal Coxeter relators and each of the two displayed relations contributes its rewrite and the rewrite of its conjugate by a, for 2*(66+2)=136 relators. Retain al rather than eliminating it with the first displayed relation, so every target relator remains a direct rewrite of a source relator. The independent source-to-Lean read-through checked all 80 source relators and the Reidemeister--Schreier rewrite producing the 136 target relators.

@[simp]

theorem TauCeti.Sporadic.fi24PrimePresentation_generatorCount : fi24PrimePresentation.generatorCount = 11

The presentation of Fi₂₄' has eleven generators. Their names and order are documented in fi24PrimePresentation.

@[simp]

theorem TauCeti.Sporadic.fi24PrimePresentation_expectedRelatorCount : fi24PrimePresentation.expectedRelatorCount = 136

The relator count obtained by rewriting each of the 66 off-diagonal Coxeter relators and each of the two displayed relations twice.

theorem TauCeti.Sporadic.fi24PrimePresentation_relatorLetters : fi24PrimePresentation.relatorLetters = List.map (fun (r : Relator (Fin 11)) => List.map (fun (letter : Fin 11 × Bool) => (↑letter.1, letter.2)) r.toWord) fi24PrimeRelators

The compiled relator words of the Fi₂₄' row are the compiled rewritten relators. A letter (i, true) is the generator with index i and (i, false) is its inverse, so index 0 reads ab and index 10 reads al.

The row's body is sealed, so this is the equation that characterizes what it transcribes. The 136 words are not spelled out: TauCeti.Sporadic.fi24PrimeRelators_def and the _def equations it cites determine every one of them from the eleven-edge source diagram, which is the form in which the source displays the presentation. Letters rather than relator expressions are compared because the index type of a relator depends on the generator count while the letters do not.

theorem TauCeti.Sporadic.fi24PrimePresentation_matchesMetadata : fi24PrimePresentation.matchesMetadata

The relator count recorded for Fi₂₄' agrees with the rewritten data.

Letter counts

Every count below is read off the source relators through TauCeti.Sporadic.length_fi24SchreierRewrite rather than off the rewritten words, which is what keeps the arithmetic tied to the eleven-edge diagram a reviewer checks against the source.

@[simp]

theorem TauCeti.Sporadic.fi24PrimePresentation_totalLength : fi24PrimePresentation.totalLength = 1076

The compiled relator words of the Fi₂₄' row contain 1076 letters in total.

By TauCeti.Sporadic.length_fi24SchreierRewrite the two rewrites of a source relator have the same length, namely its number of letters other than a, so the total is twice the 538 letters the 68 source relators selected for rewriting contribute: 262 from the off-diagonal Coxeter relators, 55 from the source equation for l, and 221 from the final source relation.

Neither Kim--Michler nor Hall--Soicher publishes a presentation length, so this figure is a property of the transcribed data and not a check against a recorded number. It is a count of compiled letters and not of reduced ones: no cyclic reduction of the words is claimed, the Reidemeister--Schreier rewrite being what stands between a source relator and the word whose letters are counted.

The row presents the commutator subgroup of the source presentation

The source relators present Fi₂₄'·2, and the row is the Reidemeister--Schreier rewrite of the source words other than the squares for the transversal {1, a}. The general theorem TauCeti.IsSchreierIndexTwoSource.mulEquivCommutator identifies the rewritten presented group with the commutator subgroup of the source presented group, once the source presentation is checked to be one by involutions with even-length relators, its Schreier generators are matched with the row's generator indices, and the source generators are shown to agree in the abelianization.

@[reducible, inline]

abbrev TauCeti.Sporadic.Fi24AutomorphismGroup : Type

The group presented by the eighty source relators, Hall--Soicher's presentation of Fi₂₄'·2. Nothing here asserts that it is finite or identifies it with any other realization.

theorem TauCeti.Sporadic.fi24AutomorphismGroup_of_mul_of_pow (i j : Fin 12) : (PresentedGroup.of i * PresentedGroup.of j) ^ fi24AutomorphismCoxeterMatrix.M i j = 1

Every Coxeter relation of the source diagram holds in the source presented group, in either order of the two generators.

theorem TauCeti.Sporadic.fi24AutomorphismGroup_of_mul_of_self (i : Fin 12) : PresentedGroup.of i * PresentedGroup.of i = 1

Every source generator is an involution in the source presented group.

theorem TauCeti.Sporadic.abelianizationOf_fi24AutomorphismGroup_of (i : Fin 12) : Abelianization.of (PresentedGroup.of i) = Abelianization.of (PresentedGroup.of 0)

All source generators agree in the abelianization of the source presented group. Two generators joined by an edge of the diagram are involutions whose product has order dividing three, so they coincide in any abelian quotient, and the diagram is connected.

def TauCeti.Sporadic.fi24SourceWords : Set (PresentationWord (Fin 12))

The source words the row rewrites: the compiled words of the sixty-six off-diagonal Coxeter relators and of the two displayed relations.

theorem TauCeti.Sporadic.mem_fi24SourceWords {w : PresentationWord (Fin 12)} : w ∈ fi24SourceWords ↔ ∃ r ∈ fi24SourcePairRelators ++ fi24AutomorphismAdditionalRelators, r.toWord = w

theorem TauCeti.Sporadic.isSchreierIndexTwoSource_fi24 : IsSchreierIndexTwoSource (Relator.relatorSet fi24AutomorphismRelators) fi24SourceWords

The source presentation is an index-two Reidemeister--Schreier source: its generators are involutions, the source words selected for rewriting have even length and are relations, and every source relator is one of those words or the square of a generator.

def TauCeti.Sporadic.fi24ParityHom : Fi24AutomorphismGroup →* Multiplicative (ZMod 2)

The parity homomorphism of the source presented group, sending each of the twelve source generators to the nontrivial element of C₂.

@[simp]

theorem TauCeti.Sporadic.fi24ParityHom_of (i : Fin 12) : fi24ParityHom (PresentedGroup.of i) = Multiplicative.ofAdd 1

theorem TauCeti.Sporadic.commutator_fi24AutomorphismGroup_eq_ker_fi24ParityHom : commutator Fi24AutomorphismGroup = fi24ParityHom.ker

The commutator subgroup of the source presented group is the kernel of its parity homomorphism, the source generators all agreeing in the abelianization.

def TauCeti.Sporadic.fi24SchreierEquiv : { x : Fin 12 // x ≠ 0 } ≃ Fin 11

The indexing of the Schreier generators by the row: the source generator x ≠ a at index i names the Schreier generator a x at index i - 1.

theorem TauCeti.Sporadic.fi24SchreierEquiv_apply (i : Fin 12) (h : i ≠ 0) : fi24SchreierEquiv ⟨i, h⟩ = i.pred h

theorem TauCeti.Sporadic.toWord_fi24SchreierRewrite (positive : Bool) (r : Relator (Fin 12)) : (fi24SchreierRewrite positive r).toWord = schreierWord 0 fi24SchreierEquiv positive r.toWord

The row's rewrite of a source relator compiles to the general Reidemeister--Schreier rewrite of its compiled word.

theorem TauCeti.Sporadic.relatorSet_fi24PrimeRelators : Relator.relatorSet fi24PrimeRelators = schreierRelators 0 fi24SchreierEquiv fi24SourceWords

The row's relations are the Reidemeister--Schreier relators of the source words.

noncomputable def TauCeti.Sporadic.fi24PrimeGroupMulEquivCommutator : fi24PrimePresentation.Group ≃* ↥(commutator Fi24AutomorphismGroup)

The group presented by the Fi₂₄' row is the commutator subgroup of the group presented by the source relators. The Schreier generator ax at row index i goes to the product a x of the source generators, TauCeti.Sporadic.coe_fi24PrimeGroupMulEquivCommutator_of.

This identifies the transcribed row with the subgroup that Kim and Michler prove to be Fi₂₄'. It asserts nothing about the order or the structure of either side.

theorem TauCeti.Sporadic.coe_fi24PrimeGroupMulEquivCommutator_of (i : Fin 11) : ↑(fi24PrimeGroupMulEquivCommutator (PresentedGroup.of (Fin.cast coe_fi24PrimeGroupMulEquivCommutator_of._proof_2 i))) = PresentedGroup.of 0 * PresentedGroup.of i.succ

The identification sends the row generator at index i, the Schreier generator a x for the source generator x at index i + 1, to the product a x in the source presented group.