CONFIGURATION SPACE

The type models the configuration space of distinct points in a smooth set , the space of ordered -tuples , used in smooth geometry, braid groups, and stable homotopy theory.

In the cohesive type system, is a type in , parameterized by and , representing smooth configurations of points in .

Formation

(-Formation). The type is a smooth set in , formed for each and , the subspace of excluding the fat diagonal.

def Conf (n : Nat) (X : SmthSet) : SmthSet

Introduction

(-Introduction). Terms of type are -tuples of distinct points in , introduced via the constructor .

def conf (n : Nat) (X : SmthSet) (x_1 ... x_n : X)
    (p : Π (i j : Fin n), i ≠ j → x_i ≠ x_j) : Conf n X

Elimination

(-Elimination). The eliminator for maps configurations to properties in , projecting distinct points to their components.

def conf_ind (n : Nat) (X : SmthSet) (beta : Conf n X -> SmthSet)
    (h : Π (c : Conf n X), beta c) : Π (c : Conf n X), beta c

Theorems

(Projection Maps). For , the configuration space has projection maps to for each coordinate.

def proj (n : Nat) (X : SmthSet) (i : Fin n) : Conf n X -> X

(Diagonal Exclusion). The space is the complement of the fat diagonal in , ensuring distinct points.

def diag_excl (n : Nat) (X : SmthSet) : Path (Conf n X) (X^n \ Diff (Delta n X))

(Smooth Structure). For , inherits the smooth structure of , forming a smooth set.

def smooth_conf (n : Nat) (X : SmthSet)
  : SheafStr (Conf n X) ℝ^m