GROUPOIDS

The type represents -groupoids as Kan complexes, defined as sheaves on the simplex category with values in . The type represents -groupoids, used in homotopy theory, gauge theory, and quantum physics.

In Urs, operates in graded universes from , with applications in gauge transformations , smooth groupoids , and differential cohomology .

Formation

(Groupoid Formation). The type represents -groupoids as Kan sheaves on , living in universe . The type represents -groupoids.

def Grpd (n : Nat) : U (n + 1) := Sh(Δ, Set)ₖₐₙ
def Grpd∞ : U∞ := Grpd ∞
def Δ : U₀ := Δ^n  -- Simplex category, indexed by n : Nat
(* Groupoid formation *)

Introduction

(Groupoid Constructors). Terms of are constructed via plots, composition, and horn-filling, reflecting the Kan complex structure.

def plt-grpd (n : Nat) (X : Grpd n) : Set := Plt(Δ^n, X)
def comp (n : Nat) (X : Grpd n) (g₁ g₂ : plt-grpd n X) (consec : Consecutive g₁ g₂)
  : plt-grpd n X := g₁ ∘ g₂
def fill (n k : Nat) (X : Grpd n) (h : Π (i : Fin n) (i ≠ k), plt-grpd (n-1) X)
  : plt-grpd n X := fill h
(* Groupoid constructors: plots, composition, horn-filling *)

Elimination

(Groupoid Eliminators). Eliminators for include mapping plots to paths (homotopy) and reasoning about composition.

def homotopy (X : Grpd 1) (g : plt-grpd 1 X) : Path X (source g) (target g) := g
def compose-elim (n : Nat) (X : Grpd n) (g₁ g₂ : plt-grpd n X) (consec : Consecutive g₁ g₂)
  : plt-grpd n X := comp n X g₁ g₂ consec
(* Groupoid eliminators: homotopy, composition *)

Theorems

(Horn-Filling Condition). The constructor satisfies the Kan condition, ensuring horns restrict to the given data.

def fill-horn (n k : Nat) (X : Grpd n) (h : Π (i : Fin n) (i ≠ k), plt-grpd (n-1) X)
  : Path (plt-grpd (n-1) X) (fill n k X h | Λ_k^n) (h k) := idp (plt-grpd (n-1) X) (h k)
(* Horn-filling condition *)

(Gauge Transformation in ). For a set , is a 1-groupoid, and gauge transformations induce loops, applicable to .

def BG (G : Set) : Grpd 1 := λ n, if n = 1 then G else if n = 0 then {pt} else {}
def test-gauge (G : Set) (g : G) : plt-grpd 1 (BG G) := g
def test-homotopy (G : Set) (g : G) : Path (BG G) pt pt := homotopy (BG G) (test-gauge G g)
(* Gauge transformation in BG *)

(Kan Condition Test). For a 2-groupoid , horn-filling constructs a 2-simplex, satisfying the Kan condition.

def test-horn (X : Grpd 2) (h : plt-grpd 1 X) : plt-grpd 2 X := fill 2 1 X (λ i _, if i = 0 then h else h)
def test-fill-horn (X : Grpd 2) (h : plt-grpd 1 X)
  : Path (plt-grpd 1 X) (fill 2 1 X (λ i _, if i = 0 then h else h) | Λ_1^2) h := fill-horn 2 1 X _
(* Kan condition test *)

(Gauge Equivalence). For -groupoids and , a gauge equivalence establishes a homotopy equivalence.

def gauge-eq (X Y : Grpd∞) (φ : Maps X Y) (φ' : Maps Y X) (g : Maps X X) (h : g = φ' ∘ φ)
  : Path (Grpd∞) X Y := idp _ _  -- Homotopy equivalence, Gauge equivalence lemma