Artin-Tits groups

A Coxeter matrix M presents two different groups on the same generating set B. The Coxeter group M.Group imposes the relations (s i * s i') ^ M i i' = 1; equivalently, that each generator is an involution and that the two alternating words of length M i i' in i and i' have the same product. Dropping the involution half and keeping only the second half presents the Artin-Tits group (or generalised braid group) of M: generators σ i, one for each i : B, subject only to

σ i * σ i' * σ i * ⋯ = σ i' * σ i * σ i' * ⋯ (both sides of length M i i').

The braid group on n strands is the Artin-Tits group of the Coxeter matrix of type A, and this file is where its presentation and universal property are proved once and for all; the type-A specialisation is TauCeti.BraidGroup in TauCeti.GroupTheory.SpecificGroups.Braid.

The alternating words are Mathlib's CoxeterSystem.braidWord, so the relator is spelled with exactly the words that Mathlib's CoxeterSystem.wordProd_braidWord_eq proves equal in a Coxeter group. That is what makes TauCeti.ArtinGroup.toCoxeterGroup, the canonical surjection onto the Coxeter group, a one-line consequence of the universal property.

Two degenerate entries of M are worth spelling out, because they are what makes the relator set above correct rather than merely plausible.

• On the diagonal, M i i = 1, and both alternating words are the one-letter word [i], so the relator is trivial. In particular no relation σ i * σ i = 1 is imposed: an Artin-Tits group is torsion-free-looking on its generators, and indeed TauCeti.ArtinGroup.orderOf_gen shows every generator has infinite order.
• When M i i' = 0, meaning that s i * s i' has infinite order in the Coxeter group, both alternating words are empty and again no relation is imposed, which is the intended reading.

Main definitions

• TauCeti.artinRelation M i i': the relator ⟨i i'⟩ * ⟨i' i⟩⁻¹ in FreeGroup B, where ⟨i i'⟩ denotes the alternating word of length M i i' in i and i' that ends with i'.
• TauCeti.artinRelationsSet M: the set of all such relators.
• TauCeti.ArtinGroup M: the Artin-Tits group of M.
• TauCeti.ArtinGroup.gen M i: its standard generator at the index i.
• TauCeti.ArtinGroup.lift: the universal property.
• TauCeti.ArtinGroup.closure_range_gen and TauCeti.ArtinGroup.gen_induction_on: generation by the standard generators and its induction principle.
• TauCeti.ArtinGroup.toCoxeterGroup: the canonical map onto a Coxeter group with matrix M.
• TauCeti.ArtinGroup.exponentSum: the total exponent of a word in the standard generators.

Main results

• TauCeti.prod_map_alternatingWord_two and TauCeti.prod_map_alternatingWord_three: the rank-two alternating-word evaluation rules used below.
• TauCeti.ArtinGroup.prod_map_gen_braidWord: the defining braid relation holds.
• TauCeti.ArtinGroup.gen_mul_gen_comm and TauCeti.ArtinGroup.gen_braid: the rank-two form of that relation, at an entry M i i' = 2 and at an entry M i i' = 3.
• TauCeti.ArtinGroup.toCoxeterGroup_surjective: the map to the Coxeter group is surjective.
• TauCeti.ArtinGroup.hom_ext: homomorphisms are determined by the standard generators.
• TauCeti.ArtinGroup.gen_ne_one and TauCeti.ArtinGroup.orderOf_gen: a standard generator is nontrivial, indeed of infinite order. These are the non-degeneracy statements which distinguish the Artin-Tits presentation from the Coxeter presentation on the same generators.

References

• E. Artin, Theorie der Zöpfe, Abh. Math. Sem. Univ. Hamburg 4 (1925), 47-72.
• E. Brieskorn, K. Saito, Artin-Gruppen und Coxeter-Gruppen, Invent. Math. 17 (1972), 245-271.
• J. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82 (1974).

This file is Layer 4 ("knot theory, done properly") of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md), which asks for "braid closures (over PresentedMonoid braid groups with the Artin relations)" as one of the presentations of a knot.

