Artin groups

8 fully proved

Coxeter Matrix

DefinitionAlternating word#✓fully proved

For elements \(a\) and \(b\) of a monoid and \(n \in \mathbb{N}\), the alternating word of length \(n\) starting with \(a\) is the product \(a b a b \cdots\) of \(n\) factors that alternate between \(a\) and \(b\), beginning with \(a\); for \(n = 0\) it is the identity.

def alternatingWord {G : Type*} [Monoid G] (a b : G) : ℕ → G
  | 0 => 1
  | n + 1 => a * alternatingWord b a n

Used by 3

Used byArtin relator · Braid relations in the Artin group · Monoid homomorphisms preserve alternating words

TheoremMonoid homomorphisms preserve alternating words#✓fully proved

Let \(f : G \to H\) be a homomorphism of monoids. For all \(a, b \in G\) and \(n \in \mathbb{N}\), \(f\) maps the alternating word \(a b a \cdots\) of length \(n\) starting with \(a\) to the alternating word \(f(a) f(b) f(a) \cdots\) of length \(n\) starting with \(f(a)\).

theorem map_alternatingWord {G H : Type*} [Monoid G] [Monoid H] (f : G →* H) (a b : G) (n : ℕ) :
    f (alternatingWord a b n) = alternatingWord (f a) (f b) n

Uses 1 · Used by 1

Statement usesAlternating word

Used byBraid relations in the Artin group

DefinitionArtin relator#✓fully proved

Let \(M = (m_{ij})\) be a Coxeter matrix over an index type \(B\), and write \(s_i\) for the free generators of the free group on \(B\). For \(i, j \in B\), let \(u\) and \(v\) be the alternating words \(s_i s_j s_i \cdots\) and \(s_j s_i s_j \cdots\) of length \(m_{ij}\). The Artin relator of the ordered pair \((i, j)\) is the element \(u v^{-1}\) of the free group; setting it equal to \(1\) imposes the braid relation \(u = v\).

def artinRelation (i j : B) : FreeGroup B :=
  alternatingWord (FreeGroup.of i) (FreeGroup.of j) (M i j) *
    (alternatingWord (FreeGroup.of j) (FreeGroup.of i) (M i j))⁻¹

Uses 1 · Used by 2

Statement usesAlternating word

Used byArtin relators of a Coxeter matrix · Braid relations in the Artin group

DefinitionArtin relators of a Coxeter matrix#✓fully proved

Let \(M = (m_{ij})\) be a Coxeter matrix over an index type \(B\), where \(m_{ij} = 0\) encodes \(m_{ij} = \infty\), and write \(s_i\) for the free generators of the free group on \(B\). The set of Artin relators of \(M\) consists of the elements \(u v^{-1}\) of the free group, one for each ordered pair of distinct \(i, j \in B\) with \(m_{ij} \neq 0\), where \(u\) and \(v\) are the alternating words \(s_i s_j s_i \cdots\) and \(s_j s_i s_j \cdots\) of length \(m_{ij}\). Pairs with \(m_{ij} = \infty\) contribute no relator.

def artinRelationsSet : Set (FreeGroup B) :=
  { r | ∃ i j, i ≠ j ∧ M i j ≠ 0 ∧ r = M.artinRelation i j }

Uses 1 · Used by 10

Statement usesArtin relator

Used byArtin group · Braid relations in the Artin group · The generators generate the Artin group · Generators of the Artin group · The braid represented by a braid word · Polynomially short conjugators in braid groups · Kourovka 11.54: pure braids conjugate to their inverses · Pure braid group · Pure braid group · Kourovka 11.55: unique roots in pure braid groups

DefinitionArtin group#✓fully proved

Let \(M = (m_{ij})_{i, j \in B}\) be a Coxeter matrix over an index type \(B\), where \(m_{ij} = 0\) encodes \(m_{ij} = \infty\). The Artin group (Artin–Tits group) of \(M\) is the group presented by generators \(s_i\), one for each \(i \in B\), subject only to the braid relations: for every ordered pair of distinct \(i, j \in B\) with \(m_{ij} \neq 0\), the alternating words \(s_i s_j s_i \cdots\) and \(s_j s_i s_j \cdots\) of length \(m_{ij}\) are equal. Unlike for the Coxeter group of \(M\), no relations \(s_i^2 = 1\) are imposed.

def ArtinGroup := PresentedGroup M.artinRelationsSet

Uses 1 · Used by 9

Statement usesArtin relators of a Coxeter matrix

Used byBraid relations in the Artin group · The generators generate the Artin group · Generators of the Artin group · The braid represented by a braid word · Polynomially short conjugators in braid groups · Kourovka 11.54: pure braids conjugate to their inverses · Pure braid group · Pure braid group · Kourovka 11.55: unique roots in pure braid groups

Artin Group

DefinitionGenerators of the Artin group#✓fully proved

For a Coxeter matrix \(M\) over an index type \(B\) and \(i \in B\), the generator \(s_i\) of the Artin group of \(M\) is the image of the free generator \(i\) under the quotient map from the free group on \(B\) onto the Artin group.

def of (i : B) : M.ArtinGroup := PresentedGroup.of i

Uses 2 · Used by 5

Statement usesArtin group · Artin relators of a Coxeter matrix

Used byBraid relations in the Artin group · The generators generate the Artin group · The braid represented by a braid word · Pure braid group · Pure braid group

TheoremThe generators generate the Artin group#✓fully proved

For a Coxeter matrix \(M\) over an index type \(B\), the subgroup of the Artin group of \(M\) generated by its generators \(s_i\), \(i \in B\), is the whole group.

theorem closure_range_of : Subgroup.closure (Set.range (of M)) = ⊤

Uses 3

Statement usesArtin group · Generators of the Artin group · Artin relators of a Coxeter matrix

TheoremBraid relations in the Artin group#✓fully proved

Let \(M = (m_{ij})\) be a Coxeter matrix over an index type \(B\), where \(m_{ij} = 0\) encodes \(m_{ij} = \infty\), and let \(s_i\) (\(i \in B\)) be the generators of the Artin group of \(M\). For distinct \(i, j \in B\) with \(m_{ij} \neq 0\), the alternating words \(s_i s_j s_i \cdots\) and \(s_j s_i s_j \cdots\) of length \(m_{ij}\) are equal in the Artin group.

theorem braid_relation {i j : B} (hij : i ≠ j) (h : M i j ≠ 0) :
    alternatingWord (of M i) (of M j) (M i j) = alternatingWord (of M j) (of M i) (M i j)

Uses 6

Statement usesArtin group · Generators of the Artin group · Alternating word · Artin relators of a Coxeter matrix

Proof usesArtin relator · Monoid homomorphisms preserve alternating words

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.