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 HasLeftKanExtension f g (and similarly for lifts) 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} (desc : (s : LeftExtension f g) → t ⟶ s) (w : ∀ (s : 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} (H : t.IsKan) (s : 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} (H : t.IsKan) (s : LeftExtension f g) : CategoryStruct.comp t.unit (whiskerLeft f (H.desc s)) = s.unit

@[simp]

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

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.hom_ext {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} (H : t.IsKan) {k : b ⟶ c} {τ τ' : t.extension ⟶ k} (w : CategoryStruct.comp t.unit (whiskerLeft f τ) = CategoryStruct.comp t.unit (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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (P : s.IsKan) (Q : t.IsKan) : StructuredArrow.Hom.right (P.uniqueUpToIso Q).hom = P.desc t

@[simp]

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

def CategoryTheory.Bicategory.LeftExtension.IsKan.ofIsoKan {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f (CategoryStruct.comp g (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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (s t : 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)

noncomputable def CategoryTheory.Bicategory.LeftExtension.IsKan.ofIso {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} {f' : a ⟶ b} {g' : a ⟶ c} (H : t.IsKan) (ef : f ≅ f') (eg : g ≅ g') : (LeftExtension.ofIso ef eg t).IsKan

LeftExtension.ofIso preserves Kan extensions.

Equations

• H.ofIso ef eg = CategoryTheory.Limits.IsInitial.isInitialObj (CategoryTheory.Bicategory.LeftExtension.mapIso ef eg).functor t H

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftExtension.IsAbsKan.desc {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} (H : t.IsAbsKan) {x : B} {h : c ⟶ x} (s : LeftExtension f (CategoryStruct.comp g h)) : 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : 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} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : 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)

noncomputable def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofIso {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} {f' : a ⟶ b} {g' : a ⟶ c} (H : t.IsAbsKan) (ef : f ≅ f') (eg : g ≅ g') : (LeftExtension.ofIso ef eg t).IsAbsKan

LeftExtension.ofIso preserves absolute left Kan extensions.

Equations

• H.ofIso ef eg h = ((H h).ofIso ef (CategoryTheory.Bicategory.whiskerRightIso eg h)).ofIsoKan (CategoryTheory.Bicategory.LeftExtension.whiskerOfIso ef eg t h)

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftExtension.IsKan.unpaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} (Ht : t.IsKan) (u : LeftExtension (CategoryStruct.comp f h) g) : LeftExtension h t.extension

Given a left Kan extension t of g along f, a left extension u of g along f ≫ h induces, via the universal property of t, a left extension of t.extension along h.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.unpaste_extension {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} (Ht : t.IsKan) (u : LeftExtension (CategoryStruct.comp f h) g) : (Ht.unpaste u).extension = u.extension

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.unpaste_fac {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} (Ht : t.IsKan) (u : LeftExtension (CategoryStruct.comp f h) g) : CategoryStruct.comp t.unit (whiskerLeft f (Ht.unpaste u).unit) = CategoryStruct.comp u.unit (associator f h u.extension).hom

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.unpaste_fac_assoc {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} (Ht : t.IsKan) (u : LeftExtension (CategoryStruct.comp f h) g) {Z : a ⟶ c} (h✝ : CategoryStruct.comp f (CategoryStruct.comp h (Ht.unpaste u).extension) ⟶ Z) : CategoryStruct.comp t.unit (CategoryStruct.comp (whiskerLeft f (Ht.unpaste u).unit) h✝) = CategoryStruct.comp u.unit (CategoryStruct.comp (associator f h u.extension).hom h✝)

def CategoryTheory.Bicategory.LeftExtension.IsKan.paste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} {s : LeftExtension h t.extension} (Ht : t.IsKan) (Hs : s.IsKan) : (t.paste s).IsKan

Pasting of left extensions preserves being Kan.

Equations

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

def CategoryTheory.Bicategory.LeftExtension.IsKan.ofPaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} {s : LeftExtension h t.extension} (Ht : t.IsKan) (Hp : (t.paste s).IsKan) : s.IsKan

