Cerise.moe

CwF adjointes

Cadre général

On étudie une manière de construire une CwF intéressante à partir d'une adjonction.

Soit C, D deux catégories. On suppose que les deux sont lex, et ont des pullbacks strictement associatifs.
Soient F : C → D et U : D → C les adjoints à gauche et à droite respectivement.
On note η et ε l'unité et la counité de l'adjonction.

Construction

On construit une CwF comme suit :

On vérifie les axiomes d'une CwF :

Substitution

Soit σ : Δ → Γ dans C, et (A, p) : D / FΓ. On doit construire un type A[σ] dans Δ.
On pose (A[σ], p[σ]) comme le pullback de (A, p) par Fσ. C'est strictement associatif, car on a supposé cette propriété pour le pullback dans D.

Maintenant, supposons qu'on aie une section s de (A, p). On doit construire une section s[σ] de (A[σ], p[σ]).
On pose s[σ] = (id ; s ∘ Fσ) : Δ → A[σ]. On vérifie qu'on arrive bien dans le pullback de Fσ et p :
Fσ = p ∘ s ∘ Fσ (car s est une section).
C'est de plus une section de p[σ], et itérer cette construction est strictement associatif.

Extension d'un contexte

On se donne Γ et (A, p) : D / FΓ. On pose alors Γ,A = { (γ : Γ ; x : UA) | ηγ = Up x }
En d'autres termes, le diagramme suivant est cartésien dans C :

       η'
  Γ,A ——→ UA
   |       |
 π |       | Up
   ↓       ↓
   Γ ———→ UFΓ
       η

Extension d'une substitution

On se donne σ : Δ → Γ dans C, (A, p) : D / FΓ, et s une section de (A[σ], p[σ]).

          σ'
    A[σ] ———→ A
     |↑       |
 p[σ]||s      |p
     ↓|       ↓
     FΔ ————→ FΓ
          Fσ

En appliquant U à tout le monde :

           Uσ'
     UA[σ] ——→ UA ←—— Γ,A
      |↑       |       |
 Up[σ]||Us     |Up     |π
      ↓|       ↓       ↓
      UFΔ ——→ UFΓ ←——— Γ
          UFσ       η

