Library UniMath.CategoryTheory.DisplayedCats.Adjunctions

Contents:

Definition of homset correspondences for a displayed adjunction.
Homset correspondences are weak equivalences.
The right adjoint functor of a displayed adjunction preserves cartesian morphisms.

Written by Tamara von Glehn and Noam Zeilberger at the School and Workshop on Univalent Mathematics, December 2017

Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Local Open Scope cat.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences.

Section fix_disp_adjunction.

Context {C C' : category}
        (A : adjunction C C')
        {D : disp_cat C}
        {D': disp_cat C'}
        (X : disp_adjunction A D D').
Let F := left_functor A.
Let G := right_functor A.

Let FF : disp_functor F D D' := left_adj_over X.
Let GG : disp_functor G D' D := right_adj_over X.

Let η : functor_identity C ⟹ F ∙ G := adjunit A.
Let ε : G ∙ F ⟹ functor_identity C' := adjcounit A.
Let ηη : disp_nat_trans η (disp_functor_identity D) (disp_functor_composite FF GG)
    := unit_over X.
Let εε : disp_nat_trans ε (disp_functor_composite GG FF) (disp_functor_identity D')
    := counit_over X.

Local Open Scope hide_transport_scope.

Section DispHomSetIso_from_Adjunction.

  Definition homset_conj_inv {c : C} {c' : C'} (g : C ⟦c , G c'⟧) (d : D c) (d' : D' c') :
      (d -->[g ] GG _ d') -> (FF _ d -->[#F g · ε _] d') :=
    λ alpha , comp_disp (♯ FF alpha) (εε _ _).

  Definition homset_conj' {c : C} {c' : C'} (f : C'⟦F c , c'⟧) (d : D c) (d' : D' c') :
     (FF _ d -->[f ] d') -> (d -->[η _ · #G f ] GG _ d') :=
    λ beta , comp_disp (ηη _ _) (♯ GG beta).

  Definition homset_conj'_inv {c : C} {c' : C'} (f : C'⟦F c , c'⟧) (d : D c) (d' : D' c') :
    (d -->[η _ · #G f ] GG _ d') -> (FF _ d -->[f ] d').
  Show proof.

    set (equiv := φ _adj_inv_after_φ _adj A f
                : # F (η c · # G f ) · ε c' = f).
    exact (λ alpha , transportf _ equiv (homset_conj_inv _ _ _ alpha)).

  Definition homset_conj {c : C} {c' : C'} (g : C ⟦c , G c'⟧) (d : D c) (d' : D' c') :
    (FF _ d -->[#F g · ε _] d') -> (d -->[g ] GG _ d').
  Show proof.

    set (equiv := φ _adj_after_φ _adj_inv A g
                : η c · # G (# F g · ε c') = g).
    exact (λ beta , transportf _ equiv (homset_conj' _ _ _ beta)).

Naturality of homset bijections

  Open Scope mor_disp.

  Lemma homset_conj_inv_natural_precomp {c : C} {c' : C'} {g : C ⟦c , G c'⟧} {c'' : C}
      {f : C ⟦c'', c ⟧} {d : D c} {d' : D' c'} {d'' : D c''}
      (gg : d -->[g ] GG _ d') (ff : d'' -->[f ] d) :
    homset_conj_inv _ _ _ (ff ;; gg) =
    transportb _ (φ _adj_inv_natural_precomp A _ _ g _ f) (♯ FF ff ;; homset_conj_inv _ _ _ gg).
  Show proof.

    unfold homset_conj_inv.
    rewrite disp_functor_comp.
    rewrite assoc_disp.
    unfold transportb.
    rewrite mor_disp_transportf_postwhisker.
    rewrite transport_f_f.
    apply maponpaths_2, homset_property.

    Lemma homset_conj_inv_natural_postcomp {c : C} {c' : C'} {g : C ⟦c , G c'⟧} {c'' : C'}
      {f : C'⟦c', c''⟧} {d : D c} {d' : D' c'} {d'' : D' c''}
      (gg : d -->[g ] GG _ d') (ff : d' -->[f ] d'') :
    homset_conj_inv _ _ _ (gg ;; ♯ GG ff) =
    transportb _ (φ _adj_inv_natural_postcomp A _ _ g _ f) (homset_conj_inv _ _ _ gg ;; ff).
  Show proof.

    unfold homset_conj_inv.
    rewrite disp_functor_comp.
    unfold transportb.
    rewrite mor_disp_transportf_postwhisker.
    rewrite 2 assoc_disp_var.
    cbn.
    set (nat_εε := disp_nat_trans_ax εε ff).
    cbn in nat_εε. rewrite nat_εε.
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite 3 transport_f_f.
    apply maponpaths_2, homset_property.

  Lemma homset_conj'_natural_precomp {c : C} {c' : C'} {f : C'⟦F c , c'⟧} {c'' : C}
        {k : C ⟦c'', c ⟧} {d : D c} {d' : D' c'} {d'' : D c''}
        (ff : FF _ d -->[f ] d') (kk : d'' -->[k ] d) :
    homset_conj' _ _ _ (♯ FF kk ;; ff) =
    transportb _ (φ _adj_natural_precomp A _ _ f _ k) (kk ;; homset_conj' _ _ _ ff).
  Show proof.

    unfold homset_conj'.
    rewrite disp_functor_comp.
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite 2 assoc_disp.
    cbn.
    set (nat_ηη := disp_nat_trans_ax_var ηη kk).
    cbn in nat_ηη. rewrite nat_ηη.
    unfold transportb.
    rewrite mor_disp_transportf_postwhisker.
    rewrite 3 transport_f_f.
    apply maponpaths_2, homset_property.

  Lemma homset_conj'_natural_postcomp {c : C} {c' : C'} {f : C'⟦F c , c'⟧} {c'' : C'}
        {k : C'⟦c', c''⟧} {d : D c} {d' : D' c'} {d'' : D' c''}
        (ff : FF _ d -->[f ] d') (kk : d' -->[k ] d'') :
    homset_conj' _ _ _ (ff ;; kk) =
      transportb _ (φ _adj_natural_postcomp A _ _ f _ k) (homset_conj' _ _ _ ff ;; ♯ GG kk).
  Show proof.

    unfold homset_conj'.
    rewrite disp_functor_comp.
    rewrite assoc_disp_var.
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    apply maponpaths_2, homset_property.

  Lemma homset_conj_inv_after_conj' {c : C} {c' : C'} (f : C'⟦F c , c'⟧)(d : D c) (d' : D' c')
        (beta : FF _ d -->[f ] d') :
    transportf _ (φ _adj_inv_after_φ _adj A f)
     (homset_conj_inv _ _ _ (homset_conj' f d d' beta)) = beta.
  Show proof.

    unfold homset_conj'.
    cbn.
    set (eq := homset_conj_inv_natural_postcomp (ηη c d) beta).
    cbn in eq. rewrite eq.
    unfold homset_conj_inv.
    cbn.
    rewrite transport_f_b.
    assert (triangle1 : ♯ FF (ηη c d );; εε (F c) (FF c d) =
                        transportb _ (triangle_id_left_ad A c ) (id_disp _))
      by (exact ((pr1 (pr2 X)) c d)).
    cbn in triangle1.
    rewrite triangle1.
    unfold transportb.
    rewrite mor_disp_transportf_postwhisker.
    rewrite id_left_disp.
    unfold transportb.
    rewrite 2 transport_f_f.
    intermediate_path (transportf _ (idpath _) beta).
    - apply maponpaths_2, homset_property.
    - apply idpath.

  Lemma homset_conj'_after_conj_inv {c : C} {c' : C'} {g : C ⟦c , G c'⟧} {d : D c} (d' : D' c')
        (alpha : d -->[g ] GG _ d') :
    transportf _ (φ _adj_after_φ _adj_inv A g)
     (homset_conj' _ _ _ (homset_conj_inv g d d' alpha)) = alpha.
    unfold homset_conj_inv.
    cbn.
    set (eq := homset_conj'_natural_precomp (εε c' d') alpha).
    cbn in eq. rewrite eq.
    unfold homset_conj'.
    cbn.
    rewrite transport_f_b.
    assert (triangle2 : (ηη (G c') (GG c' d');; ♯ GG (εε c' d')) =
       transportb _ (triangle_id_right_ad A c') (id_disp _)) by (exact (pr2 (pr2 X) c' d')).
    cbn in triangle2.
    rewrite triangle2.
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite id_right_disp.
    unfold transportb.
    rewrite 2 transport_f_f.
    intermediate_path (transportf _ (idpath _ ) alpha).
    - apply maponpaths_2, homset_property.
    - apply idpath.
  Defined.

  Close Scope mor_disp.

homset_conj_inv and homset_conj' are weak equivalences.

  Lemma homset_conj_after_conj_inv {c : C} {c' : C'} {g : C ⟦c , G c'⟧} {d : D c} (d' : D' c')
        (alpha : d -->[g ] GG _ d') :
    homset_conj _ _ _ (homset_conj_inv _ _ _ alpha) = alpha.
  Show proof.

apply homset_conj'_after_conj_inv.

  Lemma homset_conj_inv_after_conj {c : C} {c' : C'} {g : C ⟦c , G c'⟧} (d : D c) {d' : D' c'}
        (beta : FF _ d -->[#F g · ε _] d') :
    homset_conj_inv _ _ _ (homset_conj _ _ _ beta) = beta.
  Show proof.

    unfold homset_conj.
    rewrite <- homset_conj_inv_after_conj'.
    unfold homset_conj_inv.
    rewrite disp_functor_transportf.
    rewrite mor_disp_transportf_postwhisker.
    apply maponpaths_2, homset_property.

  Lemma homset_conj'_inv_after_conj' {c : C} {c' : C'} (f : C'⟦F c , c'⟧)(d : D c) (d' : D' c')
        (beta : FF _ d -->[f ] d') :
    homset_conj'_inv _ _ _ (homset_conj' _ _ _ beta) = beta.
  Show proof.

apply homset_conj_inv_after_conj'.

  Lemma homset_conj'_after_conj'_inv {c : C} {c' : C'} (f : C'⟦F c , c'⟧) (d : D c) (d' : D' c')
        (alpha : d -->[η _ · #G f ] GG _ d') :
    homset_conj' _ _ _ (homset_conj'_inv _ _ _ alpha) = alpha.
  Show proof.

    unfold homset_conj', homset_conj'_inv.
    rewrite disp_functor_transportf.
    rewrite mor_disp_transportf_prewhisker.
    rewrite <- homset_conj'_after_conj_inv.
    apply maponpaths_2, homset_property.

  Lemma dispadjunction_hom_weq (c : C) (c' : C') (g : C ⟦c , G c'⟧) (d : D c) (d' : D' c') :
      (d -->[g ] GG _ d') ≃ (FF _ d -->[# F g · ε _] d').
  Show proof.

    exists (homset_conj_inv _ _ _).
    apply (isweq_iso _ (homset_conj _ _ _)).
    - apply homset_conj_after_conj_inv.
    - apply homset_conj_inv_after_conj.

  Lemma dispadjunction_hom_weq' (c : C) (c' : C') (f : C'⟦F c , c'⟧) (d : D c) (d' : D' c') :
       (FF _ d -->[f ] d') ≃ (d -->[η _ · # G f ] GG _ d').
  Show proof.

    exists (homset_conj' _ _ _).
    apply (isweq_iso _ (homset_conj'_inv _ _ _)).
    - apply homset_conj'_inv_after_conj'.
    - apply homset_conj'_after_conj'_inv.

End DispHomSetIso_from_Adjunction.

The right adjoint functor of a displayed adjunction preserves cartesian morphisms.

Lemma right_over_adj_preserves_cartesianness : is_cartesian_disp_functor GG.
Show proof.

  unfold is_cartesian_disp_functor.
  intros c c' f d d' ff ff_cart.
  intros c'' g d'' h.
  set (eq := φ _adj_inv_natural_postcomp A _ _ g _ f
           : # F (g · # G f ) · ε c = # F g · (ε c') · f).
  Open Scope mor_disp.
  apply (@iscontrweqb _ (∑ gg , (gg ;; ff) = transportf _ eq (homset_conj_inv _ _ _ h))).
  - apply (weqbandf (dispadjunction_hom_weq _ _ g _ _)).
    intro gg.
    cbn.
    set (eq2 := homset_conj_inv_natural_postcomp gg ff).
    cbn in eq2.
    apply weqimplimpl.
    + intro p.
      rewrite <- p.
      rewrite eq2.
      rewrite transport_f_b.
      intermediate_path (transportf _ (idpath _ ) (♯ FF gg ;; εε c' d';; ff)).
      * apply idpath.
      * apply maponpaths_2, homset_property.
    + intro p.
      set (equiv1 := homset_conj'_after_conj_inv _ h).
      set (equiv2 := homset_conj'_after_conj_inv _ (gg;; ♯ GG ff)).
      unfold homset_conj' in equiv1, equiv2.
      rewrite <- equiv1.
      rewrite <- equiv2.
      rewrite eq2.
      rewrite p.
      rewrite transport_b_f.
      rewrite disp_functor_transportf.
      rewrite mor_disp_transportf_prewhisker.
      rewrite transport_f_f.
      apply maponpaths_2, homset_property.
    + apply homsets_disp.
    + apply homsets_disp.
  - apply ff_cart.

End fix_disp_adjunction.