Given a left extension t of g along f and a left extension s of t along h, if t and t.paste s are Kan, then so is s.

Equations

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

def CategoryTheory.Bicategory.LeftExtension.isKanEquivIsKanPaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} {s : LeftExtension h t.extension} (Ht : t.IsKan) : s.IsKan ≃ (t.paste s).IsKan

Let t be a left Kan extension of g along f and s a left extension of t along h. Then s is Kan if and only if t.paste s is Kan.

Equations

• CategoryTheory.Bicategory.LeftExtension.isKanEquivIsKanPaste Ht = equivOfSubsingletonOfSubsingleton Ht.paste Ht.ofPaste

noncomputable def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.paste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} {s : LeftExtension h t.extension} (H : t.IsAbsKan) (Hs : s.IsAbsKan) : (t.paste s).IsAbsKan

Pasting of left extensions preserves being absolute Kan.

Equations

• H.paste Hs k = ((H k).paste (Hs k)).ofIsoKan (t.pasteWhiskerIso s k).symm

noncomputable def CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofPaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} {s : LeftExtension h t.extension} (H : t.IsAbsKan) (Hp : (t.paste s).IsAbsKan) : s.IsAbsKan

Given a left extension t of g along f and a left extension s of t along h, if t and t.paste s are absolute Kan, then so is s.

Equations

• H.ofPaste Hp k = (H k).ofPaste ((Hp k).ofIsoKan (t.pasteWhiskerIso s k))

noncomputable def CategoryTheory.Bicategory.LeftExtension.isAbsKanEquivIsAbsKanPaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : LeftExtension f g} {s : LeftExtension h t.extension} (H : t.IsAbsKan) : s.IsAbsKan ≃ (t.paste s).IsAbsKan

Let t be an absolute left Kan extension of g along f and s a left extension of t along h. Then s is absolute Kan if and only if t.paste s is absolute Kan.

Equations

