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 adjunction 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 t of the identity along f that commutes with f, in the sense that t.whisker f is a left Kan extension, 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

      An absolute left Kan extension of the identity along f is a right adjoint to f. The unit of this adjunction is given by the unit of the Kan extension.

      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 adjunction 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 t of the identity along u that commutes with u, in the sense that t.whisker u is a left Kan lift, 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

            An absolute left Kan lift of the identity along u is a left adjoint to u. The unit of this adjunction is given by the unit of the Kan lift.

            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