On pose σ,s : Δ → Γ,A = (σ ; Uσ' ∘ Us ∘ ηΔ). On vérifie que c'est bien dans Γ,A :

  ηΓ ∘ σ = UFσ ∘ ηΔ               (naturalité de η)
  ηΓ ∘ σ = UFσ ∘ Up[σ] ∘ Us ∘ η   (s est une section de p[σ])
  ηΓ ∘ σ = Up ∘ Uσ' ∘ Us ∘ ηΔ     (commutativité du carré cartésien)

Donc on arrive bien dans le pullback de ηΓ et Up.

De plus, l'équation π ∘ σ,s = σ est immédiatement satisfaite.

Il reste à vérifier qu'étant donné τ : Θ → Δ on vérifie σ,s ∘ τ = σ∘τ , s[τ] dans Θ → Γ,A

σ,s ∘ τ = (σ ∘ τ ; Uσ' ∘ Us ∘ ηΔ ∘ τ)
        = (σ ∘ τ ; Uσ' ∘ Us ∘ UFτ ∘ ηΘ)             (naturalité de η)
        = (σ ∘ τ ; Uσ' ∘ Uτ' ∘ U(id ; s∘Fτ) ∘ ηΘ)   (projection depuis le pullback de Fτ et p[σ])
        = (σ ∘ τ ; Uσ' ∘ Uτ' ∘ s[τ] ∘ ηΘ)           (définition de s[τ])
        = (σ ∘ τ ; U(σ ∘ τ)' ∘ Us[τ] ∘ ηΘ)          (pullback pasting)
        = σ ∘ τ, s[τ]

Terme universel

On commence par faire la substitution π dans (A, p) pour obtenir un type dans le contexte Γ,A. On veut construire une section de p[π].

   A[π] ————→ A
    |         |
p[π]|         |p
    ↓         ↓
  F(Γ,A) ———→ FΓ
    |    Fπ   |
 Fη'|         |Fη
    ↓         ↓
   FUA ————→ FUFΓ
        FUp

On pose v = (id ; εA ∘ Fη'). On vérifie que c'est bien dans A[π], qui est un pullback — ie on vérifie que Fπ appliqué au premier élément est égal à p appliqué au deuxième élément :

Fπ = εFΓ ∘ FηΓ ∘ Fπ   (équation de l'adjonction)
Fπ = εFΓ ∘ FUp ∘ Fη'  (commutativité du carré cartésien)
Fπ = p ∘ εA ∘ Fη'     (naturalité de ε)

On vérifie alors que v se comporte bien par rapport aux substitutions :
Soit σ : Δ → Γ, et s une section de A[σ]. On peut alors former σ,s : Δ → Γ,A.
En substituant, on obtient que v[σ,s] est de type A[π][σ,s] = A[π ∘ σ,s] = A[σ]. On demande alors v[σ,s] = s :

v[σ,s] = (id ; v ∘ F(σ,s))
       = (id ; (F(σ,s) ; εA ∘ Fη' ∘ F(σ,s)))
       = (id ; (F(σ,s) ; εA ∘ Fη' ∘ (σ ; Uσ' ∘ Us ∘ ηΔ)))
       = (id ; (F(σ,s) ; εA ∘ FUσ' ∘ FUs ∘ FηΔ))               (η' est la deuxième projection du pullback Γ,A)
       = (id ; (F(σ,s) ; σ' ∘ s ∘ εFΔ ∘ FηΔ))                  (naturalité de ε)
       = (id ; (F(σ,s) ; σ' ∘ s))                              (équation de l'adjonction)
       = (id ; σ' ∘ s)                                         (pullback pasting + assoc stricte)
       = (p[σ] ∘ s ; σ' ∘ s)                                   (s est une section)
       = s                                                     (η-réduction pour le pullback)

On demande également π,v = id :

π,v = (π ; Uπ' ∘ Uv ∘ η)
    = (π ; Uπ' ∘ U(id ; εA ∘ Fη') ∘ η)
    = (π ; UεA ∘ UFη' ∘ η)               (π' est la deuxième projection du pullback A[π])
    = (π ; UεA ∘ ηUA ∘ η')               (naturalité de η)
    = (π ; η')                           (équation de l'adjonction)
    = id                                 (η-réduction pour le pullback)

On obtient donc bien une CwF. On mentionne maintenant quelques propriétés de cette CwF.

Les sections des types correspondent bijectivement avec les sections des contextes correspondants

[ TODO : est-ce que ce n'est pas simplement une conséquence des axiomes d'une CwF ? ]

Soit Γ un contexte, et (A, p) : D / FΓ un type dans le contexte Γ. Il existe une correspondance bijective entre les sections de p dans D et les sections de π : Γ,A → Γ dans C.

Soit s : FΓ → A une section de p. On construit ς : Γ → Γ,A de la manière suivante : ς := (id ; Us ∘ ηΓ).
On vérifie qu'on arrive bien dans le pullback Γ,A :

ηΓ = Up ∘ Us ∘ ηΓ     (s est une section de p)

On obtient évidemment une section de π, puisque le premier membre est id.

Soit ς : Γ → Γ,A une section de π. On construit s : FΓ → A de la manière suivante : s := εA ∘ Fη' ∘ Fς

p ∘ s = p ∘ εA ∘ Fη' ∘ Fς
      = εFΓ ∘ FUp ∘ Fη' ∘ Fς   (naturalité de ε)
      = εFΓ ∘ Fη ∘ Fπ ∘ Fς     (commutativité du carré cartésien)
      = Fπ ∘ Fς                (équation de l'adjonction)
      = id                     (ς est une section de π)

On obtient donc une section de p.

Vérifions que ces deux transformations sont bijectives :

εA ∘ Fη' ∘ F(id ; Us ∘ ηΓ) = εA ∘ FUs ∘ FηΓ    (η' est la seconde projection)
                           = s ∘ εFA ∘ FηΓ     (naturalité de ε)
                           = s                 (équation de l'adjonction)
(id ; U(εA ∘ Fη' ∘ Fς) ∘ ηΓ) = (id ; UεA ∘ UFη' ∘ UFς ∘ ηΓ)
                             = (id ; UεA ∘ ηUA ∘ η' ∘ ς)      (naturalité de η)
                             = (id ; η' ∘ ς)                  (équation de l'adjonction)
                             = (π ∘ ς ; η' ∘ ς)               (ς est une section de π)
                             = ς                              (η-réduction pour le pullback)

Produits dépendants

La CwF obtenue a des Π pour peu que D soie localement cartésienne close :
On note ⇒ pour le produit dépendant de D.

Soit Γ un contexte, (A, p) : D / FΓ un type dans le contexte Γ et (B, q) : D / F(Γ,A) un type dans le contexte étendu par A.
On pose ΠAB := F(Γ,A)⇒B muni de sa projection q* vers FΓ.

Soit s : F(Γ,A) → B une section de q. On obtient par l'adjonction (pullback ⊣ ⇒) une flèche λs : FΓ → ΠAB qui est une section de q*.

Soient u : FΓ → ΠAB une section de q*, et v : FΓ → A une section de p. On définit une flèche u·v : FΓ → B[id,v] par TODO

Exemples

On s'intéresse maintenant à des exemples particuliers de cette construction.

Préfaisceaux

Soit P une petite catégorie, et P₀ la catégorie de ses objets (evil !). Le foncteur canonique P₀ → P (que certains pourraient qualifier d'inclusion, mais je réserve ce terme à une sous-catégorie pleine) induit un morphisme géométrique essentiel surjectif G ⊣ F ⊣ U depuis le logos Psh(P) vers Psh(P₀) :̣

Comme le morphisme est surjectif, on obtient que la catégorie des coalgèbres de la comonade FU (qu'on notera EM) est équivalente à Psh(P). La catégorie de co-Kliesli K correspond à la sous-catégorie des coalgèbres colibres.
C'est important, car K a une présentation avec des objets et morphismes de Psh(P₀), qui a un pullback strictement associatif contrairement à Psh(P). Comme K est de plus cartésienne close, elle permet d'interpréter la théorie des types simples dans une sous-catégorie de Psh(P).
Toutefois, K n'est pas localament cartésienne close et ne peut donc pas interpréter les types dépendants naïvement. Le plus proche que l'on puisse faire est d'utiliser notre construction de CwF adjointe décrite précédemment avec l'adjonction F ⊣ U.

On obtient alors une CwF dont la catégorie des contextes est Psh(P), et dont les types dans un contexte Γ sont les éléments de Psh(P₀)/FΓ. Cette CwF a de plus la bonne propriété que la LCC obtenue en construisant inductivement des contextes en partant du contexte vide est Psh(P) dans son intégralité :

Tout d'abord, on prouve que tout préfaisceau A peut être construit comme un contexte en deux étapes. On commence par construire le type FA dans le contexte vide •, et on l'ajoute au contexte. On vérifie aisément que •;FA = UFA.
Ensuite, on construit un type A' dans le contexte UFA, c'est-à-dire un élément de Psh(P₀) au-dessus de FUFA, défini par :

A' p = { a : FUFA p | ∀ α, (a id)↓α = a α }
     = { a : (α : q → p) → A q | ∀ α, (a id)↓α = a α }

où ↓ désigne la restriction de A.
A' étant un sous-objet de FUFA, on utilise l'inclusion évidente ι : A' → FUFA pour obtenir le type dépendant souhaité. On prétend alors que •;FA;A' = A. En effet, ce dernier est décrit par le pullback { (x ; y) : •;FA × UA' | η x = Uι y}

•;FA;A' ————→ UA'
   |           |
   |           | Uι
   ↓           ↓
 •;FA ————→ UF(•;FA)
        η

Comme U préserve les monos, UA' est un sous-préfaisceau de UF(•;FA) = UFUFA, qui peut être exprimé par

UA' p = { x : UFUFA p | ∀ α β, (x α id)↓β = x α β }
      = { x : (α : q → p) → (β : r → q) | ∀ α β, (x α id)↓β = x α β }

Donc on peut calculer que

•;FA;A' p = { x : •;FA p | η x ∈ UA' p }
          = { x : (α : q → p) → A q | η x ∈ UA' p }
          = { x : (α : q → p) → A q | λ (α : q → p) (β : r → q) . x (α ∘ β) ∈ UA' p }
          = { x : (α : q → p) → A q | ∀ α β, (x α)↓β = x (α ∘ β) ∈ UA' p }
          = { x : (α : q → p) → A q | ∀ β, (x id)↓β = x β ∈ UA' p }

•;FA;A' est donc constitué des chaînes « cohérentes », ie déterminées par leur valeur en l'identité. Comme la restriction est celle des préfaisceaux libres, c'est-à-dire la troncature des chaînes, c'est exactement celle de A par cohérence des chaînes en question. On a bien •;FA;A' = A.