Library UniMath.CategoryTheory.Adjunctions.Examples
Examples of adjunctions
- The binary delta_functor is left adjoint to binproduct_functor
- The general delta functor is left adjoint to the general product
functor
- The bincoproduct_functor is left adjoint to the binary delta functor
- The general coproduct functor is left adjoint to the general delta
functor
- Swapping of arguments in functor categories
- Adjunctions are closed under natural isomorphism
- Composition of adjunctions
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.whiskering.
Local Open Scope cat.
Section bindelta_functor_adjunction.
Context {C : category} (PC : BinProducts C).
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.whiskering.
Local Open Scope cat.
Section bindelta_functor_adjunction.
Context {C : category} (PC : BinProducts C).
The binary delta_functor is left adjoint to binproduct_functor
Lemma is_left_adjoint_bindelta_functor : is_left_adjoint (bindelta_functor C).
Show proof.
End bindelta_functor_adjunction.
Section delta_functor_adjunction.
Context (I : UU) {C : category} (PC : Products I C).
Show proof.
apply (tpair _ (binproduct_functor PC)).
use tpair.
- split.
+ use tpair.
* simpl; intro x.
apply (BinProductArrow _ _ (identity x) (identity x)).
* abstract (intros p q f; simpl;
now rewrite precompWithBinProductArrow, id_right, postcompWithBinProductArrow, id_left).
+ use tpair.
* simpl; intro x; split; [ apply BinProductPr1 | apply BinProductPr2 ].
* abstract (intros p q f; unfold catbinprodmor, compose; simpl;
now rewrite BinProductOfArrowsPr1, BinProductOfArrowsPr2).
- abstract (split; simpl; intro x;
[ unfold catbinprodmor, compose; simpl;
now rewrite BinProductPr1Commutes, BinProductPr2Commutes
| cbn; rewrite postcompWithBinProductArrow, !id_left;
apply pathsinv0, BinProduct_endo_is_identity;
[ apply BinProductPr1Commutes | apply BinProductPr2Commutes ]]).
use tpair.
- split.
+ use tpair.
* simpl; intro x.
apply (BinProductArrow _ _ (identity x) (identity x)).
* abstract (intros p q f; simpl;
now rewrite precompWithBinProductArrow, id_right, postcompWithBinProductArrow, id_left).
+ use tpair.
* simpl; intro x; split; [ apply BinProductPr1 | apply BinProductPr2 ].
* abstract (intros p q f; unfold catbinprodmor, compose; simpl;
now rewrite BinProductOfArrowsPr1, BinProductOfArrowsPr2).
- abstract (split; simpl; intro x;
[ unfold catbinprodmor, compose; simpl;
now rewrite BinProductPr1Commutes, BinProductPr2Commutes
| cbn; rewrite postcompWithBinProductArrow, !id_left;
apply pathsinv0, BinProduct_endo_is_identity;
[ apply BinProductPr1Commutes | apply BinProductPr2Commutes ]]).
End bindelta_functor_adjunction.
Section delta_functor_adjunction.
Context (I : UU) {C : category} (PC : Products I C).
The general delta functor is left adjoint to the general product functor
Lemma is_left_adjoint_delta_functor :
is_left_adjoint (delta_functor I C).
Show proof.
End delta_functor_adjunction.
Section bincoproduct_functor_adjunction.
Context {C : category} (PC : BinCoproducts C).
is_left_adjoint (delta_functor I C).
Show proof.
apply (tpair _ (product_functor _ PC)).
use tpair.
- split.
+ use tpair.
* simpl; intro x.
apply (ProductArrow _ _ _ (λ _, identity x)).
* abstract (intros p q f; simpl;
now rewrite precompWithProductArrow, id_right,
postcompWithProductArrow, id_left).
+ use tpair.
* intros x i; apply ProductPr.
* abstract (intros p q f; apply funextsec; intro i; unfold compose; simpl;
now rewrite ProductOfArrowsPr).
- abstract (split; simpl; intro x;
[ apply funextsec; intro i; apply (ProductPrCommutes _ _ (λ _, x))
| cbn; rewrite postcompWithProductArrow;
apply pathsinv0, Product_endo_is_identity; intro i;
eapply pathscomp0; [|apply (ProductPrCommutes I C _ (PC x))];
apply cancel_postcomposition, maponpaths, funextsec; intro j; apply id_left]).
use tpair.
- split.
+ use tpair.
* simpl; intro x.
apply (ProductArrow _ _ _ (λ _, identity x)).
* abstract (intros p q f; simpl;
now rewrite precompWithProductArrow, id_right,
postcompWithProductArrow, id_left).
+ use tpair.
* intros x i; apply ProductPr.
* abstract (intros p q f; apply funextsec; intro i; unfold compose; simpl;
now rewrite ProductOfArrowsPr).
- abstract (split; simpl; intro x;
[ apply funextsec; intro i; apply (ProductPrCommutes _ _ (λ _, x))
| cbn; rewrite postcompWithProductArrow;
apply pathsinv0, Product_endo_is_identity; intro i;
eapply pathscomp0; [|apply (ProductPrCommutes I C _ (PC x))];
apply cancel_postcomposition, maponpaths, funextsec; intro j; apply id_left]).
End delta_functor_adjunction.
Section bincoproduct_functor_adjunction.
Context {C : category} (PC : BinCoproducts C).
The bincoproduct_functor left adjoint to delta_functor
Lemma is_left_adjoint_bincoproduct_functor : is_left_adjoint (bincoproduct_functor PC).
Show proof.
End bincoproduct_functor_adjunction.
Section coproduct_functor_adjunction.
Context (I : UU) {C : category} (PC : Coproducts I C).
Show proof.
apply (tpair _ (bindelta_functor _)).
use tpair.
- split.
+ use tpair.
* simpl; intro p; set (x := pr1 p); set (y := pr2 p).
split; [ apply (BinCoproductIn1 (PC x y)) | apply (BinCoproductIn2 (PC x y)) ].
* abstract (intros p q f; unfold catbinprodmor, compose; simpl;
now rewrite BinCoproductOfArrowsIn1, BinCoproductOfArrowsIn2).
+ use tpair.
* intro x; apply (BinCoproductArrow _ (identity x) (identity x)).
* abstract (intros p q f; simpl;
now rewrite precompWithBinCoproductArrow, postcompWithBinCoproductArrow,
id_right, id_left).
- abstract (split; simpl; intro x;
[ cbn; rewrite precompWithBinCoproductArrow, !id_right;
apply pathsinv0, BinCoproduct_endo_is_identity;
[ apply BinCoproductIn1Commutes | apply BinCoproductIn2Commutes ]
| unfold catbinprodmor, compose; simpl;
now rewrite BinCoproductIn1Commutes, BinCoproductIn2Commutes ]).
use tpair.
- split.
+ use tpair.
* simpl; intro p; set (x := pr1 p); set (y := pr2 p).
split; [ apply (BinCoproductIn1 (PC x y)) | apply (BinCoproductIn2 (PC x y)) ].
* abstract (intros p q f; unfold catbinprodmor, compose; simpl;
now rewrite BinCoproductOfArrowsIn1, BinCoproductOfArrowsIn2).
+ use tpair.
* intro x; apply (BinCoproductArrow _ (identity x) (identity x)).
* abstract (intros p q f; simpl;
now rewrite precompWithBinCoproductArrow, postcompWithBinCoproductArrow,
id_right, id_left).
- abstract (split; simpl; intro x;
[ cbn; rewrite precompWithBinCoproductArrow, !id_right;
apply pathsinv0, BinCoproduct_endo_is_identity;
[ apply BinCoproductIn1Commutes | apply BinCoproductIn2Commutes ]
| unfold catbinprodmor, compose; simpl;
now rewrite BinCoproductIn1Commutes, BinCoproductIn2Commutes ]).
End bincoproduct_functor_adjunction.
Section coproduct_functor_adjunction.
Context (I : UU) {C : category} (PC : Coproducts I C).
The general coproduct functor left adjoint to the general delta functor
Lemma is_left_adjoint_coproduct_functor :
is_left_adjoint (coproduct_functor I PC).
Show proof.
End coproduct_functor_adjunction.
is_left_adjoint (coproduct_functor I PC).
Show proof.
apply (tpair _ (delta_functor _ _)).
use tpair.
- split.
+ use tpair.
* intros p i; apply CoproductIn.
* abstract (intros p q f; apply funextsec; intro i; unfold compose; simpl;
now rewrite CoproductOfArrowsIn).
+ use tpair.
* intro x; apply (CoproductArrow _ _ _ (λ _, identity x)).
* abstract (intros p q f; simpl;
now rewrite precompWithCoproductArrow,
postcompWithCoproductArrow,
id_right, id_left).
- abstract (split; simpl; intro x;
[ cbn; rewrite precompWithCoproductArrow;
apply pathsinv0, Coproduct_endo_is_identity; intro i;
eapply pathscomp0; [|apply CoproductInCommutes];
apply maponpaths, maponpaths, funextsec; intro j; apply id_right
| apply funextsec; intro i; apply (CoproductInCommutes _ _ (λ _, x))]).
use tpair.
- split.
+ use tpair.
* intros p i; apply CoproductIn.
* abstract (intros p q f; apply funextsec; intro i; unfold compose; simpl;
now rewrite CoproductOfArrowsIn).
+ use tpair.
* intro x; apply (CoproductArrow _ _ _ (λ _, identity x)).
* abstract (intros p q f; simpl;
now rewrite precompWithCoproductArrow,
postcompWithCoproductArrow,
id_right, id_left).
- abstract (split; simpl; intro x;
[ cbn; rewrite precompWithCoproductArrow;
apply pathsinv0, Coproduct_endo_is_identity; intro i;
eapply pathscomp0; [|apply CoproductInCommutes];
apply maponpaths, maponpaths, funextsec; intro j; apply id_right
| apply funextsec; intro i; apply (CoproductInCommutes _ _ (λ _, x))]).
End coproduct_functor_adjunction.
Section functor_swap.
Local Notation "[ C , D ]" := (functor_category C D).
Lemma functor_swap {C D : precategory} {E : category} : functor C [D,E] → functor D [C,E].
Show proof.
Lemma functor_cat_swap_nat_trans {C D : precategory} {E : category}
(F G : functor C [D, E]) (α : nat_trans F G) :
nat_trans (functor_swap F) (functor_swap G).
Show proof.
Lemma functor_cat_swap (C D : precategory) (E : category) : functor [C, [D, E]] [D, [C, E]].
Show proof.
Definition id_functor_cat_swap (C D : precategory) (E : category) :
nat_trans (functor_identity [C,[D,E]])
(functor_composite (functor_cat_swap C D E) (functor_cat_swap D C E)).
Show proof.
Definition functor_cat_swap_id (C D : precategory) (E : category) :
nat_trans (functor_composite (functor_cat_swap D C E) (functor_cat_swap C D E))
(functor_identity [D,[C,E]]).
Show proof.
Lemma form_adjunction_functor_cat_swap (C D : precategory) (E : category) :
form_adjunction _ _ (id_functor_cat_swap C D E) (functor_cat_swap_id C D E).
Show proof.
Lemma are_adjoint_functor_cat_swap (C D : precategory) (E : category) :
are_adjoints (@functor_cat_swap C D E) (@functor_cat_swap D C E).
Show proof.
Lemma is_left_adjoint_functor_cat_swap (C D : precategory) (E : category) :
is_left_adjoint (functor_cat_swap C D E).
Show proof.
End functor_swap.
Local Notation "[ C , D ]" := (functor_category C D).
Lemma functor_swap {C D : precategory} {E : category} : functor C [D,E] → functor D [C,E].
Show proof.
intros F.
use tpair.
- use tpair.
+ intro d; simpl.
{ use tpair.
- use tpair.
+ intro c.
apply (pr1 (F c) d).
+ intros a b f; apply (# F f).
- abstract (split;
[ now intro x; simpl; rewrite (functor_id F)
| now intros a b c f g; simpl; rewrite (functor_comp F)]).
}
+ intros a b f; simpl.
{ use tpair.
- intros x; apply (# (pr1 (F x)) f).
- abstract (intros c d g; simpl; apply pathsinv0, nat_trans_ax).
}
- abstract (split;
[ intros d; apply (nat_trans_eq (homset_property E)); intro c; simpl; apply functor_id
| intros a b c f g; apply (nat_trans_eq (homset_property E)); intro x; simpl; apply functor_comp]).
use tpair.
- use tpair.
+ intro d; simpl.
{ use tpair.
- use tpair.
+ intro c.
apply (pr1 (F c) d).
+ intros a b f; apply (# F f).
- abstract (split;
[ now intro x; simpl; rewrite (functor_id F)
| now intros a b c f g; simpl; rewrite (functor_comp F)]).
}
+ intros a b f; simpl.
{ use tpair.
- intros x; apply (# (pr1 (F x)) f).
- abstract (intros c d g; simpl; apply pathsinv0, nat_trans_ax).
}
- abstract (split;
[ intros d; apply (nat_trans_eq (homset_property E)); intro c; simpl; apply functor_id
| intros a b c f g; apply (nat_trans_eq (homset_property E)); intro x; simpl; apply functor_comp]).
Lemma functor_cat_swap_nat_trans {C D : precategory} {E : category}
(F G : functor C [D, E]) (α : nat_trans F G) :
nat_trans (functor_swap F) (functor_swap G).
Show proof.
use tpair.
+ intros d; simpl.
use tpair.
* intro c; apply (α c).
* abstract (intros a b f; apply (nat_trans_eq_pointwise (nat_trans_ax α _ _ f) d)).
+ abstract (intros a b f; apply (nat_trans_eq (homset_property E)); intro c; simpl; apply nat_trans_ax).
+ intros d; simpl.
use tpair.
* intro c; apply (α c).
* abstract (intros a b f; apply (nat_trans_eq_pointwise (nat_trans_ax α _ _ f) d)).
+ abstract (intros a b f; apply (nat_trans_eq (homset_property E)); intro c; simpl; apply nat_trans_ax).
Lemma functor_cat_swap (C D : precategory) (E : category) : functor [C, [D, E]] [D, [C, E]].
Show proof.
use tpair.
- use tpair.
+ apply functor_swap.
+ cbn. apply functor_cat_swap_nat_trans.
- abstract (split;
[ intro F; apply (nat_trans_eq (functor_category_has_homsets _ _ (homset_property E))); simpl; intro d;
now apply (nat_trans_eq (homset_property E))
| intros F G H α β; cbn; apply (nat_trans_eq (functor_category_has_homsets _ _ (homset_property E))); intro d;
now apply (nat_trans_eq (homset_property E))]).
- use tpair.
+ apply functor_swap.
+ cbn. apply functor_cat_swap_nat_trans.
- abstract (split;
[ intro F; apply (nat_trans_eq (functor_category_has_homsets _ _ (homset_property E))); simpl; intro d;
now apply (nat_trans_eq (homset_property E))
| intros F G H α β; cbn; apply (nat_trans_eq (functor_category_has_homsets _ _ (homset_property E))); intro d;
now apply (nat_trans_eq (homset_property E))]).
Definition id_functor_cat_swap (C D : precategory) (E : category) :
nat_trans (functor_identity [C,[D,E]])
(functor_composite (functor_cat_swap C D E) (functor_cat_swap D C E)).
Show proof.
set (hsE := homset_property E).
use tpair.
+ intros F.
use tpair.
- intro c.
use tpair.
* now intro f; apply identity.
* abstract (now intros a b f; rewrite id_left, id_right).
- abstract (now intros a b f; apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right).
+ abstract (now intros a b f; apply nat_trans_eq; [apply functor_category_has_homsets|]; intro c;
apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right).
use tpair.
+ intros F.
use tpair.
- intro c.
use tpair.
* now intro f; apply identity.
* abstract (now intros a b f; rewrite id_left, id_right).
- abstract (now intros a b f; apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right).
+ abstract (now intros a b f; apply nat_trans_eq; [apply functor_category_has_homsets|]; intro c;
apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right).
Definition functor_cat_swap_id (C D : precategory) (E : category) :
nat_trans (functor_composite (functor_cat_swap D C E) (functor_cat_swap C D E))
(functor_identity [D,[C,E]]).
Show proof.
set (hsE := homset_property E).
use tpair.
+ intros F.
use tpair.
- intro c.
use tpair.
* now intro f; apply identity.
* abstract (now intros a b f; rewrite id_left, id_right).
- abstract (now intros a b f; apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right).
+ abstract (now intros a b f; apply nat_trans_eq; [apply functor_category_has_homsets|]; intro c;
apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right).
use tpair.
+ intros F.
use tpair.
- intro c.
use tpair.
* now intro f; apply identity.
* abstract (now intros a b f; rewrite id_left, id_right).
- abstract (now intros a b f; apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right).
+ abstract (now intros a b f; apply nat_trans_eq; [apply functor_category_has_homsets|]; intro c;
apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right).
Lemma form_adjunction_functor_cat_swap (C D : precategory) (E : category) :
form_adjunction _ _ (id_functor_cat_swap C D E) (functor_cat_swap_id C D E).
Show proof.
set (hsE := homset_property E).
split; intro F.
+ apply (nat_trans_eq (functor_category_has_homsets _ _ hsE)
(pr1 (pr1 (functor_cat_swap C D E) F))
(pr1 (pr1 (functor_cat_swap C D E) F))).
now intro d; apply (nat_trans_eq hsE); intro c; apply id_right.
+ apply (nat_trans_eq (functor_category_has_homsets _ _ hsE)
(pr1 (pr1 (functor_cat_swap D C E) F))
(pr1 (pr1 (functor_cat_swap D C E) F))).
now intro d; apply (nat_trans_eq hsE); intro c; apply id_left.
split; intro F.
+ apply (nat_trans_eq (functor_category_has_homsets _ _ hsE)
(pr1 (pr1 (functor_cat_swap C D E) F))
(pr1 (pr1 (functor_cat_swap C D E) F))).
now intro d; apply (nat_trans_eq hsE); intro c; apply id_right.
+ apply (nat_trans_eq (functor_category_has_homsets _ _ hsE)
(pr1 (pr1 (functor_cat_swap D C E) F))
(pr1 (pr1 (functor_cat_swap D C E) F))).
now intro d; apply (nat_trans_eq hsE); intro c; apply id_left.
Lemma are_adjoint_functor_cat_swap (C D : precategory) (E : category) :
are_adjoints (@functor_cat_swap C D E) (@functor_cat_swap D C E).
Show proof.
use tpair.
- split; [ apply id_functor_cat_swap | apply functor_cat_swap_id ].
- apply form_adjunction_functor_cat_swap.
- split; [ apply id_functor_cat_swap | apply functor_cat_swap_id ].
- apply form_adjunction_functor_cat_swap.
Lemma is_left_adjoint_functor_cat_swap (C D : precategory) (E : category) :
is_left_adjoint (functor_cat_swap C D E).
Show proof.
End functor_swap.
Section LeftAdjointIso.
Context {C D : category}
{L₁ L₂ : C ⟶ D}
(HL₁ : is_left_adjoint L₁)
(τ : nat_z_iso L₁ L₂).
Let R : D ⟶ C := right_adjoint HL₁.
Let η : functor_identity C ⟹ L₁ ∙ R := unit_from_left_adjoint HL₁.
Let ε : R ∙ L₁ ⟹ functor_identity _ := counit_from_left_adjoint HL₁.
Let η' : functor_identity C ⟹ L₂ ∙ R
:= nat_trans_comp
_ _ _
η
(post_whisker τ R).
Let ε' : R ∙ L₂ ⟹ functor_identity D
:= nat_trans_comp
_ _ _
(pre_whisker R (nat_z_iso_inv τ))
ε.
Proposition is_left_adjoint_nat_z_iso_triangle_1
: triangle_1_statement (L₂ ,, R ,, η' ,, ε').
Show proof.
Proposition is_left_adjoint_nat_z_iso_triangle_2
: triangle_2_statement (L₂ ,, R ,, η' ,, ε').
Show proof.
Definition is_left_adjoint_nat_z_iso
: is_left_adjoint L₂.
Show proof.
Context {C D : category}
{L₁ L₂ : C ⟶ D}
(HL₁ : is_left_adjoint L₁)
(τ : nat_z_iso L₁ L₂).
Let R : D ⟶ C := right_adjoint HL₁.
Let η : functor_identity C ⟹ L₁ ∙ R := unit_from_left_adjoint HL₁.
Let ε : R ∙ L₁ ⟹ functor_identity _ := counit_from_left_adjoint HL₁.
Let η' : functor_identity C ⟹ L₂ ∙ R
:= nat_trans_comp
_ _ _
η
(post_whisker τ R).
Let ε' : R ∙ L₂ ⟹ functor_identity D
:= nat_trans_comp
_ _ _
(pre_whisker R (nat_z_iso_inv τ))
ε.
Proposition is_left_adjoint_nat_z_iso_triangle_1
: triangle_1_statement (L₂ ,, R ,, η' ,, ε').
Show proof.
intros x ; cbn -[η ε].
etrans.
{
rewrite !assoc.
apply maponpaths_2.
exact (nat_trans_ax (nat_z_iso_inv τ) _ _ (η x · #R(τ x))).
}
rewrite functor_comp.
rewrite !assoc'.
etrans.
{
do 2 apply maponpaths.
apply (nat_trans_ax ε).
}
etrans.
{
apply maponpaths.
rewrite !assoc.
apply maponpaths_2.
apply (pr122 HL₁).
}
rewrite id_left.
exact (z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso τ x)).
etrans.
{
rewrite !assoc.
apply maponpaths_2.
exact (nat_trans_ax (nat_z_iso_inv τ) _ _ (η x · #R(τ x))).
}
rewrite functor_comp.
rewrite !assoc'.
etrans.
{
do 2 apply maponpaths.
apply (nat_trans_ax ε).
}
etrans.
{
apply maponpaths.
rewrite !assoc.
apply maponpaths_2.
apply (pr122 HL₁).
}
rewrite id_left.
exact (z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso τ x)).
Proposition is_left_adjoint_nat_z_iso_triangle_2
: triangle_2_statement (L₂ ,, R ,, η' ,, ε').
Show proof.
intros x ; cbn.
rewrite !assoc'.
rewrite <- functor_comp.
rewrite assoc.
etrans.
{
do 2 apply maponpaths.
apply maponpaths_2.
exact (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso τ (R x))).
}
rewrite id_left.
apply (pr222 HL₁).
rewrite !assoc'.
rewrite <- functor_comp.
rewrite assoc.
etrans.
{
do 2 apply maponpaths.
apply maponpaths_2.
exact (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso τ (R x))).
}
rewrite id_left.
apply (pr222 HL₁).
Definition is_left_adjoint_nat_z_iso
: is_left_adjoint L₂.
Show proof.
simple refine (R ,, (η' ,, ε') ,, (_ ,, _)).
- exact is_left_adjoint_nat_z_iso_triangle_1.
- exact is_left_adjoint_nat_z_iso_triangle_2.
End LeftAdjointIso.- exact is_left_adjoint_nat_z_iso_triangle_1.
- exact is_left_adjoint_nat_z_iso_triangle_2.
Section CompAdjoint.
Context {C D E : category}
{L₁ : C ⟶ D}
{L₂ : D ⟶ E}
(HL₁ : is_left_adjoint L₁)
(HL₂ : is_left_adjoint L₂).
Let R₁ : D ⟶ C := right_adjoint HL₁.
Let η₁ : functor_identity C ⟹ L₁ ∙ R₁ := unit_from_left_adjoint HL₁.
Let ε₁ : R₁ ∙ L₁ ⟹ functor_identity _ := counit_from_left_adjoint HL₁.
Let R₂ : E ⟶ D := right_adjoint HL₂.
Let η₂ : functor_identity _ ⟹ L₂ ∙ R₂ := unit_from_left_adjoint HL₂.
Let ε₂ : R₂ ∙ L₂ ⟹ functor_identity _ := counit_from_left_adjoint HL₂.
Let R' : E ⟶ C := R₂ ∙ R₁.
Let η' : functor_identity _ ⟹ L₁ ∙ L₂ ∙ R'
:= nat_trans_comp
_ _ _
η₁
(pre_whisker L₁ (post_whisker η₂ R₁)).
Let ε' : R' ∙ L₁ ∙ L₂ ⟹ functor_identity _
:= nat_trans_comp
_ _ _
(pre_whisker R₂ (post_whisker ε₁ L₂))
ε₂.
Proposition comp_is_left_adjoint_triangle_1
: triangle_1_statement (L₁ ∙ L₂ ,, R' ,, η' ,, ε').
Show proof.
Proposition comp_is_left_adjoint_triangle_2
: triangle_2_statement (L₁ ∙ L₂ ,, R' ,, η' ,, ε').
Show proof.
Definition comp_is_left_adjoint
: is_left_adjoint (L₁ ∙ L₂).
Show proof.
Context {C D E : category}
{L₁ : C ⟶ D}
{L₂ : D ⟶ E}
(HL₁ : is_left_adjoint L₁)
(HL₂ : is_left_adjoint L₂).
Let R₁ : D ⟶ C := right_adjoint HL₁.
Let η₁ : functor_identity C ⟹ L₁ ∙ R₁ := unit_from_left_adjoint HL₁.
Let ε₁ : R₁ ∙ L₁ ⟹ functor_identity _ := counit_from_left_adjoint HL₁.
Let R₂ : E ⟶ D := right_adjoint HL₂.
Let η₂ : functor_identity _ ⟹ L₂ ∙ R₂ := unit_from_left_adjoint HL₂.
Let ε₂ : R₂ ∙ L₂ ⟹ functor_identity _ := counit_from_left_adjoint HL₂.
Let R' : E ⟶ C := R₂ ∙ R₁.
Let η' : functor_identity _ ⟹ L₁ ∙ L₂ ∙ R'
:= nat_trans_comp
_ _ _
η₁
(pre_whisker L₁ (post_whisker η₂ R₁)).
Let ε' : R' ∙ L₁ ∙ L₂ ⟹ functor_identity _
:= nat_trans_comp
_ _ _
(pre_whisker R₂ (post_whisker ε₁ L₂))
ε₂.
Proposition comp_is_left_adjoint_triangle_1
: triangle_1_statement (L₁ ∙ L₂ ,, R' ,, η' ,, ε').
Show proof.
intro x.
cbn -[η₁ η₂ ε₁ ε₂].
rewrite !assoc.
rewrite <- functor_comp.
etrans.
{
apply maponpaths_2.
apply maponpaths.
rewrite functor_comp.
rewrite !assoc'.
apply maponpaths.
apply (nat_trans_ax ε₁).
}
cbn -[η₁ η₂ ε₁ ε₂].
rewrite !assoc.
etrans.
{
apply maponpaths_2.
apply maponpaths.
apply maponpaths_2.
apply (pr122 HL₁).
}
rewrite id_left.
apply (pr122 HL₂).
cbn -[η₁ η₂ ε₁ ε₂].
rewrite !assoc.
rewrite <- functor_comp.
etrans.
{
apply maponpaths_2.
apply maponpaths.
rewrite functor_comp.
rewrite !assoc'.
apply maponpaths.
apply (nat_trans_ax ε₁).
}
cbn -[η₁ η₂ ε₁ ε₂].
rewrite !assoc.
etrans.
{
apply maponpaths_2.
apply maponpaths.
apply maponpaths_2.
apply (pr122 HL₁).
}
rewrite id_left.
apply (pr122 HL₂).
Proposition comp_is_left_adjoint_triangle_2
: triangle_2_statement (L₁ ∙ L₂ ,, R' ,, η' ,, ε').
Show proof.
intro x.
cbn -[η₁ η₂ ε₁ ε₂].
rewrite !assoc'.
rewrite <- functor_comp.
etrans.
{
do 2 apply maponpaths.
rewrite functor_comp.
rewrite !assoc.
apply maponpaths_2.
refine (!_).
apply (nat_trans_ax η₂).
}
cbn -[η₁ η₂ ε₁ ε₂].
rewrite !assoc'.
etrans.
{
do 3 apply maponpaths.
apply (pr222 HL₂).
}
rewrite id_right.
apply (pr222 HL₁).
cbn -[η₁ η₂ ε₁ ε₂].
rewrite !assoc'.
rewrite <- functor_comp.
etrans.
{
do 2 apply maponpaths.
rewrite functor_comp.
rewrite !assoc.
apply maponpaths_2.
refine (!_).
apply (nat_trans_ax η₂).
}
cbn -[η₁ η₂ ε₁ ε₂].
rewrite !assoc'.
etrans.
{
do 3 apply maponpaths.
apply (pr222 HL₂).
}
rewrite id_right.
apply (pr222 HL₁).
Definition comp_is_left_adjoint
: is_left_adjoint (L₁ ∙ L₂).
Show proof.
simple refine (R' ,, (η' ,, ε') ,, (_ ,, _)).
- exact comp_is_left_adjoint_triangle_1.
- exact comp_is_left_adjoint_triangle_2.
End CompAdjoint.- exact comp_is_left_adjoint_triangle_1.
- exact comp_is_left_adjoint_triangle_2.