kenzo/examples/10_Programming_the_Kan_theory.ipynb

In [1]:

(ql:quickload "kenzo")
(in-package :cat)

To load "kenzo":
  Load 1 ASDF system:
    kenzo
; Loading "kenzo"

Out[1]:

#<PACKAGE "CAT">

Programming the Kan theory¶

Introduction¶

Let us recall some definitions in relation with the Kan simplicial sets.

Definition 1. A Kan "horn" of dimension $n$ and index $i$ is a collection of $n$ simplices of dimension $(n-1)$, noted $(\sigma_0, \ldots, \sigma_{i-1}, \sigma_{i+1}, \ldots, \sigma_n)$, such that the following conditions are fulfilled: $$ \partial_j\sigma_k=\partial_k\sigma_{j+1},\quad k \not= i,\quad j+1 \not= i, \quad 0 \leq j \leq n-1, \quad 0 \leq k \leq n-1, \quad k \leq j. $$ Note that there is no $\sigma_i$ term in the list above; in a sense, the Kan process consists in constructing the missing $\sigma_i$ to be considered as a "composition" of the given $\sigma_j$'s.

Example¶

We are going to work with the simplices of $\Delta^\mathbb{N}$. The set $(\sigma_1, \sigma_2) = $ ((0 2), (0 1)) is a Kan horn of dimension 2 and index 0. In effect, $\partial_1\sigma_1=\partial_1\sigma_2 =$ (0). Likewise, the two sets ((1 2), (0 1)) and ((1 2), (0 2)) are Kan horns of dimension 2 and of respective index 1 and 2. Of course, this definition applies equally if the simplices are degenerate.

Definition 2. A filling of a Kan horn $(\sigma_0, \ldots, \sigma_{i-1}, \sigma_{i+1}, \ldots, \sigma_n)$, is an $n$-simplex $\tilde{\sigma}$, such that for every $j \not= i$, $\partial_j\tilde{\sigma}=\sigma_j.$

Example¶

A filling of ((0 2), (0 1)) is the 2-simplex (0 1 2). A filling of the Kan horn ((1 1), (0 1)) is the degenerate 2-simplex (0 1 1). A filling of the vertex (0) is the degenerate 1-simplex (0 0).

Definition 3. A simplicial set is a Kan simplicial set if for every hat there exists a filling.

In a constructive context, an algorithm must be provided able to compute a solution for the Kan problem. In the Kenzo program, a Kan simplicial-set has an extra slot kfll devoted to this problem.

Representation of a Kan simplicial set¶

A Kan simplicial set is implemented as an instance of the class KAN, subclass of the class SIMPLICIAL-SET.

commonlisp
(DEFCLASS KAN (simplicial-set)
  ((kfll :type kfll :initarg :kfll :reader kfll1)))

We recall that this new class inherits also from the class CHAIN-COMPLEX. It has one slot of its own:

kfll

an object of type KFLL, in fact a lisp function with 3 parameters describing a Kan horn: an index (an integer), a dimension (an integer) and the Kan horn (a list of abstract simplices). This function must return a filling of the Kan horn argument, i.e. an abstract simplex satisfying the theoritical definition.

A printing method has been associated to the class KAN and the external representation of an instance is a string like [Kn Kan-Simplicial-Set], where n is the number plate of the Kenzo object.

Helpful functions on Kan simplicial sets¶

cat-init [Function]

Clear in particular *Kan-list*, the list of user created Kan simplicial sets and reset the global counter to 1.

Kan n [Function]

Retrieve in the list *Kan-list* the Kan object instance whose the Kenzo identification is n. If it does not exist, return NIL.

kfll &rest args [Macro]

With only one argument (a Kan instance) return the slot kfll of this instance. With 4 arguments like (kfll kan indx dmns horn), return a filling of the Kan horn horn, of dimension dmns and of index indx by applying the filling function value of the slot kfll of the Kan instance kan.

smst-kan smst kfll [Function]

With the filling lisp function kfll, transform the simplicial set smst in an object of type KAN (in other word, smst is modified). This is the easiest way to build a Kan simplicial set.

check-horn kan indx dmns horn [Function]

Useful verification function to check if the collection of simplices horn is a valid Kan horn of dimension dmns and of index indx in the Kan simplicial set kan. In fact this works equally if kan is a general simplicial set.

check-kan kan indx dmns horn [Function]

Useful verification function to check if the collection of simplices horn is a valid Kan horn of dimension dmns and of index indx in the Kan simplicial set kan. This verification function applies the filling function of the instance kan to the argument horn and perform the verification of the faces relations upon the resulting $dmns$-simplex.

Examples¶

Let us take again the small examples of the introduction. First we define a function dkfll, a filling function suitable for a Kan horn in $\Delta^\mathbb{N}$. The user will note that in the abstract simplices the degeneracy operators and the geometric simplices are coded in binary.

In [2]:

(defun dkfll (indx dmns horn)
     (cond ((= 1 dmns)
            (absm 1 (gmsm (first horn))))
           ((= 0 indx)
            (let ((del-1 (absm-int-ext (first horn)))
                  (del-2 (absm-int-ext (second horn))))
              (absm-ext-int
                 (cons (first del-1)
                       (cons (second del-2) (rest del-1))))))
           ((= 1 indx)
            (let ((del-0 (absm-int-ext (first horn)))
                  (del-2 (absm-int-ext (second horn))))
              (absm-ext-int
                 (cons (first del-2) del-0))))
           (t
            (let ((del-0 (absm-int-ext (first horn)))
                  (del-1 (absm-int-ext (second horn))))
              (absm-ext-int
                 (cons (first del-1) del-0))))))

Out[2]:

DKFLL

In [3]:

(def d (delta-infinity))

Out[3]:

[K1 Simplicial-Set]

In [4]:

(smst-kan d #'dkfll)

Out[4]:

[K1 Kan-Simplicial-Set]

In [5]:

(kfll d 0 1 (list (absm 0 1)))

Out[5]:

<AbSm 0 1>

In [6]:

(kfll d 0 2 (list (absm 0 5) (absm 0 3)))

Out[6]:

<AbSm - 7>

In [7]:

(kfll d 1 2 (list (absm 0 6) (absm 0 3)))

Out[7]:

<AbSm - 7>

In [8]:

(kfll d 2 2 (list (absm 0 6) (absm 0 5)))

Out[8]:

<AbSm - 7>

In [9]:

(kfll d 0 2 (list (absm 0 3) (absm 0 3)))

Out[9]:

<AbSm 1 3>

In [10]:

(kfll d 1 2 (list (absm 1 2) (absm 0 3)))

Out[10]:

<AbSm 1 3>

In [11]:

(check-hat d 1 2 (list (absm 1 2) (absm 0 3)))

Out[11]:

T

In [12]:

(check-hat d 0 1 (list (absm 0 1)))

Out[12]:

T

In [13]:

(check-kan d 0 1 (list (absm 0 1)))

---done---

Out[13]:

NIL

More elaborate examples with Kan simplicial sets will be given later in the loop spaces chapter.

Lisp files concerned in this chapter¶

kan.lisp.

[classes.lisp, macros.lisp, various.lisp].