• CategoryTheory.Bicategory.LeftExtension.isAbsKanEquivIsAbsKanPaste H = equivOfSubsingletonOfSubsingleton H.paste H.ofPaste

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.IsKan {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : 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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : 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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} (desc : (s : LeftLift f g) → t ⟶ s) (w : ∀ (s : 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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} (H : t.IsKan) (s : 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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} (H : t.IsKan) (s : LeftLift f g) : CategoryStruct.comp t.unit (whiskerRight (H.desc s) f) = s.unit

@[simp]

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

theorem CategoryTheory.Bicategory.LeftLift.IsKan.hom_ext {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} (H : t.IsKan) {k : c ⟶ b} {τ τ' : t.lift ⟶ k} (w : CategoryStruct.comp t.unit (whiskerRight τ f) = CategoryStruct.comp t.unit (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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : 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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (P : s.IsKan) (Q : t.IsKan) : StructuredArrow.Hom.right (P.uniqueUpToIso Q).hom = P.desc t

@[simp]

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

def CategoryTheory.Bicategory.LeftLift.IsKan.ofIsoKan {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : 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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f (CategoryStruct.comp (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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (s t : 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)

noncomputable def CategoryTheory.Bicategory.LeftLift.IsKan.ofIso {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} {f' : b ⟶ a} {g' : c ⟶ a} (H : t.IsKan) (ef : f ≅ f') (eg : g ≅ g') : (LeftLift.ofIso ef eg t).IsKan

LeftLift.ofIso preserves Kan lifts.

Equations

• H.ofIso ef eg = CategoryTheory.Limits.IsInitial.isInitialObj (CategoryTheory.Bicategory.LeftLift.mapIso ef eg).functor t H

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.IsAbsKan.desc {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} (H : t.IsAbsKan) {x : B} {h : x ⟶ c} (s : LeftLift f (CategoryStruct.comp h g)) : 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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : 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} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : 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)

noncomputable def CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofIso {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} {f' : b ⟶ a} {g' : c ⟶ a} (H : t.IsAbsKan) (ef : f ≅ f') (eg : g ≅ g') : (LeftLift.ofIso ef eg t).IsAbsKan

LeftLift.ofIso preserves absolute left Kan lifts.

Equations

• H.ofIso ef eg h = ((H h).ofIso ef (CategoryTheory.Bicategory.whiskerLeftIso h eg)).ofIsoKan (CategoryTheory.Bicategory.LeftLift.whiskerOfIso ef eg t h)

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftLift.IsKan.unpaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} (Ht : t.IsKan) (u : LeftLift (CategoryStruct.comp h f) g) : LeftLift h t.lift

Given a left Kan lift t of g along f, a left lift u of g along h ≫ f induces, via the universal property of t, a left lift of t.lift along h.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.IsKan.unpaste_lift {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} (Ht : t.IsKan) (u : LeftLift (CategoryStruct.comp h f) g) : (Ht.unpaste u).lift = u.lift

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.IsKan.unpaste_fac {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} (Ht : t.IsKan) (u : LeftLift (CategoryStruct.comp h f) g) : CategoryStruct.comp t.unit (whiskerRight (Ht.unpaste u).unit f) = CategoryStruct.comp u.unit (associator u.lift h f).inv

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.IsKan.unpaste_fac_assoc {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} (Ht : t.IsKan) (u : LeftLift (CategoryStruct.comp h f) g) {Z : d ⟶ a} (h✝ : CategoryStruct.comp (CategoryStruct.comp (Ht.unpaste u).lift h) f ⟶ Z) : CategoryStruct.comp t.unit (CategoryStruct.comp (whiskerRight (Ht.unpaste u).unit f) h✝) = CategoryStruct.comp u.unit (CategoryStruct.comp (associator u.lift h f).inv h✝)

def CategoryTheory.Bicategory.LeftLift.IsKan.paste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} {s : LeftLift h t.lift} (Ht : t.IsKan) (Hs : s.IsKan) : (t.paste s).IsKan

Pasting of left lifts preserves being Kan.

Equations

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

def CategoryTheory.Bicategory.LeftLift.IsKan.ofPaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} {s : LeftLift h t.lift} (Ht : t.IsKan) (Hp : (t.paste s).IsKan) : s.IsKan

Given a left lift t of g along f and a left lift s of t along h, if t and t.paste s are Kan, then so is s.

Equations

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

def CategoryTheory.Bicategory.LeftLift.isKanEquivIsKanPaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} {s : LeftLift h t.lift} (Ht : t.IsKan) : s.IsKan ≃ (t.paste s).IsKan

Let t be a left Kan lift of g along f and s a left lift of t along h. Then s is Kan if and only if t.paste s is Kan.

Equations

• CategoryTheory.Bicategory.LeftLift.isKanEquivIsKanPaste Ht = equivOfSubsingletonOfSubsingleton Ht.paste Ht.ofPaste

noncomputable def CategoryTheory.Bicategory.LeftLift.IsAbsKan.paste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} {s : LeftLift h t.lift} (H : t.IsAbsKan) (Hs : s.IsAbsKan) : (t.paste s).IsAbsKan

Pasting of left lifts preserves being absolute Kan.

Equations

• H.paste Hs k = ((H k).paste (Hs k)).ofIsoKan (t.pasteWhiskerIso s k).symm

noncomputable def CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofPaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} {s : LeftLift h t.lift} (H : t.IsAbsKan) (Hp : (t.paste s).IsAbsKan) : s.IsAbsKan

Given a left lift t of g along f and a left lift s of t along h, if t and t.paste s are absolute Kan, then so is s.

Equations

• H.ofPaste Hp k = (H k).ofPaste ((Hp k).ofIsoKan (t.pasteWhiskerIso s k))

