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}
{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
Instances For
@[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.
Instances For
@[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
Instances For
@[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
Instances For
@[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.
def
CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
{s : CategoryTheory.Bicategory.LeftExtension f g}
{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
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso_hom_right
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
{s : CategoryTheory.Bicategory.LeftExtension f g}
{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}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
{s : CategoryTheory.Bicategory.LeftExtension f g}
{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}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
{s : CategoryTheory.Bicategory.LeftExtension f g}
{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
Instances For
def
CategoryTheory.Bicategory.LeftExtension.IsKan.ofCompId
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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.
Instances For
def
CategoryTheory.Bicategory.LeftExtension.IsKan.whiskerOfCommute
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
(s : CategoryTheory.Bicategory.LeftExtension f g)
(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)
Instances For
@[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
Instances For
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.
Instances For
def
CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofIsoAbsKan
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
{s : CategoryTheory.Bicategory.LeftExtension f g}
{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)
Instances For
@[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
Instances For
@[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.
Instances For
@[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
Instances For
@[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
Instances For
@[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.
def
CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
{s : CategoryTheory.Bicategory.LeftLift f g}
{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
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso_hom_right
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
{s : CategoryTheory.Bicategory.LeftLift f g}
{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}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
{s : CategoryTheory.Bicategory.LeftLift f g}
{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}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
{s : CategoryTheory.Bicategory.LeftLift f g}
{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
Instances For
def
CategoryTheory.Bicategory.LeftLift.IsKan.ofIdComp
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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.
Instances For
def
CategoryTheory.Bicategory.LeftLift.IsKan.whiskerOfCommute
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
(s : CategoryTheory.Bicategory.LeftLift f g)
(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)
Instances For
@[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
Instances For
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
- H.isKan = (CategoryTheory.Bicategory.LeftLift.IsKan.ofIdComp (t.whisker (CategoryTheory.CategoryStruct.id c)) (H (CategoryTheory.CategoryStruct.id c))).ofIsoKan t.whiskerOfIdCompIsoSelf
Instances For
def
CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofIsoAbsKan
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
{s : CategoryTheory.Bicategory.LeftLift f g}
{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)
Instances For
@[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
Instances For
@[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.