Library UniMath.CategoryTheory.Adjunctions.Restriction

Restriction of an adjuction to an equivalence

Contents

  • Restriction of an adjunction to an equivalence

Require Import UniMath.Foundations.Preamble.
Require Import UniMath.Foundations.Propositions.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Subcategory.Core.
Require Import UniMath.CategoryTheory.Subcategory.Full.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.whiskering.

Local Open Scope cat.

Restriction of an adjunction to an equivalence

Restriction of an adjunction to the subcategories where the unit and counit are isos forms an equivalence
The full subcategory of C for which eta is an isomorphism
Definition full_subcat_nat_trans_is_z_iso {C D : category}
           {F : functor C D} {G : functor C D} (eta : nat_trans F G) :
  sub_precategories C.
Show proof.
  apply full_sub_precategory.
  intro c; use make_hProp.
  - exact (is_z_isomorphism (eta c)).
  - apply isaprop_is_z_isomorphism.

Section Restriction.
  Context {C D : category} {F : functor C D} {G : functor D C} (are : are_adjoints F G).

  Let η := adjunit are.
  Let ε := adjcounit are.

  Definition restricted_adjunction_left_adjoint :
    functor (full_subcat_nat_trans_is_z_iso η) (full_subcat_nat_trans_is_z_iso ε).
  Show proof.
    use make_functor; [use make_functor_data|split].
    -
      * intros c'; pose (c := precategory_object_from_sub_precategory_object _ _ c').
        use tpair.
        -- exact (F c).
        -- cbn.
           use make_is_z_isomorphism.
           ++ exact (post_whisker η F _).
           ++ assert (HH : (post_whisker η F) c · ε (F c) = identity (F c)).
             { apply (triangle_id_left_ad are). }
             
             assert (inv : ∑ h, is_inverse_in_precat ((post_whisker η F) c) h).
             {
               use tpair.
               - exact (# F (inv_from_z_iso (make_z_iso' _ (pr2 c')))).
               - cbn. apply (functor_is_inverse_in_precat_inv_from_z_iso F (make_z_iso' _ (pr2 c'))).
             }
             split.
             **
                 pose (eq := right_inverse_of_iso_is_inverse ((post_whisker η F) c) ).
                 specialize (eq (pr1 inv) (pr2 inv) (ε (F c)) HH).
                 refine (maponpaths (fun z => z · _) eq @ _).
                 apply is_inverse_in_precat1.
                 apply is_inverse_in_precat_inv.
                 exact (pr2 inv).
             ** exact HH.
    -
      intros ? ? f; cbn.
      use tpair.
      + exact (# F (precategory_morphism_from_sub_precategory_morphism _ _ _ _ f)).
      + exact tt.
    -
      intro; cbn.
      apply subtypePath; [intro; apply propproperty|].
      apply functor_id.
    -
      intros ? ? ? ? ?; cbn.
      apply subtypePath; [intro; apply propproperty|].
      apply functor_comp.

  Definition restricted_adjunction_right_adjoint :
    functor (full_subcat_nat_trans_is_z_iso ε) (full_subcat_nat_trans_is_z_iso η).
  Show proof.
    use make_functor; [use make_functor_data|split].
    -
      
      intros d'; pose (d := precategory_object_from_sub_precategory_object _ _ d').
      use tpair.
      + exact (G d).
      + cbn.
        use make_is_z_isomorphism.
        * exact (post_whisker ε G _).
        * assert (HH : η (G d) · (post_whisker ε G) d = identity (G d)).
          { apply (triangle_id_right_ad are). }
          assert (inv : ∑ h, is_inverse_in_precat (post_whisker ε G d) h).
          {
            use tpair.
            - exact (# G (inv_from_z_iso (make_z_iso' _ (pr2 d')))).
            - apply (functor_is_inverse_in_precat_inv_from_z_iso G (make_z_iso' _ (pr2 d'))).
          }
          split.
          -- exact HH.
          -- pose (eq := left_inverse_of_iso_is_inverse ((post_whisker ε G) d)).
             specialize (eq (pr1 inv) (pr2 inv) (η (G d)) HH).
             refine (maponpaths (fun z => _ · z) eq @ _).
             apply is_inverse_in_precat1.
             exact (pr2 inv).
    -
        * intros ? ? f; cbn.
          use tpair.
          -- exact (# G (precategory_morphism_from_sub_precategory_morphism _ _ _ _ f)).
          -- exact tt.
    -
      intro; cbn.
      apply subtypePath; [intro; apply propproperty|].
      apply functor_id.
    -
      intros ? ? ? ? ?; cbn.
      apply subtypePath; [intro; apply propproperty|].
      apply functor_comp.

  Definition restricted_adjunction_unit :
    nat_trans (functor_identity (full_subcat_nat_trans_is_z_iso η))
              (restricted_adjunction_left_adjoint ∙ restricted_adjunction_right_adjoint).
  Show proof.
    use make_nat_trans.
    - intro; cbn.
      use tpair.
      + apply η.
      + exact tt.
    -
      intros ? ? ?.
      apply subtypePath; [intro; apply propproperty|].
      apply (pr2 η).

  Definition restricted_adjunction_counit :
    nat_trans (restricted_adjunction_right_adjoint ∙ restricted_adjunction_left_adjoint)
              (functor_identity (full_subcat_nat_trans_is_z_iso ε)).
  Show proof.
    use make_nat_trans.
    - intro; cbn.
      use tpair.
      + apply ε.
      + exact tt.
    -
      intros ? ? ?.
      apply subtypePath; [intro; apply propproperty|].
      apply (pr2 ε).

  Lemma are_adjoints_restricted_adjunction :
    are_adjoints restricted_adjunction_left_adjoint
                 restricted_adjunction_right_adjoint.
  Show proof.
    use make_are_adjoints.
    - exact restricted_adjunction_unit.
    - exact restricted_adjunction_counit.
    - use make_form_adjunction.
      +
        intro; apply subtypePath; [intro; apply propproperty|].
        apply triangle_id_left_ad.
      +
        intro; apply subtypePath; [intro; apply propproperty|].
        apply triangle_id_right_ad.

  Lemma restricted_adjunction_equivalence :
    equivalence_of_cats (full_subcat_nat_trans_is_z_iso η)
                           (full_subcat_nat_trans_is_z_iso ε).
  Show proof.
    exists (adjunction_data_from_is_left_adjoint
         are_adjoints_restricted_adjunction).
    split.
    - intro a.
      pose (isomor := make_z_iso' _ (pr2 a) :
                        z_iso (pr1 a) (pr1 (right_adjoint are_adjoints_restricted_adjunction
                                           (left_adjoint are_adjoints_restricted_adjunction a)))).
      apply (iso_in_precat_is_iso_in_subcat C _ _ _ isomor).
    - intro b.
      cbn.
      pose (isomor := make_z_iso' _ (pr2 b) :
                        z_iso (pr1 (left_adjoint are_adjoints_restricted_adjunction
                                   (right_adjoint are_adjoints_restricted_adjunction b))) (pr1 b)).
      apply (iso_in_precat_is_iso_in_subcat _ _ _ _ isomor).

End Restriction.