noncomputable def CategoryTheory.Bicategory.LeftLift.isAbsKanEquivIsAbsKanPaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : LeftLift f g} {s : LeftLift h t.lift} (H : t.IsAbsKan) : s.IsAbsKan ≃ (t.paste s).IsAbsKan

Let t be an absolute left Kan lift of g along f and s a left lift of t along h. Then s is absolute Kan if and only if t.paste s is absolute Kan.

Equations

• CategoryTheory.Bicategory.LeftLift.isAbsKanEquivIsAbsKanPaste H = equivOfSubsingletonOfSubsingleton H.paste H.ofPaste

@[reducible, inline]

abbrev CategoryTheory.Bicategory.RightExtension.IsKan {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : 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.RightExtension.IsAbsKan {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f g) : Type (max (max u v) w)

An absolute right 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.RightExtension.IsKan.mk {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : RightExtension f g} (desc : (s : RightExtension f g) → s ⟶ t) (w : ∀ (s : RightExtension f g) (τ : s ⟶ t), τ = desc s) : t.IsKan

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

Equations

• CategoryTheory.Bicategory.RightExtension.IsKan.mk desc w = CategoryTheory.Limits.IsTerminal.ofUniqueHom desc w

@[reducible, inline]

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

The family of 2-morphisms into a right Kan extension.

Equations

• H.desc s = CategoryTheory.CostructuredArrow.IsUniversal.lift H s

@[simp]

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

@[simp]

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

theorem CategoryTheory.Bicategory.RightExtension.IsKan.hom_ext {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : RightExtension f g} (H : t.IsKan) {k : b ⟶ c} {τ τ' : k ⟶ t.extension} (w : CategoryStruct.comp (whiskerLeft f τ) t.counit = CategoryStruct.comp (whiskerLeft f τ') t.counit) : τ = τ'

Two 2-morphisms into a right Kan extension are equal if their compositions with each triangle 2-morphism are equal.

def CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIso {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension 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.IsTerminal.uniqueUpToIso P Q

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIso_hom_left {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (P : s.IsKan) (Q : t.IsKan) : CostructuredArrow.Hom.left (P.uniqueUpToIso Q).hom = Q.desc s

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIso_inv_left {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (P : s.IsKan) (Q : t.IsKan) : CostructuredArrow.Hom.left (P.uniqueUpToIso Q).inv = P.desc t

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

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

Equations

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

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

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

Equations

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

def CategoryTheory.Bicategory.RightExtension.IsKan.whiskerOfCommute {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (s t : RightExtension 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.RightExtension.IsKan.whiskerOfCommute s t i h P = P.ofIsoKan (CategoryTheory.Bicategory.RightExtension.whiskerIso i h)

noncomputable def CategoryTheory.Bicategory.RightExtension.IsKan.ofIso {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : RightExtension f g} {f' : a ⟶ b} {g' : a ⟶ c} (H : t.IsKan) (ef : f ≅ f') (eg : g ≅ g') : (RightExtension.ofIso ef eg t).IsKan

RightExtension.ofIso preserves Kan extensions.

Equations

• H.ofIso ef eg = CategoryTheory.Limits.IsTerminal.isTerminalObj (CategoryTheory.Bicategory.RightExtension.mapIso ef eg).functor t H

@[reducible, inline]

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

The family of 2-morphisms into an absolute right Kan extension.

Equations

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

def CategoryTheory.Bicategory.RightExtension.IsAbsKan.isKan {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : RightExtension f g} (H : t.IsAbsKan) : t.IsKan

An absolute right Kan extension is a right Kan extension.

Equations

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

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

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

Equations

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

noncomputable def CategoryTheory.Bicategory.RightExtension.IsAbsKan.ofIso {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : RightExtension f g} {f' : a ⟶ b} {g' : a ⟶ c} (H : t.IsAbsKan) (ef : f ≅ f') (eg : g ≅ g') : (RightExtension.ofIso ef eg t).IsAbsKan

RightExtension.ofIso preserves absolute right Kan extensions.

Equations

• H.ofIso ef eg h = ((H h).ofIso ef (CategoryTheory.Bicategory.whiskerRightIso eg h)).ofIsoKan (CategoryTheory.Bicategory.RightExtension.whiskerOfIso ef eg t h)

@[implicit_reducible]

def CategoryTheory.Bicategory.RightExtension.IsKan.unpaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} (Ht : t.IsKan) (u : RightExtension (CategoryStruct.comp f h) g) : RightExtension h t.extension

Given a right Kan extension t of g along f, a right extension u of g along f ≫ h induces, via the universal property of t, a right extension of t.extension along h.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.IsKan.unpaste_extension {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} (Ht : t.IsKan) (u : RightExtension (CategoryStruct.comp f h) g) : (Ht.unpaste u).extension = u.extension

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.IsKan.unpaste_fac {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} (Ht : t.IsKan) (u : RightExtension (CategoryStruct.comp f h) g) : CategoryStruct.comp (whiskerLeft f (Ht.unpaste u).counit) t.counit = CategoryStruct.comp (associator f h u.extension).inv u.counit

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.IsKan.unpaste_fac_assoc {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} (Ht : t.IsKan) (u : RightExtension (CategoryStruct.comp f h) g) {Z : a ⟶ c} (h✝ : g ⟶ Z) : CategoryStruct.comp (whiskerLeft f (Ht.unpaste u).counit) (CategoryStruct.comp t.counit h✝) = CategoryStruct.comp (associator f h u.extension).inv (CategoryStruct.comp u.counit h✝)

def CategoryTheory.Bicategory.RightExtension.IsKan.paste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} {s : RightExtension h t.extension} (Ht : t.IsKan) (Hs : s.IsKan) : (t.paste s).IsKan

Pasting of right extensions preserves being Kan.

Equations

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

def CategoryTheory.Bicategory.RightExtension.IsKan.ofPaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} {s : RightExtension h t.extension} (Ht : t.IsKan) (Hp : (t.paste s).IsKan) : s.IsKan

Given a right extension t of g along f and a right extension s of t along h, if t and t.paste s are Kan, then so is s.

Equations

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

def CategoryTheory.Bicategory.RightExtension.isKanEquivIsKanPaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} {s : RightExtension h t.extension} (Ht : t.IsKan) : s.IsKan ≃ (t.paste s).IsKan

Let t be a right Kan extension of g along f and s a right extension of t along h. Then s is Kan if and only if t.paste s is Kan.

Equations

• CategoryTheory.Bicategory.RightExtension.isKanEquivIsKanPaste Ht = equivOfSubsingletonOfSubsingleton Ht.paste Ht.ofPaste

noncomputable def CategoryTheory.Bicategory.RightExtension.IsAbsKan.paste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} {s : RightExtension h t.extension} (H : t.IsAbsKan) (Hs : s.IsAbsKan) : (t.paste s).IsAbsKan

Pasting of right extensions preserves being absolute Kan.

Equations

• H.paste Hs k = ((H k).paste (Hs k)).ofIsoKan (t.pasteWhiskerIso s k).symm

noncomputable def CategoryTheory.Bicategory.RightExtension.IsAbsKan.ofPaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} {s : RightExtension h t.extension} (H : t.IsAbsKan) (Hp : (t.paste s).IsAbsKan) : s.IsAbsKan

Given a right extension t of g along f and a right extension s of t along h, if t and t.paste s are absolute Kan, then so is s.

Equations

• H.ofPaste Hp k = (H k).ofPaste ((Hp k).ofIsoKan (t.pasteWhiskerIso s k))

noncomputable def CategoryTheory.Bicategory.RightExtension.isAbsKanEquivIsAbsKanPaste {B : Type u} [Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h : b ⟶ d} {t : RightExtension f g} {s : RightExtension h t.extension} (H : t.IsAbsKan) : s.IsAbsKan ≃ (t.paste s).IsAbsKan

