Auditable Coxeter relator lists

A Coxeter presentation is normally published as a diagram: a set of involutions, one per node, with a braid relation on each edge and a commuting relation on each non-edge. Mathlib turns a CoxeterMatrix into a group through CoxeterMatrix.relationsSet, the range of CoxeterMatrix.relation, which is a set indexed by ordered pairs rather than an explicit list whose entries and length a reviewer can audit. This file produces that finite relator list, one relator per unordered pair of nodes, the diagonal included, so that the n involution relators sᵢ ^ 2 are among them.

The count is the point. TauCeti.length_coxeterRelators says that a diagram on n nodes has (n + 1).choose 2 = n * (n + 1) / 2 relators — the number of unordered pairs with repetition allowed, not n.choose 2.

The ordered-pair set and the unordered-pair list need not agree: for distinct nodes, (sᵢ sⱼ) ^ mᵢⱼ and (sⱼ sᵢ) ^ mᵢⱼ can be distinct elements of the free group, so the list has to pick one of the two orders — here the one increasing in the node numbering. They are conjugate, so the two sets have the same normal closure, which is what TauCeti.normalClosure_relatorSet_coxeterRelators proves and what makes the presented groups the same.

A published diagram is usually simply laced: every edge carries the label three and every non-edge the label two. TauCeti.coxeterMatrixOfEdges builds the CoxeterMatrix of such a diagram from the list of its edges, so that a transcribed row records the edges the source draws rather than a hand-built matrix.

Main definitions

• TauCeti.coxeterMatrixOfEdges: the Coxeter matrix of a simply laced diagram, from its edges.
• TauCeti.coxeterRelator: the relator expression (sᵢ sⱼ) ^ M i j.
• TauCeti.coxeterRelatorsOfList and TauCeti.coxeterRelators: one Coxeter relator per unordered pair of nodes, the diagonal included.

Main results

• TauCeti.length_coxeterRelators: the relator count of a diagram on n nodes.
• TauCeti.normalClosure_relatorSet_coxeterRelators: the finite list and Mathlib's ordered-pair set have the same normal closure.
• TauCeti.mulEquivCoxeterGroup: the group presented by the Coxeter relator list of M is M.Group.
• TauCeti.mulEquivPresentedGroupCoxeterAppend: the group presented by that list followed by further relators is the group defined by Mathlib's Coxeter relations together with those extra relations.
• TauCeti.of_mul_of_pow_coxeterRelators_append and TauCeti.of_mul_of_self_coxeterRelators_append: in the group presented by that list followed by further relators, (sᵢ sⱼ) ^ M i j = 1, and every generator is an involution.
• TauCeti.GroupPresentation.mulEquivCoxeterGroup and TauCeti.GroupPresentation.mulEquivPresentedGroupCoxeterAppend: the same two conclusions for a transcribed presentation row. Neither asks the row's relators to be the Coxeter relators, or the Coxeter relators followed by the extras, on the nose: each takes as hypothesis only that the relation set of the transcription and the relation set of that list have the same normal closure, which is the datum the quotient depends on. TauCeti.Relator.relatorSet_eq_of_mem_map_toWord_iff can supply such a hypothesis from compiled-word membership.

References

This file supplies reusable Coxeter-presentation machinery needed by milestone S1 of TauCetiRoadmap/CFSGStatement/README.md. No presentation of a named group is asserted here.

TauCeti.coxeterRelatorsOfList is built from Mathlib's List.sym2 in Mathlib.Data.List.Sym, whose List.length_sym2 supplies the relator count, and from Sym2.inf/Sym2.sup in Mathlib.Data.Sym.Sym2.Order, which pick the canonical ordered representative of an unordered pair.

The Coxeter relators of a Coxeter matrix

def TauCeti.coxeterMatrixOfEdges {B : Type u_1} [DecidableEq B] (edges : List (B × B)) : CoxeterMatrix B

The Coxeter matrix of the simply laced diagram with the given edges: a node with itself has entry one, a pair of distinct nodes joined by an edge has entry three, and every other pair of distinct nodes has entry two.

The edge list is read symmetrically, so each edge may be oriented either way, and repeated edges are harmless. The body is exposed so that the checks a transcribed diagram runs on its own matrix reduce.

