module Cat.Functor.Kan.Representable where

Representability of Kan extensionsπŸ”—

Like most constructions with a universal property, we can phrase the definition of Kan extensions in terms of an equivalence of Hom\mathbf{Hom} functors. This rephrasing lets us construct extensions in terms of chains of natural isomorphisms, which can be very handy!

Let p:C→C′p : \mathcal{C} \to \mathcal{C}', and F:C→DF : \mathcal{C} \to \mathcal{D}, and (G,η)(G, \eta) be a candidate for a left extension, as in the following diagram.

Any such pair (G,Ξ·)(G, \eta) induces a natural transformation DCβ€²(G,βˆ’)β†’DC(F,βˆ’βˆ˜p)D^{C'}(G, -) \to D^{C}(F, - \circ p).

  Hom-from-precompose
    : F => G F∘ p
    β†’ Hom-from Cat[ C' , D ] G => Hom-from Cat[ C , D ] F F∘ precompose p
  Hom-from-precompose eta .Ξ· H Ξ± = (Ξ± β—‚ p) ∘nt eta
  Hom-from-precompose eta .is-natural H K Ξ± = funext Ξ» Ξ² β†’ [C,D].pushl β—‚-distribl

If this natural transformation is an isomorphism, then (G,Ξ·)(G, \eta) is a left Kan extension of FF along pp.

  represents→is-lan
    : (eta : F => G F∘ p)
    β†’ is-invertibleⁿ (Hom-from-precompose eta)
    β†’ is-lan p F G eta
  represents→is-lan eta nat-inv = lan where

This may seem somewhat difficult to prove at first glance, but it ends up being an exercise in shuffling data around. We can use the inverse to Hom-from-precompose eta to obtain the universal map of the extension, and factorisation/uniqueness follow directly from the fact that we have a natural isomorphism.

    module nat-inv = is-invertibleⁿ nat-inv

    lan : is-lan p F G eta
    lan .Οƒ {M} Ξ± = nat-inv.inv .Ξ· M Ξ±
    lan .Οƒ-comm {M} {Ξ±} = nat-inv.invl Ξ·β‚š M $β‚š Ξ±
    lan .Οƒ-uniq {M} {Ξ±} {Οƒβ€²} q = ap (nat-inv.inv .Ξ· M) q βˆ™ nat-inv.invr Ξ·β‚š M $β‚š Οƒβ€²

Furthermore, if (G,Ξ·)(G, \eta) is a left extension, then we can show that Hom-from-precompose eta is a natural isomorphism. The proof is yet another exercise in moving data around.

  is-lan→represents
    : {eta : F => G F∘ p}
    β†’ is-lan p F G eta
    β†’ is-invertibleⁿ (Hom-from-precompose eta)
  is-lan→represents {eta} lan =
    to-is-invertibleⁿ inv
      (Ξ» M β†’ funext Ξ» Ξ± β†’ lan .Οƒ-comm)
      (Ξ» M β†’ funext Ξ» Ξ± β†’ lan .Οƒ-uniq refl)
    where
      inv : Hom-from Cat[ C , D ] F F∘ precompose p => Hom-from Cat[ C' , D ] G
      inv .Ξ· M Ξ± = lan .Οƒ Ξ±
      inv .is-natural M N Ξ± = funext Ξ» Ξ² β†’
        lan .Οƒ-uniq (Nat-path Ξ» _ β†’ D.pushr (sym $ lan .Οƒ-comm Ξ·β‚š _))
  lanβ†’represents : Lan p F β†’ Corepresentation (Hom-from Cat[ C , D ] F F∘ precompose p)
  lan→represents lan .corep = lan .Ext
  lan→represents lan .corepresents =
    (is-invertibleⁿ→isoⁿ (is-lanβ†’represents (lan .has-lan))) ni⁻¹

  representsβ†’lan : Corepresentation (Hom-from Cat[ C , D ] F F∘ precompose p) β†’ Lan p F
  represents→lan has-corep .Ext = has-corep .corep
  represents→lan has-corep .eta = has-corep .corepresents .from .η _ idnt
  represents→lan has-corep .has-lan =
    represents→is-lan (Corep.to has-corep idnt) $
    to-is-invertibleⁿ (has-corep .corepresents .to)
      (Ξ» M β†’ funext Ξ» Ξ± β†’
        (Corep.from has-corep Ξ± β—‚ p) ∘nt Corep.to has-corep idnt β‰‘Λ˜βŸ¨ has-corep .corepresents .from .is-natural _ _ _ $β‚š idnt βŸ©β‰‘Λ˜
        Corep.to has-corep (Corep.from has-corep Ξ± ∘nt idnt)     β‰‘βŸ¨ ap (Corep.to has-corep) ([C',D].idr _) βŸ©β‰‘
        Corep.to has-corep (Corep.from has-corep Ξ±)              β‰‘βŸ¨ Corep.Ξ΅ has-corep Ξ± βŸ©β‰‘
        α ∎)
      (Ξ» M β†’ funext Ξ» Ξ± β†’
        Corep.from has-corep ((Ξ± β—‚ p) ∘nt Corep.to has-corep idnt) β‰‘βŸ¨ has-corep .corepresents .to .is-natural _ _ _ $β‚š _ βŸ©β‰‘
        Ξ± ∘nt Corep.from has-corep (Corep.to has-corep idnt)       β‰‘βŸ¨ [C',D].elimr (Corep.Ξ· has-corep idnt) βŸ©β‰‘
        α ∎)