Let t be an absolute right Kan extension of g along f and s a right extension of t along h. Then s is absolute Kan if and only if t.paste s is absolute Kan.

Equations

• CategoryTheory.Bicategory.RightExtension.isAbsKanEquivIsAbsKanPaste H = equivOfSubsingletonOfSubsingleton H.paste H.ofPaste

@[reducible, inline]

abbrev CategoryTheory.Bicategory.RightLift.IsKan {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : 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

@[reducible, inline]

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

An absolute right 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.RightLift.IsKan.mk {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : RightLift f g} (desc : (s : RightLift f g) → s ⟶ t) (w : ∀ (s : RightLift f g) (τ : s ⟶ t), τ = desc s) : t.IsKan

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

Equations

• CategoryTheory.Bicategory.RightLift.IsKan.mk desc w = CategoryTheory.Limits.IsTerminal.ofUniqueHom desc w

@[reducible, inline]

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

The family of 2-morphisms into a right Kan lift.

Equations

• H.desc s = CategoryTheory.CostructuredArrow.IsUniversal.lift H s

@[simp]

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

@[simp]

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

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

Two 2-morphisms into a right Kan lift are equal if their compositions with each triangle 2-morphism are equal.

def CategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIso {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift 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.IsTerminal.uniqueUpToIso P Q

@[simp]

theorem CategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIso_hom_left {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (P : s.IsKan) (Q : t.IsKan) : CostructuredArrow.Hom.left (P.uniqueUpToIso Q).hom = Q.desc s

@[simp]

theorem CategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIso_inv_left {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (P : s.IsKan) (Q : t.IsKan) : CostructuredArrow.Hom.left (P.uniqueUpToIso Q).inv = P.desc t

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

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

Equations

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

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

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

Equations

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

def CategoryTheory.Bicategory.RightLift.IsKan.whiskerOfCommute {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (s t : RightLift 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.RightLift.IsKan.whiskerOfCommute s t i h P = P.ofIsoKan (CategoryTheory.Bicategory.RightLift.whiskerIso i h)

noncomputable def CategoryTheory.Bicategory.RightLift.IsKan.ofIso {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : RightLift f g} {f' : b ⟶ a} {g' : c ⟶ a} (H : t.IsKan) (ef : f ≅ f') (eg : g ≅ g') : (RightLift.ofIso ef eg t).IsKan

RightLift.ofIso preserves Kan lifts.

Equations

• H.ofIso ef eg = CategoryTheory.Limits.IsTerminal.isTerminalObj (CategoryTheory.Bicategory.RightLift.mapIso ef eg).functor t H

@[reducible, inline]

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

The family of 2-morphisms into an absolute right Kan lift.

Equations

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

def CategoryTheory.Bicategory.RightLift.IsAbsKan.isKan {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : RightLift f g} (H : t.IsAbsKan) : t.IsKan

An absolute right Kan lift is a right Kan lift.

Equations

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

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

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

Equations

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

noncomputable def CategoryTheory.Bicategory.RightLift.IsAbsKan.ofIso {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : RightLift f g} {f' : b ⟶ a} {g' : c ⟶ a} (H : t.IsAbsKan) (ef : f ≅ f') (eg : g ≅ g') : (RightLift.ofIso ef eg t).IsAbsKan

RightLift.ofIso preserves absolute right Kan lifts.

Equations

• H.ofIso ef eg h = ((H h).ofIso ef (CategoryTheory.Bicategory.whiskerLeftIso h eg)).ofIsoKan (CategoryTheory.Bicategory.RightLift.whiskerOfIso ef eg t h)

@[implicit_reducible]

def CategoryTheory.Bicategory.RightLift.IsKan.unpaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} (Ht : t.IsKan) (u : RightLift (CategoryStruct.comp h f) g) : RightLift h t.lift

Given a right Kan lift t of g along f, a right lift u of g along h ≫ f induces, via the universal property of t, a right lift of t.lift along h.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightLift.IsKan.unpaste_lift {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} (Ht : t.IsKan) (u : RightLift (CategoryStruct.comp h f) g) : (Ht.unpaste u).lift = u.lift

@[simp]

theorem CategoryTheory.Bicategory.RightLift.IsKan.unpaste_fac {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} (Ht : t.IsKan) (u : RightLift (CategoryStruct.comp h f) g) : CategoryStruct.comp (whiskerRight (Ht.unpaste u).counit f) t.counit = CategoryStruct.comp (associator u.lift h f).hom u.counit

@[simp]

theorem CategoryTheory.Bicategory.RightLift.IsKan.unpaste_fac_assoc {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} (Ht : t.IsKan) (u : RightLift (CategoryStruct.comp h f) g) {Z : d ⟶ a} (h✝ : g ⟶ Z) : CategoryStruct.comp (whiskerRight (Ht.unpaste u).counit f) (CategoryStruct.comp t.counit h✝) = CategoryStruct.comp (associator u.lift h f).hom (CategoryStruct.comp u.counit h✝)

def CategoryTheory.Bicategory.RightLift.IsKan.paste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} {s : RightLift h t.lift} (Ht : t.IsKan) (Hs : s.IsKan) : (t.paste s).IsKan

Pasting of right lifts preserves being Kan.

Equations

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

def CategoryTheory.Bicategory.RightLift.IsKan.ofPaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} {s : RightLift h t.lift} (Ht : t.IsKan) (Hp : (t.paste s).IsKan) : s.IsKan

Given a right lift t of g along f and a right lift s of t along h, if t and t.paste s are Kan, then so is s.

Equations

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

def CategoryTheory.Bicategory.RightLift.isKanEquivIsKanPaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} {s : RightLift h t.lift} (Ht : t.IsKan) : s.IsKan ≃ (t.paste s).IsKan

Let t be a right Kan lift of g along f and s a right lift of t along h. Then s is Kan if and only if t.paste s is Kan.

Equations

• CategoryTheory.Bicategory.RightLift.isKanEquivIsKanPaste Ht = equivOfSubsingletonOfSubsingleton Ht.paste Ht.ofPaste

noncomputable def CategoryTheory.Bicategory.RightLift.IsAbsKan.paste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} {s : RightLift h t.lift} (H : t.IsAbsKan) (Hs : s.IsAbsKan) : (t.paste s).IsAbsKan

Pasting of right lifts preserves being absolute Kan.

Equations

• H.paste Hs k = ((H k).paste (Hs k)).ofIsoKan (t.pasteWhiskerIso s k).symm

noncomputable def CategoryTheory.Bicategory.RightLift.IsAbsKan.ofPaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} {s : RightLift h t.lift} (H : t.IsAbsKan) (Hp : (t.paste s).IsAbsKan) : s.IsAbsKan

Given a right lift t of g along f and a right lift s of t along h, if t and t.paste s are absolute Kan, then so is s.

Equations

• H.ofPaste Hp k = (H k).ofPaste ((Hp k).ofIsoKan (t.pasteWhiskerIso s k))

noncomputable def CategoryTheory.Bicategory.RightLift.isAbsKanEquivIsAbsKanPaste {B : Type u} [Bicategory B] {a b c d : B} {f : b ⟶ a} {g : d ⟶ a} {h : c ⟶ b} {t : RightLift f g} {s : RightLift h t.lift} (H : t.IsAbsKan) : s.IsAbsKan ≃ (t.paste s).IsAbsKan

Let t be an absolute right Kan lift of g along f and s a right lift of t along h. Then s is absolute Kan if and only if t.paste s is absolute Kan.

Equations

• CategoryTheory.Bicategory.RightLift.isAbsKanEquivIsAbsKanPaste H = equivOfSubsingletonOfSubsingleton H.paste H.ofPaste