# Restriction of an adjuction to an equivalence

## Contents

• Restriction of an adjunction to an equivalence

## 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_iso {C D : category}
{F : functor C D} {G : functor C D} (eta : nat_trans F G) :
sub_precategories C.
Proof.
apply full_sub_precategory.
intro c; use make_hProp.
- exact (is_iso (eta c)).
- apply isaprop_is_iso.
Defined.

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

functor (full_subcat_nat_trans_is_iso η) (full_subcat_nat_trans_is_iso ε).
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.
apply is_iso_from_is_z_iso.
use make_is_z_isomorphism.
++ exact (post_whisker η F _).
++ assert (HH : (post_whisker η F) c · ε (F c) = identity (F c)).

assert (inv : h, is_inverse_in_precat ((post_whisker η F) c) h).
{
use tpair.
- exact (# F (inv_from_iso (make_iso _ (pr2 c')))).
- apply (functor_is_inverse_in_precat_inv_from_iso F (make_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 zz · _) 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.
Defined.

functor (full_subcat_nat_trans_is_iso ε) (full_subcat_nat_trans_is_iso η).
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.
apply is_iso_from_is_z_iso.
use make_is_z_isomorphism.
× exact (post_whisker ε G _).
× assert (HH : η (G d) · (post_whisker ε G) d = identity (G d)).
assert (inv : h, is_inverse_in_precat (post_whisker ε G d) h).
{
use tpair.
- exact (# G (inv_from_iso (make_iso _ (pr2 d')))).
- apply (functor_is_inverse_in_precat_inv_from_iso G (make_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.
Defined.

nat_trans (functor_identity (full_subcat_nat_trans_is_iso η))
Proof.
use make_nat_trans.
- intro; cbn.
use tpair.
+ apply η.
+ exact tt.
-
intros ? ? ?.
apply subtypePath; [intro; apply propproperty|].
apply (pr2 η).
Defined.

(functor_identity (full_subcat_nat_trans_is_iso ε)).
Proof.
use make_nat_trans.
- intro; cbn.
use tpair.
+ apply ε.
+ exact tt.
-
intros ? ? ?.
apply subtypePath; [intro; apply propproperty|].
apply (pr2 ε).
Defined.

Proof.
+
intro; apply subtypePath; [intro; apply propproperty|].
+
intro; apply subtypePath; [intro; apply propproperty|].
Defined.

equivalence_of_precats (full_subcat_nat_trans_is_iso η)
(full_subcat_nat_trans_is_iso ε).
Proof.
split.
- intro a.
pose (isomor := make_iso _ (pr2 a) :