module Cat.Functor.Kan.Base where
private variable o β : Level C Cβ² D E : Precategory o β kan-lvl : β {o β oβ² ββ² oβ²β² ββ²β²} {C : Precategory o β} {Cβ² : Precategory oβ² ββ²} {D : Precategory oβ²β² ββ²β²} β Functor C D β Functor C Cβ² β Level kan-lvl {a} {b} {c} {d} {e} {f} _ _ = a β b β c β d β e β f open _=>_
Left Kan extensionsπ
Suppose we have a functor , and a functor β perhaps to be thought of as a full subcategory inclusion, where is a completion of , 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
extending to a functor . 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 along , and denote it . 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 is equipped with a natural transformation 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 is another functor with a transformation , there is a unique natural transformation which commutes with .
Note that in general the triangle commutes βweaklyβ, but when is fully faithful and is cocomplete, genuinely extends , in that 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 has a natural transformation witnessing the same βdirected commutativityβ that does for ), 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 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 be the left Kan extension of along , and suppose that is a functor. We can βapplyβ 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 preserves .
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 . Unfortunately, proof assistants; our definition of whiskering lands in , but we requires a natural transformation to .
We say that a Kan extension is absolute if it is preserved by all functors out of . 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 is already a left kan extension of along . We say that reflects this Kan extension if is a also a left extension of along .
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