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 example of this is 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