Timings for Adjoint.v
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences.
Require Import WildCat.Core.
Require Import WildCat.NatTrans.
Require Import WildCat.Equiv.
Require Import WildCat.Prod.
Require Import WildCat.Opposite.
Require Import WildCat.Yoneda.
Require Import WildCat.FunctorCat.
Require Import WildCat.Universe.
Require Import Types.Prod.
Generalizable Variables C D F G.
(** ** Notions of adjunctions in wild categories. *)
(** We try to capture a wild notion of (oo,1)-adjunctions since these are the ones that commonly appear in practice. Special cases include the standard 1-categorical adjunction.
There are notions of 2-adjunction/biadjunction/higher adjunction but it is not clear if this generality is useful.
We will define an adjunction to be an equivalence (in Type) between corresponding hom-types. This is a more immediately useful definition than others we can consider.
We should also be able to define "F having a left adjoint" as the initial object of a slice category C / F. However this seems like too much work for now, and it is not immediately obvious how it ties back to the adjunction isomorphism.
In the future, it ought to be possible to generalize this definition to live inside a given bicategory, however due to current structural issues in the WildCat library, writing down a usable definition of bicategory requires a lot of effort.
*)
(** * Definition of adjunction *)
(** ** Definition of adjunction *)
Record Adjunction {C D : Type} (F : C -> D) (G : D -> C)
`{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G} :=
{
equiv_adjunction (x : C) (y : D) : (F x $-> y) <~> (x $-> G y) ;
(** Naturality condition in both varibles seperately *)
(** The left variable is a bit trickier to state since we have opposite categories involved. *)
is1natural_equiv_adjunction_l (y : D)
: Is1Natural (A := C^op) (yon y o F)
(** We have to explicitly give a witness to the functoriality of [yon y o F]. *)
(is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
(yon (G y)) (fun x => equiv_adjunction _ y) ;
(** Naturality in the right variable *)
is1natural_equiv_adjunction_r (x : C)
: Is1Natural (opyon (F x)) (opyon x o G) (equiv_adjunction x) ;
}.
Arguments equiv_adjunction {C D F G
isgraph_C is2graph_C is01cat_C is1cat_C
isgraph_D is2graph_D is01cat_D is1cat_D
is0functor_F is0functor_G} adj x y : rename.
Arguments is1natural_equiv_adjunction_l {C D F G
isgraph_C is2graph_C is01cat_C is1cat_C
isgraph_D is2graph_D is01cat_D is1cat_D
is0functor_F is0functor_G} adj y : rename.
Arguments is1natural_equiv_adjunction_r {C D F G
isgraph_C is2graph_C is01cat_C is1cat_C
isgraph_D is2graph_D is01cat_D is1cat_D
is0functor_F is0functor_G} adj x : rename.
Global Existing Instances
is1natural_equiv_adjunction_l
is1natural_equiv_adjunction_r.
Notation "F ⊣ G" := (Adjunction F G).
(** TODO: move but where? *)
Lemma fun01_profunctor {A B C D : Type} (F : A -> B) (G : C -> D)
`{Is0Functor A B F, Is0Functor C D G}
: Fun01 (A^op * C) (B^op * D).
1: exact (functor_prod F G).
rapply is0functor_prod_functor.
Definition fun01_hom {C : Type} `{Is01Cat C}
: Fun01 (C^op * C) Type
:= @Build_Fun01 _ _ _ _ _ is0functor_hom.
(** ** Natural equivalences coming from adjunctions. *)
(** There are various bits of data we would like to extract from adjunctions. *)
Context {C D : Type} {F : C -> D} {G : D -> C}
`{Is1Cat C, Is1Cat D, !HasMorExt C, !HasMorExt D,
!Is0Functor F, !Is0Functor G, !Is1Functor F, !Is1Functor G}
(adj : Adjunction F G).
Definition natequiv_adjunction_l (y : D)
: NatEquiv (A := C^op) (yon y o F)
(** We have to explicitly give a witness to the functoriality of [yon y o F]. *)
(is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
(yon (G y)).
apply (is1natural_equiv_adjunction_l adj).
Definition natequiv_adjunction_r (x : C)
: NatEquiv (opyon (F x)) (opyon x o G).
apply (is1natural_equiv_adjunction_r adj).
(** We also have the natural equivalence in both arguments at the same time. *)
(** In order to manage the typeclass instances, we have to bundle them up into Fun01. *)
Definition natequiv_adjunction
: NatEquiv (A := C^op * D)
(fun01_compose fun01_hom (fun01_profunctor F idmap))
(fun01_compose fun01_hom (fun01_profunctor idmap G)).
1: intros [x y]; exact (equiv_adjunction adj x y).
intros [a b] [a' b'] [f g] K.
refine (_ @ ap (fun x : a $-> G b' => x $o f)
(is1natural_equiv_adjunction_r adj a b b' g K)).
exact (is1natural_equiv_adjunction_l adj _ _ _ f (g $o K)).
(** The counit of an adjunction *)
Definition adjunction_counit : NatTrans idmap (G o F).
exact (equiv_adjunction adj x (F x) (Id _)).
1: exact (is1natural_equiv_adjunction_l adj _ _ _ f (Id _)).
2: exact (is1natural_equiv_adjunction_r adj _ _ _ (fmap F f) (Id _)).
(** The unit of an adjunction *)
Definition adjunction_unit : NatTrans (F o G) idmap.
exact ((equiv_adjunction adj (G y) y)^-1 (Id _)).
1: exact (is1natural_natequiv (natequiv_inverse
(natequiv_adjunction_l _)) (G y') _ (fmap G f) _).
2: exact (is1natural_natequiv (natequiv_inverse
(natequiv_adjunction_r _)) _ _ _ (Id _)).
Lemma triangle_helper1 x y f
: equiv_adjunction adj x y f = fmap G f $o adjunction_counit x.
refine (_ @ is1natural_equiv_adjunction_r adj _ _ _ _ _).
by cbv; rewrite (cat_idr_strong f).
Lemma triangle_helper2 x y g
: (equiv_adjunction adj x y)^-1 g = adjunction_unit y $o fmap F g.
epose (n1 := is1natural_natequiv
(natequiv_inverse (natequiv_adjunction_l _)) _ _ _ _).
by rewrite cat_idl_strong.
Definition adjunction_triangle1
: Transformation
(nattrans_comp
(nattrans_prewhisker adjunction_unit F)
(nattrans_postwhisker F adjunction_counit))
(nattrans_id _).
change (?x $-> _) with (x $-> Id (F c)).
rewrite <- (eissect (equiv_adjunction adj _ _) (Id (F c))).
cbv;rewrite <- (triangle_helper2 _ (F c) (adjunction_counit _)).
Definition adjunction_triangle2
: Transformation
(nattrans_comp
(nattrans_postwhisker G adjunction_unit)
(nattrans_prewhisker adjunction_counit G))
(nattrans_id _).
change (?x $-> _) with (x $-> Id (G d)).
rewrite <- (eisretr (equiv_adjunction adj _ _) (Id (G d))).
cbv;rewrite <- (triangle_helper1 (G d) _ (adjunction_unit _)).
(** ** Building adjunctions *)
(** There are various ways to build an adjunction. *)
(** A natural equivalence between functors [D -> Type] which is also natural in the left. *)
Definition Build_Adjunction_natequiv_nat_left
{C D : Type} (F : C -> D) (G : D -> C)
`{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G}
(e : forall x, NatEquiv (opyon (F x)) (opyon x o G))
(is1nat_e : forall y, Is1Natural (A := C^op) (yon y o F)
(** We have to explicitly give a witness to the functoriality of [yon y o F]. *)
(is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
(yon (G y)) (fun x => e _ y))
: Adjunction F G.
snrapply Build_Adjunction.
intros x; apply (is1natural_natequiv (e x)).
(** A natural equivalence between functors [C^op -> Type] which is also natural in the left. *)
Definition Build_Adjunction_natequiv_nat_right
{C D : Type} (F : C -> D) (G : D -> C)
`{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G}
(e : forall y, NatEquiv (A := C^op) (yon y o F) (yon (G y))
(is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _))
(is1nat_e : forall x, Is1Natural (opyon (F x)) (opyon x o G) (fun y => e y x))
: Adjunction F G.
snrapply Build_Adjunction.
1: exact (fun x y => e y x).
1: intros y; apply (is1natural_natequiv (e y)).
(** TODO: A natural equivalence between functors [C^op * D -> Type] *)
Section UnitCounitAdjunction.
(** From the data of an adjunction: unit, counit, left triangle, right triangle *)
Context {C D : Type} (F : C -> D) (G : D -> C)
`{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G,
!Is1Functor F, !Is1Functor G}
`{!HasMorExt C, !HasMorExt D}
(ε : NatTrans (F o G) idmap)
(η : NatTrans idmap (G o F))
(t1 : Transformation
(nattrans_comp (nattrans_prewhisker ε F) (nattrans_postwhisker F η))
(nattrans_id _))
(t2 : Transformation
(nattrans_comp (nattrans_postwhisker G ε) (nattrans_prewhisker η G))
(nattrans_id _)).
(** We can construct an equivalence between homs *)
Local Definition γ a b : (F a $-> b) $<~> (a $-> G b).
srapply equiv_adjointify.
1: exact (fun x => fmap G x $o (η : _ $=> _) a).
1: exact (fun x => (ε : _ $=> _) b $o fmap F x).
refine ((fmap_comp G _ _ $@R _) $@ _).
refine (cat_assoc _ _ _ $@ _).
refine ((_ $@L (isnat η f)^$) $@ _).
refine (cat_assoc_opp _ _ _ $@ _).
refine (_ $@R _ $@ cat_idl _).
refine ((_ $@L fmap_comp F _ _) $@ _).
refine (cat_assoc_opp _ _ _ $@ _).
refine (((isnat ε g) $@R _) $@ _).
refine (cat_assoc _ _ _ $@ _).
refine (_ $@L _ $@ cat_idr _).
(** Which is natural in the left *)
Lemma is1natural_γ_l (y : D)
: Is1Natural (yon y o F) (yon (G y))
(is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
(is0functor_G := is0functor_yon (G y))
(fun x : C^op => γ x y).
nrapply (is1natural_natequiv (natequiv_inverse
(Build_NatEquiv (yon (G y)) (yon y o F) (fun x => (γ x y)^-1$) _))).
nrapply is1natural_yoneda.
nrapply is1functor_compose.
1: nrapply is1functor_op; exact _.
nrapply is1functor_opyon.
nrapply hasmorext_op; exact _.
(** And natural in the right. *)
Lemma is1natural_γ_r x
: Is1Natural (opyon (F x)) (fun x0 : D => opyon x (G x0)) (γ x).
nrapply is1natural_opyoneda.
(** Together this constructs an adjunction. *)
Definition Build_Adjunction_unit_counit : Adjunction F G.
snrapply Build_Adjunction.
End UnitCounitAdjunction.
(** * Properties of adjunctions *)
(** ** Postcomposition adjunction *)
(** There are at least two easy proofs of the following on paper:
1. Using ends: Hom(F*x,y) ≃ ∫_c Hom(Fxc,yc) ≃ ∫_c Hom(xc,Gyc) ≃ Hom(x,G*y)
2. 2-cat theory: postcomp (-)* is a 2-functor so preserves adjunctions.
*)
Lemma adjunction_postcomp (C D J : Type)
`{HasEquivs C, HasEquivs D, Is01Cat J} (F : Fun11 C D) (G : Fun11 D C)
`{!HasMorExt C, !HasMorExt D, !HasMorExt (Fun01 J C), !HasMorExt (Fun01 J D)}
: F ⊣ G -> fun11_fun01_postcomp (A:=J) F ⊣ fun11_fun01_postcomp (A:=J) G.
srapply Build_Adjunction_unit_counit.
exact (nattrans_prewhisker (adjunction_unit adj) K).
refine (_ @ is1natural_natequiv (natequiv_inverse
(natequiv_adjunction_r adj _)) _ _ _ _).
refine ((is1natural_natequiv (natequiv_inverse
(natequiv_adjunction_l adj _)) _ _ _ _)^ @ _).
refine(cat_idl_strong _ @ _^).
exact (nattrans_prewhisker (adjunction_counit adj) K).
refine (_ @ is1natural_natequiv
(natequiv_adjunction_r adj _) _ _ _ _).
refine ((is1natural_natequiv
(natequiv_adjunction_l adj _) _ _ _ _)^ @ _).
refine(cat_idl_strong _ @ _^).
exact (trans_prewhisker (adjunction_triangle1 adj)).
exact (trans_prewhisker (adjunction_triangle2 adj)).
(** We can compose adjunctions. Notice how the middle category must have equivalences. *)
Lemma adjunction_compose (A B C : Type)
(F : A -> B) (G : B -> A) (F' : B -> C) (G' : C -> B)
`{Is1Cat A, HasEquivs B, Is1Cat C}
`{!Is0Functor F, !Is0Functor G, !Is0Functor F', !Is0Functor G'}
: F ⊣ G -> F' ⊣ G' -> F' o F ⊣ G o G'.
snrapply Build_Adjunction_natequiv_nat_right.
nrefine (natequiv_compose (natequiv_adjunction_l adj1 _) _).
exact (natequiv_prewhisker (A:=A^op) (B:=B^op)
(natequiv_adjunction_l adj2 y) F).
rapply (is1natural_prewhisker G' (natequiv_adjunction_r adj1 x)).
rapply is1natural_equiv_adjunction_r.
(** Replace the left functor in an adjunction by a naturally equivalent one. *)
Lemma adjunction_natequiv_left {C D : Type} (F F' : C -> D) (G : D -> C)
`{Is1Cat C, HasEquivs D, !HasMorExt D,
!Is0Functor F, !Is0Functor F', !Is0Functor G}
: NatEquiv F F' -> F ⊣ G -> F' ⊣ G.
snrapply Build_Adjunction_natequiv_nat_right.
refine (natequiv_compose (natequiv_adjunction_l adj _) _).
rapply (natequiv_postwhisker _ (natequiv_op _ _ e)).
(** Replace the right functor in an adjunction by a naturally equivalent one. *)
Lemma adjunction_natequiv_right {C D : Type} (F : C -> D) (G G' : D -> C)
`{HasEquivs C, Is1Cat D, !HasMorExt C,
!Is0Functor F, !Is0Functor G, !Is0Functor G'}
: NatEquiv G G' -> F ⊣ G -> F ⊣ G'.
snrapply Build_Adjunction_natequiv_nat_left.
refine (natequiv_compose _ (natequiv_adjunction_r adj _)).
rapply (natequiv_postwhisker _ e).
rapply is1natural_yoneda.