The simply laced Artin presentation of a graph

A simple graph determines the Coxeter matrix with diagonal entries 1, adjacent entries 3 and distinct nonadjacent entries 2. A family of group elements satisfying the graph's commuting and length-three braid relations extends to its Artin group by the existing Artin-Tits universal property.

The rank-two entries specify the two types of alternating-word relators.

Conversely, a Coxeter matrix M determines its Coxeter graph CoxeterMatrix.graph, joining two distinct indices exactly when their entry is not 2, that is, when the corresponding simple reflections do not commute. Entries 0, which encode infinite order, are edges too. This forgets the edge labels, and on simply laced matrices it inverts the first construction (SimpleGraph.graph_coxeterMatrix). Simple reflections whose indices are not adjacent in the Coxeter graph commute (CoxeterSystem.commute_simple_of_not_adj).

noncomputable def SimpleGraph.coxeterMatrix {V : Type u} (G : SimpleGraph V) : CoxeterMatrix V

The simply laced Coxeter matrix associated to a graph.

@[simp]

theorem SimpleGraph.coxeterMatrix_apply_of_adj {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : G.coxeterMatrix.M i j = 3

Adjacent vertices give the three-letter Artin braid relation.

@[simp]

theorem SimpleGraph.coxeterMatrix_apply_of_not_adj {V : Type u} (G : SimpleGraph V) {i j : V} (hij : i ≠ j) (h : ¬G.Adj i j) : G.coxeterMatrix.M i j = 2

Distinct nonadjacent vertices give the commuting Artin relation.

noncomputable def SimpleGraph.artinGroupLift {V : Type u} (G : SimpleGraph V) {H : Type v} [Group H] (f : V → H) (commute : ∀ {i j : V}, i ≠ j → ¬G.Adj i j → f i * f j = f j * f i) (braid : ∀ {i j : V}, G.Adj i j → f i * f j * f i = f j * f i * f j) : TauCeti.ArtinGroup G.coxeterMatrix →* H

A graph-braid family of group elements extends to the graph's Artin group.

@[simp]

theorem SimpleGraph.artinGroupLift_gen {V : Type u} (G : SimpleGraph V) {H : Type v} [Group H] (f : V → H) (commute : ∀ {i j : V}, i ≠ j → ¬G.Adj i j → f i * f j = f j * f i) (braid : ∀ {i j : V}, G.Adj i j → f i * f j * f i = f j * f i * f j) (i : V) : (G.artinGroupLift f commute braid) (TauCeti.ArtinGroup.gen G.coxeterMatrix i) = f i

The graph-presentation extension sends each standard generator to its supplied element.

def CoxeterMatrix.graph {B : Type u_1} (M : CoxeterMatrix B) : SimpleGraph B

The Coxeter graph of a Coxeter matrix: two distinct indices are adjacent exactly when their entry is not 2, so that nonadjacent simple reflections commute. The edge labels M i j are forgotten.

@[simp]

theorem CoxeterMatrix.graph_adj {B : Type u_1} (M : CoxeterMatrix B) {i j : B} : M.graph.Adj i j ↔ i ≠ j ∧ M.M i j ≠ 2

@[simp]

theorem SimpleGraph.graph_coxeterMatrix {V : Type u_1} (G : SimpleGraph V) : G.coxeterMatrix.graph = G

The Coxeter graph of the simply laced Coxeter matrix of a graph is the graph itself.

theorem CoxeterSystem.commute_simple_of_not_adj {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} (h : ¬M.graph.Adj i i') : Commute (cs.simple i) (cs.simple i')

Two simple reflections commute when their indices are not adjacent in the Coxeter graph.