@[simp]

theorem TauCeti.coxeterMatrixOfEdges_apply {B : Type u_1} [DecidableEq B] (edges : List (B × B)) (i j : B) : (coxeterMatrixOfEdges edges).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 of a simply laced diagram directly from its edge list.

def TauCeti.coxeterRelator {B : Type u_1} (M : CoxeterMatrix B) (i j : B) : Relator B

The Coxeter relator (sᵢ sⱼ) ^ M i j, as an auditable relator expression. On the diagonal M i i = 1, so this is the involution relator sᵢ ^ 2 written as (sᵢ sᵢ) ^ 1.

@[simp]

theorem TauCeti.toWord_coxeterRelator {B : Type u_1} (M : CoxeterMatrix B) (i j : B) : (coxeterRelator M i j).toWord = (List.replicate (M.M i j) [(i, true), (j, true)]).flatten

The compiled signed word of a Coxeter relator.

theorem TauCeti.length_toWord_coxeterRelator {B : Type u_1} (M : CoxeterMatrix B) (i j : B) : List.length (coxeterRelator M i j).toWord = 2 * M.M i j

A Coxeter relator contains twice as many signed letters as its matrix entry.

theorem TauCeti.isCyclicallyReduced_toWord_coxeterRelator {B : Type u_1} (M : CoxeterMatrix B) (i j : B) : FreeGroup.IsCyclicallyReduced (coxeterRelator M i j).toWord

The signed word of a Coxeter relator is cyclically reduced.

@[simp]

theorem TauCeti.toFreeGroup_coxeterRelator {B : Type u_1} (M : CoxeterMatrix B) (i j : B) : (coxeterRelator M i j).toFreeGroup = M.relation i j

Interpreting a Coxeter relator in the free group yields Mathlib's Coxeter relation.

def TauCeti.coxeterRelatorsOfList {B : Type u_1} [LinearOrder B] (M : CoxeterMatrix B) (l : List B) : List (Relator B)

The Coxeter relators drawn from a list of nodes: one relator (sᵢ sⱼ) ^ M i j for each unordered pair of list entries, including pairs that use the same entry, so that the involution relators are among them. Duplicate entries can produce repeated relators. The pair is written in increasing order.

The unordered pairs are Mathlib's List.sym2; Sym2.inf and Sym2.sup name the smaller and the larger node, which is the choice of order the free group forces on the transcription.

theorem TauCeti.coxeterRelatorsOfList_def {B : Type u_1} [LinearOrder B] (M : CoxeterMatrix B) (l : List B) : coxeterRelatorsOfList M l = List.map (fun (z : Sym2 B) => coxeterRelator M z.inf z.sup) l.sym2

The Coxeter relator list is obtained by mapping the canonically ordered representative of each unordered pair of list positions to its Coxeter relator.

This is the unfolding lemma for the sealed body, and like TauCeti.GroupPresentation.relators_def it is deliberately not @[simp]: it lets a concrete finite presentation audit the compiled words without the definition being exposed.

@[simp]

theorem TauCeti.length_coxeterRelatorsOfList {B : Type u_1} [LinearOrder B] (M : CoxeterMatrix B) (l : List B) : (coxeterRelatorsOfList M l).length = (l.length + 1).choose 2

A list of length n yields (n + 1).choose 2 Coxeter relators, the number of unordered pairs of list positions with repetition allowed.

@[simp]

theorem TauCeti.mem_coxeterRelatorsOfList_iff {B : Type u_1} [LinearOrder B] {M : CoxeterMatrix B} {l : List B} {t : Relator B} : t ∈ coxeterRelatorsOfList M l ↔ ∃ i ∈ l, ∃ j ∈ l, t = coxeterRelator M s(i, j).inf s(i, j).sup

Membership in the Coxeter relator list, in terms of two nodes of the source list and their canonical increasing order.

def TauCeti.coxeterRelators {n : ℕ} (M : CoxeterMatrix (Fin n)) : List (Relator (Fin n))

The Coxeter relators of a matrix indexed by Fin n, in the order of the Bourbaki-style node numbering 0, 1, …, n - 1.

