module Cat.Functor.Kan.Base where

Left Kan extensionsπŸ”—

Suppose we have a functor F:C→DF : \mathcal{C} \to \mathcal{D}, and a functor p:C→C′p : \mathcal{C} \to \mathcal{C}' — perhaps to be thought of as a full subcategory inclusion, where C′\mathcal{C}' is a completion of C\mathcal{C}, but the situation applies just as well to any pair of functors — which naturally fit into a commutative diagram

but as we can see this is a particularly sad commutative diagram; it’s crying out for a third edge Cβ€²β†’D\mathcal{C}' \to \mathcal{D}

extending FF to a functor Cβ€²β†’D\mathcal{C}' \to \mathcal{D}. If there exists an universal such extension (we’ll define what β€œuniversal” means in just a second), we call it the left Kan extension of FF along pp, and denote it Lan⁑pF\operatorname{Lan}_p F. Such extensions do not come for free (in a sense they’re pretty hard to come by), but concept of Kan extension can be used to rephrase the definition of both limit and adjoint functor.

A left Kan extension Lan⁑pF\operatorname{Lan}_p F is equipped with a natural transformation Ξ·:Fβ‡’Lan⁑pF∘p\eta : F \Rightarrow \operatorname{Lan}_p F \circ p witnessing the (β€œdirected”) commutativity of the triangle (so that it need not commute on-the-nose) which is universal among such transformations; Meaning that if M:Cβ€²β†’DM : \mathcal{C'} \to \mathcal{D} is another functor with a transformation Ξ±:Fβ‡’M∘p\alpha : F \Rightarrow M \circ p, there is a unique natural transformation Οƒ:Lan⁑pFβ‡’M\sigma : \operatorname{Lan}_p F \Rightarrow M which commutes with Ξ±\alpha.

Note that in general the triangle commutes β€œweakly”, but when pp is fully faithful and D\mathcal{D} is cocomplete, Lan⁑pF\operatorname{Lan}_p F genuinely extends pp, in that Ξ·\eta is a natural isomorphism.

record
  is-lan (p : Functor C C') (F : Functor C D) (L : Functor C' D) (eta : F => L F∘ p)
    : Type (kan-lvl p F) where
  field

Universality of eta is witnessed by the following fields, which essentially say that, in the diagram below (assuming MM has a natural transformation Ξ±\alpha witnessing the same β€œdirected commutativity” that Ξ·\eta does for Lan⁑pF\operatorname{Lan}_p F), the 2-cell exists and is unique.

    Οƒ : {M : Functor C' D} (Ξ± : F => M F∘ p) β†’ L => M
    Οƒ-comm : {M : Functor C' D} {Ξ± : F => M F∘ p} β†’ (Οƒ Ξ± β—‚ p) ∘nt eta ≑ Ξ±
    Οƒ-uniq : {M : Functor C' D} {Ξ± : F => M F∘ p} {Οƒ' : L => M}
           β†’ Ξ± ≑ (Οƒ' β—‚ p) ∘nt eta
           β†’ Οƒ Ξ± ≑ Οƒ'

  Οƒ-uniqβ‚‚
    : {M : Functor C' D} (Ξ± : F => M F∘ p) {σ₁' Οƒβ‚‚' : L => M}
    β†’ Ξ± ≑ (σ₁' β—‚ p) ∘nt eta
    β†’ Ξ± ≑ (Οƒβ‚‚' β—‚ p) ∘nt eta
    β†’ σ₁' ≑ Οƒβ‚‚'
  Οƒ-uniqβ‚‚ Ξ² p q = sym (Οƒ-uniq p) βˆ™ Οƒ-uniq q

  Οƒ-uniqp
    : βˆ€ {M₁ Mβ‚‚ : Functor C' D}
    β†’ {α₁ : F => M₁ F∘ p} {Ξ±β‚‚ : F => Mβ‚‚ F∘ p}
    β†’ (q : M₁ ≑ Mβ‚‚)
    β†’ PathP (Ξ» i β†’ F => q i F∘ p) α₁ Ξ±β‚‚
    β†’ PathP (Ξ» i β†’ L => q i) (Οƒ α₁) (Οƒ Ξ±β‚‚)
  Οƒ-uniqp q r = Nat-pathp refl q Ξ» c' i β†’
    Οƒ {M = q i} (r i) .Ξ· c'

  open _=>_ eta

We also provide a bundled form of this data.

record Lan (p : Functor C C') (F : Functor C D) : Type (kan-lvl p F) where
  field
    Ext     : Functor C' D
    eta     : F => Ext F∘ p
    has-lan : is-lan p F Ext eta

  module Ext = Func Ext
  open is-lan has-lan public

Right Kan extensionsπŸ”—

Our choice of universal property in the section above isn’t the only choice; we could instead require a terminal solution to the lifting problem, instead of an initial one. We can picture the terminal situation using the following diagram.

Note the same warnings about β€œweak, directed” commutativity as for left Kan extensions apply here, too. Rather than either of the triangles commuting on the nose, we have natural transformations Ξ΅\varepsilon witnessing their commutativity.

record is-ran
  (p : Functor C C') (F : Functor C D) (Ext : Functor C' D)
  (eps : Ext F∘ p => F)
  : Type (kan-lvl p F) where
  no-eta-equality

  field
    Οƒ : {M : Functor C' D} (Ξ± : M F∘ p => F) β†’ M => Ext
    Οƒ-comm : {M : Functor C' D} {Ξ² : M F∘ p => F} β†’ eps ∘nt (Οƒ Ξ² β—‚ p) ≑ Ξ²
    Οƒ-uniq : {M : Functor C' D} {Ξ² : M F∘ p => F} {Οƒ' : M => Ext}
           β†’ Ξ² ≑ eps ∘nt (Οƒ' β—‚ p)
           β†’ Οƒ Ξ² ≑ Οƒ'

  open _=>_ eps renaming (Ξ· to Ξ΅)

  Οƒ-uniqβ‚‚
    : {M : Functor C' D} (Ξ² : M F∘ p => F) {σ₁' Οƒβ‚‚' : M => Ext}
    β†’ Ξ² ≑ eps ∘nt (σ₁' β—‚ p)
    β†’ Ξ² ≑ eps ∘nt (Οƒβ‚‚' β—‚ p)
    β†’ σ₁' ≑ Οƒβ‚‚'
  Οƒ-uniqβ‚‚ Ξ² p q = sym (Οƒ-uniq p) βˆ™ Οƒ-uniq q

record Ran (p : Functor C C') (F : Functor C D) : Type (kan-lvl p F) where
  no-eta-equality
  field
    Ext     : Functor C' D
    eps     : Ext F∘ p => F
    has-ran : is-ran p F Ext eps

  module Ext = Func Ext
  open is-ran has-ran public
is-lan-is-prop
  : {p : Functor C C'} {F : Functor C D} {G : Functor C' D} {eta : F => G F∘ p}
  β†’ is-prop (is-lan p F G eta)
is-lan-is-prop {p = p} {F} {G} {eta} a b = path where
  private
    module a = is-lan a
    module b = is-lan b

  σ≑ : {M : Functor _ _} (Ξ± : F => M F∘ p) β†’ a.Οƒ Ξ± ≑ b.Οƒ Ξ±
  σ≑ Ξ± = Nat-path Ξ» x β†’ a.Οƒ-uniq (sym b.Οƒ-comm) Ξ·β‚š x

  open is-lan
  path : a ≑ b
  path i .Οƒ Ξ± = σ≑ Ξ± i
  path i .Οƒ-comm {Ξ± = Ξ±} =
    is-propβ†’pathp (Ξ» i β†’ Nat-is-set ((σ≑ Ξ± i β—‚ p) ∘nt eta) Ξ±)
      (a.Οƒ-comm {Ξ± = Ξ±}) (b.Οƒ-comm {Ξ± = Ξ±})
      i
  path i .Οƒ-uniq {Ξ± = Ξ±} Ξ² =
    is-propβ†’pathp (Ξ» i β†’ Nat-is-set (σ≑ Ξ± i) _)
      (a.Οƒ-uniq Ξ²) (b.Οƒ-uniq Ξ²)
      i

is-ran-is-prop
  : {p : Functor C C'} {F : Functor C D} {G : Functor C' D} {eps : G F∘ p => F}
  β†’ is-prop (is-ran p F G eps)
is-ran-is-prop {p = p} {F} {G} {eps} a b = path where
  private
    module a = is-ran a
    module b = is-ran b

  σ≑ : {M : Functor _ _} (Ξ± : M F∘ p => F) β†’ a.Οƒ Ξ± ≑ b.Οƒ Ξ±
  σ≑ Ξ± = Nat-path Ξ» x β†’ a.Οƒ-uniq (sym b.Οƒ-comm) Ξ·β‚š x

  open is-ran
  path : a ≑ b
  path i .Οƒ Ξ± = σ≑ Ξ± i
  path i .Οƒ-comm {Ξ² = Ξ±} =
    is-propβ†’pathp (Ξ» i β†’ Nat-is-set (eps ∘nt (σ≑ Ξ± i β—‚ p)) Ξ±)
      (a.Οƒ-comm {Ξ² = Ξ±}) (b.Οƒ-comm {Ξ² = Ξ±})
      i
  path i .Οƒ-uniq {Ξ² = Ξ±} Ξ³ =
    is-propβ†’pathp (Ξ» i β†’ Nat-is-set (σ≑ Ξ± i) _)
      (a.Οƒ-uniq Ξ³) (b.Οƒ-uniq Ξ³)
      i

Preservation and reflection of Kan extensionsπŸ”—

Let (G:Cβ€²β†’D,Ξ·:Fβ†’G∘p)(G : C' \to D, \eta : F \to G \circ p) be the left Kan extension of F:Cβ†’DF : C \to D along p:Cβ†’Cβ€²p : C \to C', and suppose that H:Dβ†’EH : D \to E is a functor. We can β€œapply” HH to all the data of the Kan extension, obtaining the following diagram.

This looks like yet another Kan extension diagram, but it may not be universal! If this diagram is a left Kan extension, we say that HH preserves (G,Ξ·)(G, \eta).

  preserves-lan : (H : Functor D E) β†’ is-lan p F G eta β†’ Type _
  preserves-lan H _ =
    is-lan p (H F∘ F) (H F∘ G) (nat-assoc-to (H β–Έ eta))

In the diagram above, the 2-cell is simply the whiskering HΞ·H\eta. Unfortunately, proof assistants; our definition of whiskering lands in H(Gp)H(Gp), but we requires a natural transformation to (HG)p(HG)p.

We say that a Kan extension is absolute if it is preserved by all functors out of DD. An important class of examples given by adjoint functors.

  is-absolute-lan : is-lan p F G eta → Typeω
  is-absolute-lan lan =
    {o β„“ : Level} {E : Precategory o β„“} (H : Functor D E) β†’ preserves-lan H lan

It may also be the case that (HG,HΞ·)(HG, H\eta) is already a left kan extension of HFHF along pp. We say that HH reflects this Kan extension if G,Ξ·G, \eta is a also a left extension of FF along pp.

  reflects-lan
    : (H : Functor D E)
    β†’ is-lan p (H F∘ F) (H F∘ G) (nat-assoc-to (H β–Έ eta))
    β†’ Type _
  reflects-lan _ _ =
    is-lan p F G eta

We can define dual notions for right Kan extensions as well.

  preserves-ran : (H : Functor D E) β†’ is-ran p F G eps β†’ Type _
  preserves-ran H _ =
    is-ran p (H F∘ F) (H F∘ G) (nat-assoc-from (H β–Έ eps))

  is-absolute-ran : is-ran p F G eps → Typeω
  is-absolute-ran ran =
    {o β„“ : Level} {E : Precategory o β„“} (H : Functor D E) β†’ preserves-ran H ran

  reflects-ran
    : (H : Functor D E)
    β†’ is-ran p (H F∘ F) (H F∘ G) (nat-assoc-from (H β–Έ eps))
    β†’ Type _
  reflects-ran _ _ =
    is-ran p F G eps