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. The universal property can be accessed by the following definition and lemmas:

• LeftExtension.IsKan.desc: the family of 2-morphisms out of the left Kan extension.
• LeftExtension.IsKan.fac: the unit of any left extension factors through the left Kan extension.
• LeftExtension.IsKan.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.

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

References

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

@[reducible, inline]

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

• t.IsKan = CategoryTheory.StructuredArrow.IsUniversal t

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftExtension.IsAbsKan {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 u v) w)

An absolute left Kan extension is a Kan extension that commutes with any 1-morphism.

Equations

• t.IsAbsKan = ({x : B} → (h : c ⟶ x) → (t.whisker h).IsKan)

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftExtension.IsKan.mk {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ c} {t : CategoryTheory.Bicategory.LeftExtension f g} (desc : (s : CategoryTheory.Bicategory.LeftExtension f g) → t ⟶ s) (w : ∀ (s : CategoryTheory.Bicategory.LeftExtension f g) (τ : t ⟶ s), τ = desc s) : t.IsKan

To show that a left extension t is a Kan extension, we need to show that for every left extension s there is a unique morphism t ⟶ s.

Equations

• CategoryTheory.Bicategory.LeftExtension.IsKan.mk desc w = CategoryTheory.Limits.IsInitial.ofUniqueHom desc w

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftExtension.IsKan.desc {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) (s : CategoryTheory.Bicategory.LeftExtension f g) : t.extension ⟶ s.extension

The family of 2-morphisms out of a left Kan extension.

Equations

• H.desc s = CategoryTheory.StructuredArrow.IsUniversal.desc H s

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.fac_assoc {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) (s : CategoryTheory.Bicategory.LeftExtension f g) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f s.extension ⟶ Z) : CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (H.desc s)) h) = CategoryTheory.CategoryStruct.comp s.unit h

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.fac {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) (s : CategoryTheory.Bicategory.LeftExtension f g) : CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f (H.desc s)) = s.unit

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.hom_ext {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) {k : b ⟶ c} {τ : t.extension ⟶ k} {τ' : t.extension ⟶ k} (w : CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f τ) = CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f τ')) : τ = τ'

Two 2-morphisms out of a left Kan extension are equal if their compositions with each triangle 2-morphism are equal.

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftExtension.IsAbsKan.desc {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.IsAbsKan) {x : B} {h : c ⟶ x} (s : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g h)) : CategoryTheory.CategoryStruct.comp t.extension h ⟶ s.extension

The family of 2-morphisms out of an absolute left Kan extension.

Equations

• H.desc s = (H h).desc s

def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.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} (H : t.IsAbsKan) : t.IsKan

An absolute left Kan extension is a left Kan extension.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

• t.IsKan = CategoryTheory.StructuredArrow.IsUniversal t

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.IsAbsKan {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 u v) w)

An absolute left Kan lift is a Kan lift such that every 1-morphism commutes with it.

Equations

• t.IsAbsKan = ({x : B} → (h : x ⟶ c) → (t.whisker h).IsKan)

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.IsKan.mk {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} {t : CategoryTheory.Bicategory.LeftLift f g} (desc : (s : CategoryTheory.Bicategory.LeftLift f g) → t ⟶ s) (w : ∀ (s : CategoryTheory.Bicategory.LeftLift f g) (τ : t ⟶ s), τ = desc s) : t.IsKan

To show that a left lift t is a Kan lift, we need to show that for every left lift s there is a unique morphism t ⟶ s.

Equations

• CategoryTheory.Bicategory.LeftLift.IsKan.mk desc w = CategoryTheory.Limits.IsInitial.ofUniqueHom desc w

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.IsKan.desc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.LeftLift f g) : t.lift ⟶ s.lift

The family of 2-morphisms out of a left Kan lift.

Equations

• H.desc s = CategoryTheory.StructuredArrow.IsUniversal.desc H s

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.IsKan.fac_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.LeftLift f g) {Z : c ⟶ a} (h : CategoryTheory.CategoryStruct.comp s.lift f ⟶ Z) : CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (H.desc s) f) h) = CategoryTheory.CategoryStruct.comp s.unit h

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.IsKan.fac {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.LeftLift f g) : CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight (H.desc s) f) = s.unit

theorem CategoryTheory.Bicategory.LeftLift.IsKan.hom_ext {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan) {k : c ⟶ b} {τ : t.lift ⟶ k} {τ' : t.lift ⟶ k} (w : CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight τ f) = CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight τ' f)) : τ = τ'

Two 2-morphisms out of a left Kan lift are equal if their compositions with each triangle 2-morphism are equal.

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.IsAbsKan.desc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsAbsKan) {x : B} {h : x ⟶ c} (s : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp h g)) : CategoryTheory.CategoryStruct.comp h t.lift ⟶ s.lift

The family of 2-morphisms out of an absolute left Kan lift.

Equations

• H.desc s = (H h).desc s

def CategoryTheory.Bicategory.LeftLift.IsAbsKan.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} (H : t.IsAbsKan) : t.IsKan

An absolute left Kan lift is a left Kan lift.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

• t.IsKan = CategoryTheory.CostructuredArrow.IsUniversal t

@[reducible, inline]

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

• t.IsKan = CategoryTheory.CostructuredArrow.IsUniversal t