theorem TauCeti.coxeterRelators_def {n : ℕ} (M : CoxeterMatrix (Fin n)) : coxeterRelators M = coxeterRelatorsOfList M (List.finRange n)

The numbered Coxeter relator list uses the nodes 0, …, n - 1 in that order. This is the unfolding lemma for the sealed body, and like coxeterRelatorsOfList_def it is not @[simp].

@[simp]

theorem TauCeti.mem_coxeterRelators_iff {n : ℕ} {M : CoxeterMatrix (Fin n)} {t : Relator (Fin n)} : t ∈ coxeterRelators M ↔ ∃ (i : Fin n) (j : Fin n), t = coxeterRelator M s(i, j).inf s(i, j).sup

Membership in the Coxeter relator list of a Fin n-indexed matrix: every pair of nodes contributes, so the only condition is that the relator be the one of a pair, written in the canonical increasing order.

@[simp]

theorem TauCeti.length_coxeterRelators {n : ℕ} (M : CoxeterMatrix (Fin n)) : (coxeterRelators M).length = (n + 1).choose 2

A Coxeter diagram on n nodes has (n + 1).choose 2 relators.

theorem TauCeti.normalClosure_relatorSet_coxeterRelatorsOfList {B : Type u_1} [LinearOrder B] (M : CoxeterMatrix B) {l : List B} (hl : ∀ (i : B), i ∈ l) : Subgroup.normalClosure (Relator.relatorSet (coxeterRelatorsOfList M l)) = Subgroup.normalClosure M.relationsSet

The finite Coxeter relator list presents the same group as Mathlib's relation set. The two sets of relations need not coincide: for distinct nodes, only one of (sᵢ sⱼ) ^ mᵢⱼ and (sⱼ sᵢ) ^ mᵢⱼ is transcribed. They are conjugate and so have the same normal closure.

theorem TauCeti.normalClosure_relatorSet_coxeterRelatorsOfList_append {B : Type u_1} [LinearOrder B] (M : CoxeterMatrix B) {l : List B} (hl : ∀ (i : B), i ∈ l) (extra : List (Relator B)) : Subgroup.normalClosure (Relator.relatorSet (coxeterRelatorsOfList M l ++ extra)) = Subgroup.normalClosure (M.relationsSet ∪ Relator.relatorSet extra)

Appending further relators to the Coxeter relator list imposes Mathlib's Coxeter relations together with the extra relations. A published Y-diagram presentation has this shape, its extra relator being the spider relator.

theorem TauCeti.normalClosure_relatorSet_coxeterRelators {n : ℕ} (M : CoxeterMatrix (Fin n)) : Subgroup.normalClosure (Relator.relatorSet (coxeterRelators M)) = Subgroup.normalClosure M.relationsSet

The Fin n-indexed form of TauCeti.normalClosure_relatorSet_coxeterRelatorsOfList.

theorem TauCeti.normalClosure_relatorSet_coxeterRelators_append {n : ℕ} (M : CoxeterMatrix (Fin n)) (extra : List (Relator (Fin n))) : Subgroup.normalClosure (Relator.relatorSet (coxeterRelators M ++ extra)) = Subgroup.normalClosure (M.relationsSet ∪ Relator.relatorSet extra)

The Fin n-indexed form of TauCeti.normalClosure_relatorSet_coxeterRelatorsOfList_append.

def TauCeti.mulEquivCoxeterGroup {n : ℕ} (M : CoxeterMatrix (Fin n)) : PresentedGroup (Relator.relatorSet (coxeterRelators M)) ≃* M.Group

The group presented by the finite Coxeter relator list is Mathlib's Coxeter group.

@[simp]

theorem TauCeti.mulEquivCoxeterGroup_apply_of {n : ℕ} (M : CoxeterMatrix (Fin n)) (i : Fin n) : (mulEquivCoxeterGroup M) (PresentedGroup.of i) = M.simple i

def TauCeti.mulEquivPresentedGroupCoxeterAppend {n : ℕ} (M : CoxeterMatrix (Fin n)) (extra : List (Relator (Fin n))) : PresentedGroup (Relator.relatorSet (coxeterRelators M ++ extra)) ≃* PresentedGroup (M.relationsSet ∪ Relator.relatorSet extra)

