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 defined in CategoryTheory.Bicategory.Kan.HasKan 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 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 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 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 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 {B : Type u} [CategoryTheory.Bicategory B] {a 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

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.fac_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.hom_ext {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : CategoryTheory.Bicategory.LeftExtension f g} (H : t.IsKan) {k : b ⟶ c} {τ τ' : 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.

def CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : CategoryTheory.Bicategory.LeftExtension f g} (P : s.IsKan) (Q : t.IsKan) : s ≅ t

Kan extensions on g along f are unique up to isomorphism.

Equations

• P.uniqueUpToIso Q = CategoryTheory.Limits.IsInitial.uniqueUpToIso P Q

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso_hom_right {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : CategoryTheory.Bicategory.LeftExtension f g} (P : s.IsKan) (Q : t.IsKan) : (P.uniqueUpToIso Q).hom.right = P.desc t

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso_inv_right {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : CategoryTheory.Bicategory.LeftExtension f g} (P : s.IsKan) (Q : t.IsKan) : (P.uniqueUpToIso Q).inv.right = Q.desc s

def CategoryTheory.Bicategory.LeftExtension.IsKan.ofIsoKan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : CategoryTheory.Bicategory.LeftExtension f g} (P : s.IsKan) (i : s ≅ t) : t.IsKan

Transport evidence that a left extension is a Kan extension across an isomorphism of extensions.

Equations

• P.ofIsoKan i = CategoryTheory.Limits.IsInitial.ofIso P i

def CategoryTheory.Bicategory.LeftExtension.IsKan.ofCompId {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))) (P : t.IsKan) : t.ofCompId.IsKan

If t : LeftExtension f (g ≫ 𝟙 c) is a Kan extension, then t.ofCompId : LeftExtension f g is also a Kan extension.

Equations

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

def CategoryTheory.Bicategory.LeftExtension.IsKan.whiskerOfCommute {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (s t : CategoryTheory.Bicategory.LeftExtension f g) (i : s ≅ t) {x : B} (h : c ⟶ x) (P : (s.whisker h).IsKan) : (t.whisker h).IsKan

If s ≅ t and IsKan (s.whisker h), then IsKan (t.whisker h).

Equations

• CategoryTheory.Bicategory.LeftExtension.IsKan.whiskerOfCommute s t i h P = P.ofIsoKan (CategoryTheory.Bicategory.LeftExtension.whiskerIso i h)

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftExtension.IsAbsKan.desc {B : Type u} [CategoryTheory.Bicategory B] {a 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 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.

def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofIsoAbsKan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : CategoryTheory.Bicategory.LeftExtension f g} (P : s.IsAbsKan) (i : s ≅ t) : t.IsAbsKan

Transport evidence that a left extension is a Kan extension across an isomorphism of extensions.

Equations

• P.ofIsoAbsKan i h = (P h).ofIsoKan (CategoryTheory.Bicategory.LeftExtension.whiskerIso i h)

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.IsKan {B : Type u} [CategoryTheory.Bicategory B] {a 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 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 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 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 {B : Type u} [CategoryTheory.Bicategory B] {a 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

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.IsKan.fac_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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

theorem CategoryTheory.Bicategory.LeftLift.IsKan.hom_ext {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan) {k : c ⟶ b} {τ τ' : 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.

def CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : CategoryTheory.Bicategory.LeftLift f g} (P : s.IsKan) (Q : t.IsKan) : s ≅ t

Kan lifts on g along f are unique up to isomorphism.

Equations

• P.uniqueUpToIso Q = CategoryTheory.Limits.IsInitial.uniqueUpToIso P Q

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso_hom_right {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : CategoryTheory.Bicategory.LeftLift f g} (P : s.IsKan) (Q : t.IsKan) : (P.uniqueUpToIso Q).hom.right = P.desc t

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso_inv_right {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : CategoryTheory.Bicategory.LeftLift f g} (P : s.IsKan) (Q : t.IsKan) : (P.uniqueUpToIso Q).inv.right = Q.desc s

def CategoryTheory.Bicategory.LeftLift.IsKan.ofIsoKan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : CategoryTheory.Bicategory.LeftLift f g} (P : s.IsKan) (i : s ≅ t) : t.IsKan

Transport evidence that a left lift is a Kan lift across an isomorphism of lifts.

Equations

• P.ofIsoKan i = CategoryTheory.Limits.IsInitial.ofIso P i

def CategoryTheory.Bicategory.LeftLift.IsKan.ofIdComp {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)) (P : t.IsKan) : t.ofIdComp.IsKan

If t : LeftLift f (𝟙 c ≫ g) is a Kan lift, then t.ofIdComp : LeftLift f g is also a Kan lift.

Equations

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

def CategoryTheory.Bicategory.LeftLift.IsKan.whiskerOfCommute {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (s t : CategoryTheory.Bicategory.LeftLift f g) (i : s ≅ t) {x : B} (h : x ⟶ c) (P : (s.whisker h).IsKan) : (t.whisker h).IsKan

If s ≅ t and IsKan (s.whisker h), then IsKan (t.whisker h).

Equations

• CategoryTheory.Bicategory.LeftLift.IsKan.whiskerOfCommute s t i h P = P.ofIsoKan (CategoryTheory.Bicategory.LeftLift.whiskerIso i h)

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.IsAbsKan.desc {B : Type u} [CategoryTheory.Bicategory B] {a 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 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

• H.isKan = (CategoryTheory.Bicategory.LeftLift.IsKan.ofIdComp (t.whisker (CategoryTheory.CategoryStruct.id c)) (H (CategoryTheory.CategoryStruct.id c))).ofIsoKan t.whiskerOfIdCompIsoSelf

def CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofIsoAbsKan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : CategoryTheory.Bicategory.LeftLift f g} (P : s.IsAbsKan) (i : s ≅ t) : t.IsAbsKan

Transport evidence that a left lift is a Kan lift across an isomorphism of lifts.

Equations

• P.ofIsoAbsKan i h = (P h).ofIsoKan (CategoryTheory.Bicategory.LeftLift.whiskerIso i h)

@[reducible, inline]

abbrev CategoryTheory.Bicategory.RightExtension.IsKan {B : Type u} [CategoryTheory.Bicategory B] {a 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 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