Kan extensions and Kan lifts in bicategories

The left Kan extension of a 1-morphism g : a ⟶ c along a 1-morphism f : a ⟶ b is the initial object in the category of left extensions LeftExtension f g.

We define LeftExtension.IsKan t for an extension t : LeftExtension f g (which is an abbreviation of t : StructuredArrow g (precomp _ f)) to be StructuredArrow.IsUniversal t. This means that we can use the following definition and lemmas for h : LeftExtension.IsKan t living in the namespace StructuredArrow.IsUniversal:

• h.desc: the family of 2-morphisms out of the left Kan extension.
• h.fac: the unit of any left extension factors through the left Kan extension.
• h.hom_ext: two 2-morphisms out of the left Kan extension are equal if their compositions with each unit are equal.

We also define left Kan lifts, right Kan extensions, and right Kan lifts.

Implementation Notes

We use the Is-Has design pattern, which is used for the implementation of limits and colimits in the category theory library. This means that IsKan t is a structure containing the data of 2-morphisms which ensure that t is a Kan extension, while HasKan f g (to be implemented in the near future) is a Prop-valued typeclass asserting that a Kan extension of g along f exists.

References

https://ncatlab.org/nlab/show/Kan+extension

@[inline, reducible]

abbrev CategoryTheory.Bicategory.LeftExtension.IsKan {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ c} (t : CategoryTheory.Bicategory.LeftExtension f g) : Type (max (max v w) w)

A left Kan extension of g along f is an initial object in LeftExtension f g.

Equations

• CategoryTheory.Bicategory.LeftExtension.IsKan t = CategoryTheory.StructuredArrow.IsUniversal t

@[inline, reducible]

abbrev CategoryTheory.Bicategory.LeftLift.IsKan {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} (t : CategoryTheory.Bicategory.LeftLift f g) : Type (max (max v w) w)

A left Kan lift of g along f is an initial object in LeftLift f g.

Equations

• CategoryTheory.Bicategory.LeftLift.IsKan t = CategoryTheory.StructuredArrow.IsUniversal t

@[inline, reducible]

abbrev CategoryTheory.Bicategory.RightExtension.IsKan {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ c} (t : CategoryTheory.Bicategory.RightExtension f g) : Type (max (max v w) w)

A right Kan extension of g along f is a terminal object in RightExtension f g.

Equations

• CategoryTheory.Bicategory.RightExtension.IsKan t = CategoryTheory.CostructuredArrow.IsUniversal t

@[inline, reducible]

abbrev CategoryTheory.Bicategory.RightLift.IsKan {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} (t : CategoryTheory.Bicategory.RightLift f g) : Type (max (max v w) w)

A right Kan lift of g along f is a terminal object in RightLift f g.

Equations

• CategoryTheory.Bicategory.RightLift.IsKan t = CategoryTheory.CostructuredArrow.IsUniversal t