BRAID GROUP

The type models the braid group on strands over a smooth set , the fundamental group of the configuration space , used in knot theory, quantum computing, and smooth geometry.

In Urs, is a type in , parameterized by and , supporting braid generators and relations, with applications to anyonic quantum gates and knot invariants.

Formation

(-Formation). The type is a type in , formed for each and , representing the braid group .

def Braid (n : Nat) (X : SmthSet) : U_0
(* Braid group type *)

Introduction

(-Introduction). Terms of type are braid elements, introduced via the constructor, representing generators for .

def braid (n : Nat) (X : SmthSet) (i : Fin (n-1)) : Braid n X
(* Braid generator sigma_i *)

Elimination

(-Elimination). The eliminator for maps braid elements to properties in , analyzing their groupoid structure.

def braid_ind (n : Nat) (X : SmthSet) (beta : Braid n X -> U_0) (h : Π (b : Braid n X), beta b) : Π (b : Braid n X), beta b
(* Eliminator for braids *)

Theorems

(Braid Relations). For , , satisfies the braid group relations, where .

def braid_rel_comm (n : Nat) (X : SmthSet) (i j : Fin (n-1)) : Path (braid i · braid j) (braid j · braid i)
    (* Commutation: σ_i · σ_j = σ_j · σ_i for |i-j| ≥ 2 *)
def braid_rel_yang (n : Nat) (X : SmthSet) (i : Fin (n-2)) : Path (braid i · braid (i+1) · braid i) (braid (i+1) · braid i · braid (i+1))
    (* Yang-Baxter: σ_i · σ_{i+1} · σ_i = σ_{i+1} · σ_i · σ_{i+1} *)
(* Braid group relations *)

(Configuration Space Link). For , , is the fundamental groupoid of .

def braid_conf (n : Nat) (X : SmthSet) : Path (Braid n X) (pi_1 (Conf n X))
(* Braid as fundamental groupoid *)

(Quantum Braiding). For , acts on as braiding operators.

def braid_qubit (n : Nat) (C H : U_0) (X : SmthSet) : Braid n X -> (Qubit C H)^n -> (Qubit C H)^n
(* Quantum braiding action *)

(Braid Group Delooping). For , the delooping of the braid group is a 1-groupoid, defined as the fundamental groupoid of .

def BB_n (n : Nat) : Grpd 1 := ℑ (Conf n ℝ^2)
(* Delooping of braid group *)