The Artin braid group

The braid group B n on n strands is the group generated by the elementary braids σ 0, …, σ (n - 2), where σ i crosses strand i over strand i + 1, subject to

• σ i * σ j = σ j * σ i when the two crossings are disjoint, that is |i - j| ≥ 2, and
• σ i * σ j * σ i = σ j * σ i * σ j when they share a strand, that is |i - j| = 1.

These are exactly the Artin-Tits relations of the Coxeter matrix of type A, so TauCeti.BraidGroup n is defined as TauCeti.ArtinGroup (CoxeterMatrix.A (n - 1)) and inherits the presentation and exponent-sum homomorphism proved there. This file restates the universal property in the classical index form and adds the type-A bookkeeping: the two relations in their classical index form, and the permutation homomorphism B n →* Equiv.Perm (Fin n) recording where a braid sends its strands, which is what makes the presentation visibly non-degenerate.

Indexing follows the classical convention: BraidGroup n is the group on n strands, so its generators are indexed by Fin (n - 1) and it acts on the n strands Fin n. In particular BraidGroup 0 and BraidGroup 1 are trivial.

Two theorems keep the presentation honest. TauCeti.BraidGroup.permHom_surjective says that every permutation of the strands is realised by a braid, and TauCeti.BraidGroup.not_commute_sigma says that two generators sharing a strand do not commute, so BraidGroup n is nonabelian as soon as n ≥ 3. Together with TauCeti.BraidGroup.sigma_ne_one and TauCeti.BraidGroup.orderOf_sigma (each generator is nontrivial and has infinite order), they rule out the collapse that a mis-stated relator set would cause.

Main definitions

• TauCeti.BraidGroup n: the braid group on n strands.
• TauCeti.BraidGroup.sigma i: the elementary braid crossing strands i and i + 1.
• TauCeti.BraidGroup.lift: the universal property in terms of the classical braid relations, with computation rule lift_sigma and sigma-phrased extensionality theorem hom_ext.
• TauCeti.BraidGroup.strand and TauCeti.BraidGroup.strandSucc: the two strands that sigma i crosses, as elements of Fin n.
• TauCeti.BraidGroup.transposition i: the transposition of those two strands.
• TauCeti.BraidGroup.strandIncl: the homomorphism adding one uncrossed strand, BraidGroup (n + 1) →* BraidGroup (n + 2).
• TauCeti.BraidGroup.permHom n: the underlying-permutation homomorphism.
• TauCeti.BraidGroup.pureSubgroup n: the pure braid group, its kernel.

Main results

• TauCeti.BraidGroup.sigma_mul_sigma_comm and TauCeti.BraidGroup.sigma_braid: the two defining relations, in their classical index form.
• TauCeti.BraidGroup.closure_range_sigma and TauCeti.BraidGroup.sigma_induction_on: generation by the elementary braids and its induction principle.
• TauCeti.BraidGroup.permHom_surjective: every permutation of the strands underlies a braid.
• TauCeti.BraidGroup.permHom_strandIncl_castSucc and TauCeti.BraidGroup.permHom_strandIncl_last: adding an uncrossed strand permutes the old strands as before and fixes the new one.
• TauCeti.BraidGroup.permHom_sigma_last: the last elementary braid transposes the last two strands.
• TauCeti.BraidGroup.not_commute_sigma and TauCeti.BraidGroup.exists_not_commute: generators sharing a strand do not commute, so BraidGroup n is nonabelian for n ≥ 3.
• TauCeti.BraidGroup.sigma_zpow_mem_pureSubgroup_iff and TauCeti.BraidGroup.sigma_pow_mem_pureSubgroup_iff: precisely the even integer and natural powers of a generator are pure braids; in particular, the generator is not pure and its square is pure.

References

• E. Artin, Theorie der Zöpfe, Abh. Math. Sem. Univ. Hamburg 4 (1925), 47-72.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 1 (printed p. 10).
• J. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82 (1974), Chapter 1.

This is Layer 4 ("knot theory, done properly") of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md), which lists "braid closures (over PresentedMonoid braid groups with the Artin relations)" among the presentations of a knot, with the closure of a braid word and Markov's theorem as the edge joining that presentation to the diagram hub.

@[reducible, inline]

