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 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 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