module Cat.Functor.Adjoint.Mate where
Matesπ
Let , be a pair of adjunctions, and let and be a pair of functors, fitting together into a diagram
which neednβt necessarily commute. By pasting with the adjunction units and counits, there is an equivalence between the sets of natural transformations and , which in one direction sends
to
We call natural transformations and mates, with respect to the adjunctions and , if they correspond under this equivalence.
open Functor module _ {oa βa ob βb oc βc od βd} {A : Precategory oa βa} {A' : Precategory ob βb} {B : Precategory oc βc} {B' : Precategory od βd} {F : Functor A B} {U : Functor B A} {F' : Functor A' B'} {U' : Functor B' A'} (Fβ£U : F β£ U) (F'β£U' : F' β£ U') (X : Functor A A') (Y : Functor B B') where private module Fβ£U = _β£_ Fβ£U module F'β£U' = _β£_ F'β£U' module U = Cat.Functor.Reasoning U module U' = Cat.Functor.Reasoning U' module F = Cat.Functor.Reasoning F module F' = Cat.Functor.Reasoning F' module X = Cat.Functor.Reasoning X module Y = Cat.Functor.Reasoning Y module A = Cat.Reasoning A module B = Cat.Reasoning B module A' = Cat.Reasoning A' module B' = Cat.Reasoning B' private Ξ· : β {x} β A.Hom x (U.β (F.β x)) Ξ· = Fβ£U.unit.Ξ· _ Ξ΅ : β {x} β B.Hom (F.β (U.β x)) x Ξ΅ = Fβ£U.counit.Ξ΅ _ Ξ·' : β {x} β A'.Hom x (U'.β (F'.β x)) Ξ·' = F'β£U'.unit.Ξ· _ Ξ΅' : β {x} β B'.Hom (F'.β (U'.β x)) x Ξ΅' = F'β£U'.counit.Ξ΅ _
Unfortunately, proof assistants: if we were to define mates by pasting, we would get a natural transformation with much worse definitional behaviour. Therefore, we calculate the mate of a transformation by hand.
mate : (X Fβ U) => (U' Fβ Y) β (F' Fβ X) => (Y Fβ F) mate Ξ± = nt module mate where module Ξ± = _=>_ Ξ± nt : (F' Fβ X) => (Y Fβ F) nt ._=>_.Ξ· _ = Ξ΅' B'.β F'.β (Ξ±.Ξ· _) B'.β F'.β (X.β Ξ·) nt ._=>_.is-natural x y f = (Ξ΅' B'.β F'.β (Ξ±.Ξ· _) B'.β F'.β (X.β Ξ·)) B'.β F'.β (X.β f) β‘β¨ B'.extendr (B'.pullr (F'.weave (X.weave (Fβ£U.unit.is-natural _ _ _)))) β©β‘ (Ξ΅' B'.β F'.β (Ξ±.Ξ· _)) B'.β F'.β (X.β (U.β (F.β f))) B'.β F'.β (X.β Ξ·) β‘β¨ B'.extendl (B'.extendr (F'.weave (Ξ±.is-natural _ _ _))) β©β‘ (Ξ΅' B'.β F'.β (U'.β (Y.β (F.β f)))) B'.β F'.β (Ξ±.Ξ· _) B'.β F'.β (X.β Ξ·) β‘β¨ B'.pushl (F'β£U'.counit.is-natural _ _ _) β©β‘ Y.β (F.β f) B'.β (Ξ΅' B'.β F'.β (Ξ±.Ξ· _) B'.β F'.β (X.β Ξ·)) β
By a very similar calculation, we can define the mate of .
mate-inv : (F' Fβ X) => (Y Fβ F) β (X Fβ U) => (U' Fβ Y) mate-inv Ξ± = nt module mate-inv where module Ξ± = _=>_ Ξ± nt : (X Fβ U) => (U' Fβ Y) nt ._=>_.Ξ· _ = U'.β (Y.β Ξ΅) A'.β U'.β (Ξ±.Ξ· _) A'.β Ξ·' nt ._=>_.is-natural x y f = (U'.β (Y.β Ξ΅) A'.β U'.β (Ξ±.Ξ· _) A'.β Ξ·') A'.β X.β (U.β f) β‘β¨ A'.extendr (A'.pullr (F'β£U'.unit.is-natural _ _ _)) β©β‘ (U'.β (Y.β Ξ΅) A'.β U'.β (Ξ±.Ξ· (U.β y))) A'.β U'.β (F'.β (X.β (U.β f))) A'.β Ξ·' β‘β¨ A'.extendl (A'.extendr (U'.weave (Ξ±.is-natural _ _ _))) β©β‘ (U'.β (Y.β Ξ΅) A'.β U'.β (Y.β (F.β (U.β f)))) A'.β U'.β (Ξ±.Ξ· _) A'.β Ξ·' β‘β¨ A'.pushl (U'.weave (Y.weave (Fβ£U.counit.is-natural _ _ f))) β©β‘ U'.β (Y.β f) A'.β U'.β (Y.β Ξ΅) A'.β U'.β (Ξ±.Ξ· _) A'.β Ξ·' β
By some rather tedious applications of the triangle identities, we
can calculate that the operations mate
and mate-inv
are inverse
equivalences.
mate-invl : β (Ξ± : (F' Fβ X) => (Y Fβ F)) β mate (mate-inv Ξ±) β‘ Ξ± mate-invl Ξ± = Nat-path Ξ» _ β Ξ΅' B'.β β F'.β (U'.β (Y.β Ξ΅) A'.β U'.β (Ξ±.Ξ· _) A'.β Ξ·') β B'.β F'.β (X.β Ξ·) β‘β¨ ap! (F'.F-β _ _ β (apβ B'._β_ refl (F'.F-β _ _))) β©β‘ Ξ΅' B'.β (F'.β (U'.β (Y.β Ξ΅)) B'.β F'.β (U'.β (Ξ±.Ξ· _)) B'.β F'.β Ξ·') B'.β F'.β (X.β Ξ·) β‘β¨ B'.extendl (B'.pulll (F'β£U'.counit.is-natural _ _ _)) β©β‘ (Y.β Ξ΅ B'.β Ξ΅') B'.β (F'.β (U'.β (Ξ±.Ξ· _)) B'.β F'.β Ξ·') B'.β F'.β (X.β Ξ·) β‘β¨ B'.extendl (B'.pulll (B'.pullr (F'β£U'.counit.is-natural _ _ _))) β©β‘ (Y.β Ξ΅ B'.β Ξ±.Ξ· _ B'.β Ξ΅') B'.β F'.β Ξ·' B'.β F'.β (X.β Ξ·) β‘β¨ B'.pulll (B'.pullr (B'.cancelr F'β£U'.zig)) β©β‘ (Y.β Ξ΅ B'.β Ξ±.Ξ· _) B'.β F'.β (X.β Ξ·) β‘β¨ B'.pullr (Ξ±.is-natural _ _ _) β©β‘ Y.β Ξ΅ B'.β Y.β (F.β Ξ·) B'.β Ξ±.Ξ· _ β‘β¨ B'.cancell (Y.annihilate Fβ£U.zig) β©β‘ Ξ±.Ξ· _ β where module Ξ± = _=>_ Ξ± mate-invr : β (Ξ± : (X Fβ U) => (U' Fβ Y)) β mate-inv (mate Ξ±) β‘ Ξ± mate-invr Ξ± = Nat-path Ξ» _ β U'.β (Y.β Ξ΅) A'.β β U'.β (Ξ΅' B'.β F'.β (Ξ±.Ξ· _) B'.β F'.β (X.β Ξ·)) β A'.β Ξ·' β‘β¨ ap! (U'.F-β _ _ β (apβ A'._β_ refl (U'.F-β _ _))) β©β‘ U'.β (Y.β Ξ΅) A'.β (U'.β Ξ΅' A'.β U'.β (F'.β (Ξ±.Ξ· _)) A'.β U'.β (F'.β (X.β Ξ·))) A'.β Ξ·' β‘β¨ apβ A'._β_ refl (A'.extendr (A'.pullr (sym (F'β£U'.unit.is-natural _ _ _)))) β©β‘ U'.β (Y.β Ξ΅) A'.β (U'.β Ξ΅' A'.β U'.β (F'.β (Ξ±.Ξ· _))) A'.β Ξ·' A'.β X.β Ξ· β‘β¨ apβ A'._β_ refl (A'.pullr (A'.extendl (sym (F'β£U'.unit.is-natural _ _ _)))) β©β‘ U'.β (Y.β Ξ΅) A'.β U'.β Ξ΅' A'.β Ξ·' A'.β Ξ±.Ξ· _ A'.β X.β Ξ· β‘β¨ apβ A'._β_ refl (A'.cancell F'β£U'.zag) β©β‘ U'.β (Y.β Ξ΅) A'.β Ξ±.Ξ· _ A'.β X.β Ξ· β‘β¨ A'.pulll (sym (Ξ±.is-natural _ _ _)) β©β‘ (Ξ±.Ξ· _ A'.β X.β (U.β Ξ΅)) A'.β X.β Ξ· β‘β¨ A'.cancelr (X.annihilate Fβ£U.zag) β©β‘ Ξ±.Ξ· _ β where module Ξ± = _=>_ Ξ± mate-is-equiv : is-equiv mate mate-is-equiv = is-isoβis-equiv (iso mate-inv mate-invl mate-invr)