Documentation

Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Adjunctions as Kan extensions #

We show that adjunctions are realized as Kan extensions or Kan lifts.

We also show that a left adjoint commutes with a left Kan extension. Under the assumption that IsLeftAdjoint h, the isomorphism f⁺ (g ≫ h) ≅ f⁺ g ≫ h can be accessed by Lan.CommuteWith.lanCompIso f g h.

References #

TODO #

At the moment, the results are stated for left Kan extensions and left Kan lifts. We can prove the similar results for right Kan extensions and right Kan lifts.

source
def CategoryTheory.Bicategory.Adjunction.isAbsoluteLeftKan {B : Type u} [Bicategory B] {a b : B} {f : a ⟶ b} {u : b ⟶ a} (adj : Adjunction f u) :
(LeftExtension.mk u adj.unit).IsAbsKan

For an adjuntion f ⊣ u, u is an absolute left Kan extension of the identity along f. The unit of this Kan extension is given by the unit of the adjunction.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def CategoryTheory.Bicategory.LeftExtension.IsKan.adjunction {B : Type u} [Bicategory B] {a b : B} {f : a ⟶ b} {t : LeftExtension f (CategoryStruct.id a)} (H : t.IsKan) (H' : (t.whisker f).IsKan) :
    Adjunction f t.extension

    A left Kan extension of the identity along f such that f commutes with is a right adjoint to f. The unit of this adjoint is given by the unit of the Kan extension.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.adjunction {B : Type u} [Bicategory B] {a b : B} {f : a ⟶ b} (t : LeftExtension f (CategoryStruct.id a)) (H : t.IsAbsKan) :
      Adjunction f t.extension

      For an adjuntion f ⊣ u, u is a left Kan extension of the identity along f. The unit of this Kan extension is given by the unit of the adjunction.

      Equations
      Instances For
        source
        theorem CategoryTheory.Bicategory.isLeftAdjoint_TFAE {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) :
        [IsLeftAdjoint f, HasAbsLeftKanExtension f (CategoryStruct.id a), ∃ (x : HasLeftKanExtension f (CategoryStruct.id a)), Lan.CommuteWith f (CategoryStruct.id a) f].TFAE
        source
        def CategoryTheory.Bicategory.Adjunction.isAbsoluteLeftKanLift {B : Type u} [Bicategory B] {a b : B} {f : a ⟶ b} {u : b ⟶ a} (adj : Adjunction f u) :
        (LeftLift.mk f adj.unit).IsAbsKan

        For an adjuntion f ⊣ u, f is an absolute left Kan lift of the identity along u. The unit of this Kan lift is given by the unit of the adjunction.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def CategoryTheory.Bicategory.LeftLift.IsKan.adjunction {B : Type u} [Bicategory B] {a b : B} {u : b ⟶ a} {t : LeftLift u (CategoryStruct.id a)} (H : t.IsKan) (H' : (t.whisker u).IsKan) :
          Adjunction t.lift u

          A left Kan lift of the identity along u such that u commutes with is a left adjoint to u. The unit of this adjoint is given by the unit of the Kan lift.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def CategoryTheory.Bicategory.LeftLift.IsAbsKan.adjunction {B : Type u} [Bicategory B] {a b : B} {u : b ⟶ a} (t : LeftLift u (CategoryStruct.id a)) (H : t.IsAbsKan) :
            Adjunction t.lift u

            For an adjuntion f ⊣ u, f is a left Kan lift of the identity along u. The unit of this Kan lift is given by the unit of the adjunction.

            Equations
            Instances For
              source
              theorem CategoryTheory.Bicategory.isRightAdjoint_TFAE {B : Type u} [Bicategory B] {a b : B} (u : b ⟶ a) :
              [IsRightAdjoint u, HasAbsLeftKanLift u (CategoryStruct.id a), ∃ (x : HasLeftKanLift u (CategoryStruct.id a)), LanLift.CommuteWith u (CategoryStruct.id a) u].TFAE
              source
              def CategoryTheory.Bicategory.LeftExtension.isKanOfWhiskerLeftAdjoint {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} (H : t.IsKan) {x : B} {h : c ⟶ x} {u : x ⟶ c} (adj : Adjunction h u) :
              (t.whisker h).IsKan

              A left adjoint commutes with a left Kan extension.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance CategoryTheory.Bicategory.LeftExtension.instCommuteWithOfIsLeftAdjoint {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} {h : c ⟶ x} [IsLeftAdjoint h] [HasLeftKanExtension f g] :
                Lan.CommuteWith f g h