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

• [Riehl, Category theory in context, Proposition 6.5.2][riehl2017]

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.

def CategoryTheory.Bicategory.Adjunction.isAbsoluteLeftKan {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {u : b ⟶ a} (adj : CategoryTheory.Bicategory.Adjunction f u) : (CategoryTheory.Bicategory.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.

def CategoryTheory.Bicategory.LeftExtension.IsKan.adjunction {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.id a)} (H : t.IsKan) (H' : (t.whisker f).IsKan) : CategoryTheory.Bicategory.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.

def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.adjunction {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} (t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.id a)) (H : t.IsAbsKan) : CategoryTheory.Bicategory.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

• CategoryTheory.Bicategory.LeftExtension.IsAbsKan.adjunction t H = H.isKan.adjunction (H f)

theorem CategoryTheory.Bicategory.isLeftAdjoint_TFAE {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) : [CategoryTheory.Bicategory.IsLeftAdjoint f, CategoryTheory.Bicategory.HasAbsLeftKanExtension f (CategoryTheory.CategoryStruct.id a), ∃ (x : CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.id a)), CategoryTheory.Bicategory.Lan.CommuteWith f (CategoryTheory.CategoryStruct.id a) f].TFAE

def CategoryTheory.Bicategory.Adjunction.isAbsoluteLeftKanLift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {u : b ⟶ a} (adj : CategoryTheory.Bicategory.Adjunction f u) : (CategoryTheory.Bicategory.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.

def CategoryTheory.Bicategory.LeftLift.IsKan.adjunction {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {u : b ⟶ a} {t : CategoryTheory.Bicategory.LeftLift u (CategoryTheory.CategoryStruct.id a)} (H : t.IsKan) (H' : (t.whisker u).IsKan) : CategoryTheory.Bicategory.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.

def CategoryTheory.Bicategory.LeftLift.IsAbsKan.adjunction {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {u : b ⟶ a} (t : CategoryTheory.Bicategory.LeftLift u (CategoryTheory.CategoryStruct.id a)) (H : t.IsAbsKan) : CategoryTheory.Bicategory.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

• CategoryTheory.Bicategory.LeftLift.IsAbsKan.adjunction t H = H.isKan.adjunction (H u)

theorem CategoryTheory.Bicategory.isRightAdjoint_TFAE {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (u : b ⟶ a) : [CategoryTheory.Bicategory.IsRightAdjoint u, CategoryTheory.Bicategory.HasAbsLeftKanLift u (CategoryTheory.CategoryStruct.id a), ∃ (x : CategoryTheory.Bicategory.HasLeftKanLift u (CategoryTheory.CategoryStruct.id a)), CategoryTheory.Bicategory.LanLift.CommuteWith u (CategoryTheory.CategoryStruct.id a) u].TFAE

def CategoryTheory.Bicategory.LeftExtension.isKanOfWhiskerLeftAdjoint {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ c} {t : CategoryTheory.Bicategory.LeftExtension f g} (H : t.IsKan) {x : B} {h : c ⟶ x} {u : x ⟶ c} (adj : CategoryTheory.Bicategory.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.

instance CategoryTheory.Bicategory.LeftExtension.instCommuteWithOfIsLeftAdjoint {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} {h : c ⟶ x} [CategoryTheory.Bicategory.IsLeftAdjoint h] [CategoryTheory.Bicategory.HasLeftKanExtension f g] : CategoryTheory.Bicategory.Lan.CommuteWith f g h

Equations

• ⋯ = ⋯