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
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).
Let η := adjunit are.
Let ε := adjcounit are.
Definition restricted_adjunction_left_adjoint :
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)).
{ apply (triangle_id_left_ad are). }
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 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.
Defined.
Definition restricted_adjunction_right_adjoint :
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)).
{ apply (triangle_id_right_ad are). }
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.
Definition restricted_adjunction_unit :
nat_trans (functor_identity (full_subcat_nat_trans_is_iso η))
(restricted_adjunction_left_adjoint ∙ restricted_adjunction_right_adjoint).
Proof.
use make_nat_trans.
- intro; cbn.
use tpair.
+ apply η.
+ exact tt.
-
intros ? ? ?.
apply subtypePath; [intro; apply propproperty|].
apply (pr2 η).
Defined.
Definition restricted_adjunction_counit :
nat_trans (restricted_adjunction_right_adjoint ∙ restricted_adjunction_left_adjoint)
(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.
Lemma are_adjoints_restricted_adjunction :
are_adjoints restricted_adjunction_left_adjoint
restricted_adjunction_right_adjoint.
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.
Defined.
Lemma restricted_adjunction_equivalence :
equivalence_of_precats (full_subcat_nat_trans_is_iso η)
(full_subcat_nat_trans_is_iso ε).
Proof.
∃ (adjunction_data_from_is_left_adjoint
are_adjoints_restricted_adjunction).
split.
- intro a.
pose (isomor := make_iso _ (pr2 a) :
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_iso _ (pr2 b) :
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).
Defined.
End Restriction.
{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).
Let η := adjunit are.
Let ε := adjcounit are.
Definition restricted_adjunction_left_adjoint :
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)).
{ apply (triangle_id_left_ad are). }
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 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.
Defined.
Definition restricted_adjunction_right_adjoint :
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)).
{ apply (triangle_id_right_ad are). }
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.
Definition restricted_adjunction_unit :
nat_trans (functor_identity (full_subcat_nat_trans_is_iso η))
(restricted_adjunction_left_adjoint ∙ restricted_adjunction_right_adjoint).
Proof.
use make_nat_trans.
- intro; cbn.
use tpair.
+ apply η.
+ exact tt.
-
intros ? ? ?.
apply subtypePath; [intro; apply propproperty|].
apply (pr2 η).
Defined.
Definition restricted_adjunction_counit :
nat_trans (restricted_adjunction_right_adjoint ∙ restricted_adjunction_left_adjoint)
(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.
Lemma are_adjoints_restricted_adjunction :
are_adjoints restricted_adjunction_left_adjoint
restricted_adjunction_right_adjoint.
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.
Defined.
Lemma restricted_adjunction_equivalence :
equivalence_of_precats (full_subcat_nat_trans_is_iso η)
(full_subcat_nat_trans_is_iso ε).
Proof.
∃ (adjunction_data_from_is_left_adjoint
are_adjoints_restricted_adjunction).
split.
- intro a.
pose (isomor := make_iso _ (pr2 a) :
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_iso _ (pr2 b) :
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).
Defined.
End Restriction.