abbrev TauCeti.BraidGroup (n : ℕ) : Type

The Artin braid group on n strands: the Artin-Tits group of the Coxeter matrix of type A (n - 1). This is motivated by the classical identification of the corresponding Coxeter group with the symmetric group on the n strands, which is not formalized here; permHom below is constructed directly from adjacent transpositions.

Equations

• TauCeti.BraidGroup n = TauCeti.ArtinGroup (CoxeterMatrix.A (n - 1))

def TauCeti.BraidGroup.sigma {n : ℕ} (i : Fin (n - 1)) : BraidGroup n

The elementary braid σ i, crossing strand i over strand i + 1.

Equations

• TauCeti.BraidGroup.sigma i = TauCeti.ArtinGroup.gen (CoxeterMatrix.A (n - 1)) i

theorem TauCeti.BraidGroup.sigma_eq_gen {n : ℕ} (i : Fin (n - 1)) : sigma i = ArtinGroup.gen (CoxeterMatrix.A (n - 1)) i

An elementary braid is a standard Artin-Tits generator. This is the bridge that carries the universal property TauCeti.ArtinGroup.lift and its computation rule over to BraidGroup.

theorem TauCeti.BraidGroup.sigma_mul_sigma_comm {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : sigma i * sigma j = sigma j * sigma i

Disjoint crossings commute.

theorem TauCeti.BraidGroup.sigma_braid {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : sigma i * sigma j * sigma i = sigma j * sigma i * sigma j

Crossings sharing a strand satisfy the braid relation.

@[simp]

theorem TauCeti.BraidGroup.sigma_ne_one {n : ℕ} (i : Fin (n - 1)) : sigma i ≠ 1

Every elementary braid is nontrivial.

@[simp]

theorem TauCeti.BraidGroup.orderOf_sigma {n : ℕ} (i : Fin (n - 1)) : orderOf (sigma i) = 0

Every elementary braid has infinite order.

@[simp]

theorem TauCeti.BraidGroup.sigma_zpow_eq_one_iff {n : ℕ} (i : Fin (n - 1)) (k : ℤ) : sigma i ^ k = 1 ↔ k = 0

A power of an elementary braid is trivial only for the exponent 0.

@[simp]

theorem TauCeti.BraidGroup.sigma_pow_eq_one_iff {n : ℕ} (i : Fin (n - 1)) (k : ℕ) : sigma i ^ k = 1 ↔ k = 0

A natural-number power of an elementary braid is trivial only for the exponent 0.

@[simp]

theorem TauCeti.BraidGroup.exponentSum_sigma {n : ℕ} (i : Fin (n - 1)) : (ArtinGroup.exponentSum (CoxeterMatrix.A (n - 1))) (sigma i) = Multiplicative.ofAdd 1

The exponent sum of an elementary braid is one.

@[simp]

theorem TauCeti.BraidGroup.closure_range_sigma {n : ℕ} : Subgroup.closure (Set.range sigma) = ⊤

The elementary braids generate the braid group.

theorem TauCeti.BraidGroup.sigma_induction_on {n : ℕ} {p : BraidGroup n → Prop} (b : BraidGroup n) (sigma : ∀ (i : Fin (n - 1)), p (sigma i)) (one : p 1) (mul : ∀ (b b' : BraidGroup n), p b → p b' → p (b * b')) (inv : ∀ (b : BraidGroup n), p b → p b⁻¹) : p b

To prove a predicate for every braid, it suffices to prove it for the identity and elementary braids and show that it is preserved by multiplication and inverse.

def TauCeti.BraidGroup.lift {n : ℕ} {G : Type u_1} [Group G] (f : Fin (n - 1) → G) (hcomm : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i → f i * f j = f j * f i) (hbraid : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → f i * f j * f i = f j * f i * f j) : BraidGroup n →* G

The universal property of the braid-group presentation: a family satisfying distant commutation and the adjacent braid relation extends to a homomorphism from BraidGroup n.

Equations

• TauCeti.BraidGroup.lift f hcomm hbraid = TauCeti.ArtinGroup.lift (CoxeterMatrix.A (n - 1)) f ⋯

@[simp]

theorem TauCeti.BraidGroup.lift_sigma {n : ℕ} {G : Type u_1} [Group G] (f : Fin (n - 1) → G) (hcomm : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i → f i * f j = f j * f i) (hbraid : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → f i * f j * f i = f j * f i * f j) (i : Fin (n - 1)) : (lift f hcomm hbraid) (sigma i) = f i

The homomorphism constructed by BraidGroup.lift takes each elementary braid to its prescribed value.

theorem TauCeti.BraidGroup.hom_ext {n : ℕ} {G : Type u_1} [Group G] {f g : BraidGroup n →* G} (h : ∀ (i : Fin (n - 1)), f (sigma i) = g (sigma i)) : f = g

Two homomorphisms from a braid group are equal if they agree on every elementary braid. The generic ArtinGroup.hom_ext remains the registered extensionality theorem for this abbrev.

def TauCeti.BraidGroup.strand {n : ℕ} (i : Fin (n - 1)) : Fin n

The lower of the two strands crossed by sigma i.

Equations

• TauCeti.BraidGroup.strand i = ⟨↑i, ⋯⟩

def TauCeti.BraidGroup.strandSucc {n : ℕ} (i : Fin (n - 1)) : Fin n

The upper of the two strands crossed by sigma i.

Equations

• TauCeti.BraidGroup.strandSucc i = ⟨↑i + 1, ⋯⟩

@[simp]

theorem TauCeti.BraidGroup.val_strand {n : ℕ} (i : Fin (n - 1)) : ↑(strand i) = ↑i

@[simp]

theorem TauCeti.BraidGroup.val_strandSucc {n : ℕ} (i : Fin (n - 1)) : ↑(strandSucc i) = ↑i + 1

theorem TauCeti.BraidGroup.strand_ne_strandSucc {n : ℕ} (i : Fin (n - 1)) : strand i ≠ strandSucc i

The two strands crossed by an elementary braid are distinct.

theorem TauCeti.BraidGroup.strandSucc_ne_strandSucc {n : ℕ} {i j : Fin (n - 1)} (h : i ≠ j) : strandSucc i ≠ strandSucc j

Distinct braid indices have distinct upper strands.

theorem TauCeti.BraidGroup.strand_ne_strandSucc_of_succ {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j) : strand i ≠ strandSucc j

If j follows i, the lower strand of i differs from the upper strand of j.

theorem TauCeti.BraidGroup.strand_eq_strandSucc_of_succ {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j) : strand j = strandSucc i

If j follows i, its lower strand is the upper strand of i.

def TauCeti.BraidGroup.transposition {n : ℕ} (i : Fin (n - 1)) : Equiv.Perm (Fin n)

The transposition of the two strands crossed by sigma i.

Equations

• TauCeti.BraidGroup.transposition i = Equiv.swap (TauCeti.BraidGroup.strand i) (TauCeti.BraidGroup.strandSucc i)

theorem TauCeti.BraidGroup.transposition_eq_swap {n : ℕ} (i : Fin (n - 1)) : transposition i = Equiv.swap (strand i) (strandSucc i)

The defining equation of TauCeti.BraidGroup.transposition.

theorem TauCeti.BraidGroup.transposition_eq_swap_castSucc_succ {m : ℕ} (i : Fin m) : transposition i = Equiv.swap i.castSucc i.succ

The transposition underlying an elementary braid is Mathlib's adjacent-swap generator.

theorem TauCeti.BraidGroup.transposition_mul_transposition_comm {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : transposition i * transposition j = transposition j * transposition i

The adjacent transpositions underlying disjoint elementary braids commute.

theorem TauCeti.BraidGroup.transposition_braid {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : transposition i * transposition j * transposition i = transposition j * transposition i * transposition j

The adjacent transpositions underlying neighbouring elementary braids satisfy the braid relation.

def TauCeti.BraidGroup.permHom (n : ℕ) : BraidGroup n →* Equiv.Perm (Fin n)

The underlying permutation of the strands of a braid, obtained from the universal property TauCeti.BraidGroup.lift and the two relations satisfied by the adjacent transpositions.

Equations

• TauCeti.BraidGroup.permHom n = TauCeti.BraidGroup.lift TauCeti.BraidGroup.transposition ⋯ ⋯

@[simp]

theorem TauCeti.BraidGroup.permHom_sigma {n : ℕ} (i : Fin (n - 1)) : (permHom n) (sigma i) = transposition i

theorem TauCeti.BraidGroup.permHom_surjective (n : ℕ) : Function.Surjective ⇑(permHom n)

Every permutation of the strands is realised by a braid.

def TauCeti.BraidGroup.strandIncl {n : ℕ} : BraidGroup (n + 1) →* BraidGroup (n + 2)

The homomorphism from BraidGroup (n + 1) to BraidGroup (n + 2) that adds one strand and leaves it uncrossed: each elementary braid is sent to the elementary braid of the same index, and the new top strand is never touched. This is the homomorphism the Markov stabilization move is built from.

Equations

• TauCeti.BraidGroup.strandIncl = TauCeti.BraidGroup.lift (fun (i : Fin n) => TauCeti.BraidGroup.sigma i.castSucc) ⋯ ⋯

@[simp]

theorem TauCeti.BraidGroup.strandIncl_sigma {n : ℕ} (i : Fin n) : strandIncl (sigma i) = sigma i.castSucc

@[simp]

theorem TauCeti.BraidGroup.permHom_strandIncl_castSucc {n : ℕ} (b : BraidGroup (n + 1)) (i : Fin (n + 1)) : ((permHom (n + 2)) (strandIncl b)) i.castSucc = (((permHom (n + 1)) b) i).castSucc

The added strand does not interfere: on the old strands, strandIncl b permutes exactly as b does.

theorem TauCeti.BraidGroup.permHom_sigma_last (n : ℕ) : (permHom (n + 2)) (sigma (Fin.last n)) = Equiv.swap (Fin.last n).castSucc (Fin.last (n + 1))

The last elementary braid of BraidGroup (n + 2) transposes the last two strands.

@[simp]

theorem TauCeti.BraidGroup.permHom_strandIncl_last {n : ℕ} (b : BraidGroup (n + 1)) : ((permHom (n + 2)) (strandIncl b)) (Fin.last (n + 1)) = Fin.last (n + 1)

The strand added by strandIncl is left where it is.

def TauCeti.BraidGroup.pureSubgroup (n : ℕ) : Subgroup (BraidGroup n)

The pure braid group: the braids that return every strand to its own position.

Equations

• TauCeti.BraidGroup.pureSubgroup n = (TauCeti.BraidGroup.permHom n).ker

@[simp]

theorem TauCeti.BraidGroup.mem_pureSubgroup {n : ℕ} {b : BraidGroup n} : b ∈ pureSubgroup n ↔ (permHom n) b = 1

instance TauCeti.BraidGroup.instNormalPureSubgroup {n : ℕ} : (pureSubgroup n).Normal

theorem TauCeti.BraidGroup.sigma_zpow_mem_pureSubgroup_iff {n : ℕ} (i : Fin (n - 1)) (k : ℤ) : sigma i ^ k ∈ pureSubgroup n ↔ Even k

An integer power of an elementary braid is pure exactly when its exponent is even.

theorem TauCeti.BraidGroup.sigma_pow_mem_pureSubgroup_iff {n : ℕ} (i : Fin (n - 1)) (k : ℕ) : sigma i ^ k ∈ pureSubgroup n ↔ Even k

A natural-number power of an elementary braid is pure exactly when its exponent is even.

theorem TauCeti.BraidGroup.sigma_sq_mem_pureSubgroup {n : ℕ} (i : Fin (n - 1)) : sigma i ^ 2 ∈ pureSubgroup n

The square of an elementary braid is a pure braid: the two strands cross twice and end where they started.

theorem TauCeti.BraidGroup.sigma_not_mem_pureSubgroup {n : ℕ} (i : Fin (n - 1)) : sigma i ∉ pureSubgroup n

An elementary braid is not pure: it exchanges the two strands that it crosses.

theorem TauCeti.BraidGroup.not_commute_sigma {n : ℕ} {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : ¬Commute (sigma i) (sigma j)

Two elementary braids sharing a strand do not commute.

theorem TauCeti.BraidGroup.exists_not_commute {n : ℕ} (h : 3 ≤ n) : ∃ (a : BraidGroup n) (b : BraidGroup n), ¬Commute a b

The braid group on at least three strands is nonabelian: the first two elementary braids share a strand, so they do not commute.