The Coxeter relator list followed by further relators presents Mathlib's Coxeter relations together with those extra relations. Taking extra = [] recovers TauCeti.mulEquivCoxeterGroup.

@[simp]

theorem TauCeti.mulEquivPresentedGroupCoxeterAppend_apply_of {n : ℕ} (M : CoxeterMatrix (Fin n)) (extra : List (Relator (Fin n))) (i : Fin n) : (mulEquivPresentedGroupCoxeterAppend M extra) (PresentedGroup.of i) = PresentedGroup.of i

@[simp]

theorem TauCeti.of_mul_of_pow_coxeterRelators_append {n : ℕ} (M : CoxeterMatrix (Fin n)) (extra : List (Relator (Fin n))) (i j : Fin n) : (PresentedGroup.of i * PresentedGroup.of j) ^ M.M i j = 1

Every Coxeter relation of M holds in a presented group whose relators are the Coxeter relators of M followed by any further relators, in either order of the two generators.

@[simp]

theorem TauCeti.of_mul_of_self_coxeterRelators_append {n : ℕ} (M : CoxeterMatrix (Fin n)) (extra : List (Relator (Fin n))) (i : Fin n) : PresentedGroup.of i * PresentedGroup.of i = 1

Every generator is an involution in a presented group whose relators are the Coxeter relators of M followed by any further relators.

def TauCeti.GroupPresentation.mulEquivCoxeterGroup (P : GroupPresentation) (M : CoxeterMatrix (Fin P.generatorCount)) (h : Subgroup.normalClosure (Relator.relatorSet P.transcribed) = Subgroup.normalClosure (Relator.relatorSet (coxeterRelators M))) : P.Group ≃* M.Group

A transcription whose relations have the same normal closure as the Coxeter relators of M presents M.Group. A presentation row that adds relators to the diagram — every published Y-diagram row does, its spider relator being the addition — is served by TauCeti.GroupPresentation.mulEquivPresentedGroupCoxeterAppend instead.

The hypothesis is stated at the normal-closure level, so it also applies when different relation sets generate the same normal subgroup.

@[simp]

theorem TauCeti.GroupPresentation.mulEquivCoxeterGroup_apply_of (P : GroupPresentation) (M : CoxeterMatrix (Fin P.generatorCount)) (h : Subgroup.normalClosure (Relator.relatorSet P.transcribed) = Subgroup.normalClosure (Relator.relatorSet (coxeterRelators M))) (i : Fin P.generatorCount) : (P.mulEquivCoxeterGroup M h) (PresentedGroup.of i) = M.simple i

def TauCeti.GroupPresentation.mulEquivPresentedGroupCoxeterAppend (P : GroupPresentation) (M : CoxeterMatrix (Fin P.generatorCount)) (extra : List (Relator (Fin P.generatorCount))) (h : Subgroup.normalClosure (Relator.relatorSet P.transcribed) = Subgroup.normalClosure (Relator.relatorSet (coxeterRelators M ++ extra))) : P.Group ≃* PresentedGroup (M.relationsSet ∪ Relator.relatorSet extra)

A transcription whose relations have the same normal closure as the Coxeter relators of M followed by further relators presents the Coxeter relations together with those extra relations. This is the form an audited Y-diagram presentation row uses: the record supplies the generator names, the source, and the count checks, the diagram supplies the Coxeter relators, and the row's own relators — the spider relator, and for the Monster the relator Z as well — are the extras.

@[simp]

theorem TauCeti.GroupPresentation.mulEquivPresentedGroupCoxeterAppend_apply_of (P : GroupPresentation) (M : CoxeterMatrix (Fin P.generatorCount)) (extra : List (Relator (Fin P.generatorCount))) (h : Subgroup.normalClosure (Relator.relatorSet P.transcribed) = Subgroup.normalClosure (Relator.relatorSet (coxeterRelators M ++ extra))) (i : Fin P.generatorCount) : (P.mulEquivPresentedGroupCoxeterAppend M extra h) (PresentedGroup.of i) = PresentedGroup.of i