src/Adjoints_ch9.v

   1 Generalizable All Variables.
   2 Require Import Preamble.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5 Require Import Isomorphisms_ch1_5.
   6 Require Import NaturalTransformations_ch7_4.
   7 Require Import NaturalIsomorphisms_ch7_5.
   8 Require Import MonoidalCategories_ch7_8.
   9
  10 (*******************************************************************************)
  11 (* Chapter 9: Adjoints                                                         *)
  12 (*******************************************************************************)
  13
  14 Class Adjunction `{C:Category}`{D:Category}{Fobj}{Gobj}(L:Functor D C Fobj)(R:Functor C D Gobj) :=
  15 { adj_counit : functor_id D ~~~> L >>>> R
  16 ; adj_unit   : R >>>> L          ~~~> functor_id C
  17 ; adj_pf1    : forall (X:C)(Y:D), id (L Y) ~~ (L \ (adj_counit Y)) >>> (adj_unit (L Y))
  18 ; adj_pf2    : forall (X:C)(Y:D), id (R X) ~~ (adj_counit (R X)) >>> (R \ (adj_unit X))
  19 (* FIXME: use the definition based on whiskering *)
  20 }.
  21 Notation "L -| R" := (Adjunction L R).
  22 Notation "'ε'"    := (adj_counit _).
  23 Notation "'η'"    := (adj_unit _).
  24
  25 (* Definition 9.6 "Official" *)
  26 (*
  27 Lemma homset_adjunction `(C:ECategory(V:=V))`(D:ECategory(V:=V))(L:Func C D)(R:Func D C)
  28  :  (L -| R)
  29  -> RepresentableFunctorºᑭ _ _ >>>> YonedaBiFunctor D ≃
  30     RepresentableFunctorºᑭ _ _ >>>> YonedaBiFunctor C.
  31   *)
  32   (* adjuncts are unique up to natural iso *)
  33   (* adjuncts compose *)
  34   (* adjuncts preserve limits *)
  35   (* every adjunction determines a monad, vice versa *)
  36   (* E-M category *)
  37   (* Kleisli category *)
  38   (* if C is enriched, then we get an iso of hom-sets *)
  39
  40
  41
  42
  43 (* Example 9.7: exopnentiation is right adjoint to product *)
  44
  45 (* Example 9.8: terminal object selection is right adjoint to the terminal-functor in Cat *)
  46
  47 (* Proposition 9.9: Adjoints are unique up to iso *)
  48
  49 (* Example 9.9: Product is left adjoint to diagonal, and coproduct is right adjoint; generalizes to limits/colimits *)
  50
  51
  52 (* Proposition 9.14: RAPL *)
  53
  54
  55