def TauCeti.artinRelation {B : Type u_1} (M : CoxeterMatrix B) (i i' : B) : FreeGroup B

The Artin-Tits relator of a Coxeter matrix M at a pair of indices: the quotient of the two alternating words of length M i i' in i and i'. It is trivial when M i i' ∈ {0, 1}, in particular on the diagonal.

Equations

• TauCeti.artinRelation M i i' = (List.map FreeGroup.of (CoxeterSystem.braidWord M i i')).prod * (List.map FreeGroup.of (CoxeterSystem.braidWord M i' i)).prod⁻¹

theorem TauCeti.artinRelation_def {B : Type u_1} (M : CoxeterMatrix B) (i i' : B) : artinRelation M i i' = (List.map FreeGroup.of (CoxeterSystem.braidWord M i i')).prod * (List.map FreeGroup.of (CoxeterSystem.braidWord M i' i)).prod⁻¹

The defining equation of an Artin-Tits relator.

def TauCeti.artinRelationsSet {B : Type u_1} (M : CoxeterMatrix B) : Set (FreeGroup B)

The set of all Artin-Tits relators of a Coxeter matrix.

Equations

• TauCeti.artinRelationsSet M = Set.range (Function.uncurry (TauCeti.artinRelation M))

theorem TauCeti.artinRelation_mem_artinRelationsSet {B : Type u_1} (M : CoxeterMatrix B) (i i' : B) : artinRelation M i i' ∈ artinRelationsSet M

@[simp]

theorem TauCeti.mem_artinRelationsSet {B : Type u_1} (M : CoxeterMatrix B) {r : FreeGroup B} : r ∈ artinRelationsSet M ↔ ∃ (i : B) (i' : B), artinRelation M i i' = r

@[reducible, inline]

abbrev TauCeti.ArtinGroup {B : Type u_1} (M : CoxeterMatrix B) : Type u_1

The Artin-Tits group of a Coxeter matrix M; that is, the group $$\langle \{σ_i\}_{i ∈ B} \mid \underbrace{σ_i σ_{i'} ⋯}_{M_{i,i'}} = \underbrace{σ_{i'} σ_i ⋯}_{M_{i,i'}} \rangle .$$ Unlike the Coxeter group of M, the generators are not required to be involutions.

Equations

• TauCeti.ArtinGroup M = PresentedGroup (TauCeti.artinRelationsSet M)

def TauCeti.ArtinGroup.gen {B : Type u_1} (M : CoxeterMatrix B) (i : B) : ArtinGroup M

The standard generator σ i of the Artin-Tits group of M.

Equations

• TauCeti.ArtinGroup.gen M i = PresentedGroup.of i

@[simp]

theorem TauCeti.ArtinGroup.of_eq_gen {B : Type u_1} (M : CoxeterMatrix B) (i : B) : PresentedGroup.of i = gen M i

Mathlib's presented-group generator is the standard Artin-Tits generator.

@[simp]

theorem TauCeti.ArtinGroup.closure_range_gen {B : Type u_1} (M : CoxeterMatrix B) : Subgroup.closure (Set.range (gen M)) = ⊤

The standard generators generate the Artin-Tits group.

theorem TauCeti.ArtinGroup.gen_induction_on {B : Type u_1} (M : CoxeterMatrix B) {p : ArtinGroup M → Prop} (g : ArtinGroup M) (gen : ∀ (i : B), p (gen M i)) (one : p 1) (mul : ∀ (g g' : ArtinGroup M), p g → p g' → p (g * g')) (inv : ∀ (g : ArtinGroup M), p g → p g⁻¹) : p g

To prove a predicate for every Artin-Tits group element, it suffices to prove it for the identity and standard generators and show that it is preserved by multiplication and inverse.

theorem TauCeti.ArtinGroup.prod_map_gen_braidWord {B : Type u_1} (M : CoxeterMatrix B) (i i' : B) : (List.map (gen M) (CoxeterSystem.braidWord M i i')).prod = (List.map (gen M) (CoxeterSystem.braidWord M i' i)).prod

The defining relation of the Artin-Tits group: the two alternating words of length M i i' in the standard generators σ i and σ i' have the same product.

theorem TauCeti.ArtinGroup.gen_mul_gen_comm {B : Type u_1} (M : CoxeterMatrix B) {i i' : B} (h : M.M i i' = 2) : gen M i * gen M i' = gen M i' * gen M i

Two standard generators commute when the corresponding entry of M is 2.

theorem TauCeti.ArtinGroup.gen_braid {B : Type u_1} (M : CoxeterMatrix B) {i i' : B} (h : M.M i i' = 3) : gen M i * gen M i' * gen M i = gen M i' * gen M i * gen M i'

Two standard generators satisfy the length-three braid relation when the corresponding entry of M is 3.

def TauCeti.ArtinGroup.lift {B : Type u_1} {G : Type u_2} [Group G] (M : CoxeterMatrix B) (f : B → G) (hf : ∀ (i i' : B), (List.map f (CoxeterSystem.braidWord M i i')).prod = (List.map f (CoxeterSystem.braidWord M i' i)).prod) : ArtinGroup M →* G

The universal property of the Artin-Tits presentation: a family f of elements of a group satisfying the braid relations of M extends to a homomorphism out of ArtinGroup M.

Equations

• TauCeti.ArtinGroup.lift M f hf = PresentedGroup.toGroup ⋯

@[simp]

theorem TauCeti.ArtinGroup.lift_gen {B : Type u_1} {G : Type u_2} [Group G] (M : CoxeterMatrix B) (f : B → G) (hf : ∀ (i i' : B), (List.map f (CoxeterSystem.braidWord M i i')).prod = (List.map f (CoxeterSystem.braidWord M i' i)).prod) (i : B) : (lift M f hf) (gen M i) = f i

theorem TauCeti.ArtinGroup.hom_ext {B : Type u_1} {G : Type u_2} [Group G] (M : CoxeterMatrix B) {f g : ArtinGroup M →* G} (h : ∀ (i : B), f (gen M i) = g (gen M i)) : f = g

Two homomorphisms from an Artin–Tits group are equal if they agree on every standard generator.

theorem TauCeti.ArtinGroup.hom_ext_iff {B : Type u_1} {G : Type u_2} [Group G] {M : CoxeterMatrix B} {f g : ArtinGroup M →* G} : f = g ↔ ∀ (i : B), f (gen M i) = g (gen M i)

def TauCeti.ArtinGroup.exponentSum {B : Type u_1} (M : CoxeterMatrix B) : ArtinGroup M →* Multiplicative ℤ

The exponent-sum homomorphism, sending every standard generator to 1 : ℤ. It is well defined because the two sides of every Artin-Tits relation are words of the same length; this is what fails for the Coxeter presentation, where σ i * σ i = 1 has sides of lengths 2 and 0.

Equations

• TauCeti.ArtinGroup.exponentSum M = TauCeti.ArtinGroup.lift M (fun (x : B) => Multiplicative.ofAdd 1) ⋯

@[simp]

theorem TauCeti.ArtinGroup.exponentSum_gen {B : Type u_1} (M : CoxeterMatrix B) (i : B) : (exponentSum M) (gen M i) = Multiplicative.ofAdd 1

@[simp]

theorem TauCeti.ArtinGroup.gen_zpow_eq_one_iff {B : Type u_1} (M : CoxeterMatrix B) (i : B) (k : ℤ) : gen M i ^ k = 1 ↔ k = 0

A power of a standard generator is trivial only for the exponent 0; in particular the Artin-Tits presentation does not collapse.

@[simp]

theorem TauCeti.ArtinGroup.gen_pow_eq_one_iff {B : Type u_1} (M : CoxeterMatrix B) (i : B) (k : ℕ) : gen M i ^ k = 1 ↔ k = 0

@[simp]

theorem TauCeti.ArtinGroup.orderOf_gen {B : Type u_1} (M : CoxeterMatrix B) (i : B) : orderOf (gen M i) = 0

Every standard Artin-Tits generator has infinite order.

@[simp]

theorem TauCeti.ArtinGroup.gen_ne_one {B : Type u_1} (M : CoxeterMatrix B) (i : B) : gen M i ≠ 1

Every standard Artin-Tits generator is nontrivial.

def TauCeti.ArtinGroup.toCoxeterGroup {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : ArtinGroup M →* W

The canonical homomorphism from the Artin-Tits group of M onto a Coxeter group with matrix M, sending each standard generator to the corresponding simple reflection. It exists because the Coxeter relations imply the Artin-Tits relations, which is Mathlib's CoxeterSystem.wordProd_braidWord_eq.

Equations

• TauCeti.ArtinGroup.toCoxeterGroup cs = TauCeti.ArtinGroup.lift M cs.simple ⋯

@[simp]

theorem TauCeti.ArtinGroup.toCoxeterGroup_gen {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : (toCoxeterGroup cs) (gen M i) = cs.simple i

theorem TauCeti.ArtinGroup.toCoxeterGroup_surjective {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Function.Surjective ⇑(toCoxeterGroup cs)

The canonical map from the Artin–Tits group onto the associated Coxeter group is surjective.