Existence of Kan extensions and Kan lifts in bicategories

We provide the propositional typeclass HasLeftKanExtension f g, which asserts that there exists a left Kan extension of g along f. See CategoryTheory.Bicategory.Kan.IsKan for the definition of left Kan extensions. Under the assumption that HasLeftKanExtension f g, we define the left Kan extension lan f g by using the axiom of choice.

Main definitions

• lan f g is the left Kan extension of g along f, and is denoted by f⁺ g.
• lanLift f g is the left Kan lift of g along f, and is denoted by f₊ g.

These notations are inspired by [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006].

TODO

• ran f g is the right Kan extension of g along f, and is denoted by f⁺⁺ g.
• ranLift f g is the right Kan lift of g along f, and is denoted by f₊₊ g.

class CategoryTheory.Bicategory.HasLeftKanExtension {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) : Prop

The existence of a left Kan extension of g along f.

• hasInitial : CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftExtension f g)

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension {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) : CategoryTheory.Bicategory.HasLeftKanExtension f g

instance CategoryTheory.Bicategory.instHasInitialLeftExtensionOfHasLeftKanExtension {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] : CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftExtension f g)

Equations

• ⋯ = ⋯

def CategoryTheory.Bicategory.lanLeftExtension {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] : CategoryTheory.Bicategory.LeftExtension f g

The left Kan extension of g along f at the level of structured arrows.

Equations

• CategoryTheory.Bicategory.lanLeftExtension f g = ⊥_ CategoryTheory.Bicategory.LeftExtension f g

def CategoryTheory.Bicategory.lan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] : b ⟶ c

The left Kan extension of g along f.

Equations

• CategoryTheory.Bicategory.lan f g = (CategoryTheory.Bicategory.lanLeftExtension f g).extension

def CategoryTheory.Bicategory.«term_⁺_» : Lean.TrailingParserDescr

f⁺ g is the left Kan extension of g along f.

  b
  △ \
  |   \ f⁺ g
f |     \
  |       ◿
  a - - - ▷ c
      g

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.lanLeftExtension_extension {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] : (CategoryTheory.Bicategory.lanLeftExtension f g).extension = CategoryTheory.Bicategory.lan f g

def CategoryTheory.Bicategory.lanUnit {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] : g ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Bicategory.lan f g)

The unit for the left Kan extension f⁺ g.

Equations

• CategoryTheory.Bicategory.lanUnit f g = (CategoryTheory.Bicategory.lanLeftExtension f g).unit

@[simp]

theorem CategoryTheory.Bicategory.lanLeftExtension_unit {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] : (CategoryTheory.Bicategory.lanLeftExtension f g).unit = CategoryTheory.Bicategory.lanUnit f g

def CategoryTheory.Bicategory.lanIsKan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] : (CategoryTheory.Bicategory.lanLeftExtension f g).IsKan

Evidence that the Lan.extension f g is a Kan extension.

Equations

• CategoryTheory.Bicategory.lanIsKan f g = CategoryTheory.Limits.initialIsInitial

def CategoryTheory.Bicategory.lanDesc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g) : CategoryTheory.Bicategory.lan f g ⟶ s.extension

The family of 2-morphisms out of the left Kan extension f⁺ g.

Equations

• CategoryTheory.Bicategory.lanDesc s = (CategoryTheory.Bicategory.lanIsKan f g).desc s

@[simp]

theorem CategoryTheory.Bicategory.lanUnit_desc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.lanDesc s)) = s.unit

@[simp]

theorem CategoryTheory.Bicategory.lanUnit_desc_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f s.extension ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.lanDesc s)) h) = CategoryTheory.CategoryStruct.comp s.unit h

@[simp]

theorem CategoryTheory.Bicategory.lanIsKan_desc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g) : (CategoryTheory.Bicategory.lanIsKan f g).desc s = CategoryTheory.Bicategory.lanDesc s

theorem CategoryTheory.Bicategory.Lan.existsUnique {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g) : ∃! τ : CategoryTheory.Bicategory.lan f g ⟶ s.extension, CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g) (CategoryTheory.Bicategory.whiskerLeft f τ) = s.unit

class CategoryTheory.Bicategory.Lan.CommuteWith {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) : Prop

We say that a 1-morphism h commutes with the left Kan extension f⁺ g if the whiskered left extension for f⁺ g by h is a Kan extension of g ≫ h along f.

• commute : Nonempty ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h).IsKan

theorem CategoryTheory.Bicategory.Lan.CommuteWith.of_isKan_whisker {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] (t : CategoryTheory.Bicategory.LeftExtension f g) {x : B} (h : c ⟶ x) (H : (t.whisker h).IsKan) (i : t.whisker h ≅ (CategoryTheory.Bicategory.lanLeftExtension f g).whisker h) : CategoryTheory.Bicategory.Lan.CommuteWith f g h

theorem CategoryTheory.Bicategory.Lan.CommuteWith.of_lan_comp_iso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} {h : c ⟶ x} [CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.comp g h)] (i : CategoryTheory.Bicategory.lan f (CategoryTheory.CategoryStruct.comp g h) ≅ CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lan f g) h) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft f i.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.lanUnit f g) h) (CategoryTheory.Bicategory.associator f (CategoryTheory.Bicategory.lan f g) h).hom) : CategoryTheory.Bicategory.Lan.CommuteWith f g h

def CategoryTheory.Bicategory.Lan.CommuteWith.isKan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h).IsKan

Evidence that h commutes with the left Kan extension f⁺ g.

Equations

• CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h = Classical.choice ⋯

instance CategoryTheory.Bicategory.Lan.CommuteWith.instHasLeftKanExtensionComp {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.comp g h)

Equations

• ⋯ = ⋯

def CategoryTheory.Bicategory.Lan.CommuteWith.isKanWhisker {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] (t : CategoryTheory.Bicategory.LeftExtension f g) (H : t.IsKan) {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : (t.whisker h).IsKan

If h commutes with f⁺ g and t is another left Kan extension of g along f, then t.whisker h is a left Kan extension of g ≫ h along f.

Equations

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

def CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h) ≅ (CategoryTheory.Bicategory.lanLeftExtension f g).whisker h

The isomorphism f⁺ (g ≫ h) ≅ f⁺ g ≫ h at the level of structured arrows.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_hom_right {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker f g h).hom.right = CategoryTheory.Bicategory.lanDesc ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h)

@[simp]

theorem CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_inv_right {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker f g h).inv.right = (CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h))

def CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : CategoryTheory.Bicategory.lan f (CategoryTheory.CategoryStruct.comp g h) ≅ CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lan f g) h

The 1-morphism h commutes with the left Kan extension f⁺ g.

Equations

• CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h = CategoryTheory.Comma.rightIso (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker f g h)

@[simp]

theorem CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h).inv = (CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h))

@[simp]

theorem CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h).hom = CategoryTheory.Bicategory.lanDesc ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h)

class CategoryTheory.Bicategory.HasAbsLeftKanExtension {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) extends CategoryTheory.Bicategory.HasLeftKanExtension f g : Prop

We say that there exists an absolute left Kan extension of g along f if any 1-morphism h commutes with the left Kan extension f⁺ g.

• hasInitial : CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftExtension f g)
• commute : ∀ {x : B} (h : c ⟶ x), CategoryTheory.Bicategory.Lan.CommuteWith f g h

instance CategoryTheory.Bicategory.instCommuteWith {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasAbsLeftKanExtension f g] {x : B} (h : c ⟶ x) : CategoryTheory.Bicategory.Lan.CommuteWith f g h

Equations

• ⋯ = ⋯

theorem CategoryTheory.Bicategory.LeftExtension.IsAbsKan.hasAbsLeftKanExtension {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) : CategoryTheory.Bicategory.HasAbsLeftKanExtension f g

class CategoryTheory.Bicategory.HasLeftKanLift {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) : Prop

The existence of a left kan lift of g along f.

• mk' :: (
• hasInitial : CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftLift f g)
• )

theorem CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift {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) : CategoryTheory.Bicategory.HasLeftKanLift f g

instance CategoryTheory.Bicategory.instHasInitialLeftLiftOfHasLeftKanLift {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] : CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftLift f g)

Equations

• ⋯ = ⋯

def CategoryTheory.Bicategory.lanLiftLeftLift {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] : CategoryTheory.Bicategory.LeftLift f g

The left Kan lift of g along f at the level of structured arrows.

Equations

• CategoryTheory.Bicategory.lanLiftLeftLift f g = ⊥_ CategoryTheory.Bicategory.LeftLift f g

def CategoryTheory.Bicategory.lanLift {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] : c ⟶ b

The left Kan lift of g along f.

Equations

• CategoryTheory.Bicategory.lanLift f g = (CategoryTheory.Bicategory.lanLiftLeftLift f g).lift

def CategoryTheory.Bicategory.«term_₊_» : Lean.TrailingParserDescr

f₊ g is the left Kan lift of g along f.

            b
          ◹ |
   f₊ g /   |
      /     | f
    /       ▽
  c - - - ▷ a
       g

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.lanLiftLeftLift_lift {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] : (CategoryTheory.Bicategory.lanLiftLeftLift f g).lift = CategoryTheory.Bicategory.lanLift f g

def CategoryTheory.Bicategory.lanLiftUnit {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] : g ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLift f g) f

The unit for the left Kan lift f₊ g.

Equations

• CategoryTheory.Bicategory.lanLiftUnit f g = (CategoryTheory.Bicategory.lanLiftLeftLift f g).unit

@[simp]

theorem CategoryTheory.Bicategory.lanLiftLeftLift_unit {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] : (CategoryTheory.Bicategory.lanLiftLeftLift f g).unit = CategoryTheory.Bicategory.lanLiftUnit f g

def CategoryTheory.Bicategory.lanLiftIsKan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] : (CategoryTheory.Bicategory.lanLiftLeftLift f g).IsKan

Evidence that the LanLift.lift f g is a Kan lift.

Equations

• CategoryTheory.Bicategory.lanLiftIsKan f g = CategoryTheory.Limits.initialIsInitial

def CategoryTheory.Bicategory.lanLiftDesc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g) : CategoryTheory.Bicategory.lanLift f g ⟶ s.lift

The family of 2-morphisms out of the left Kan lift f₊ g.

Equations

• CategoryTheory.Bicategory.lanLiftDesc s = (CategoryTheory.Bicategory.lanLiftIsKan f g).desc s

@[simp]

theorem CategoryTheory.Bicategory.lanLiftUnit_desc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.lanLiftDesc s) f) = s.unit

@[simp]

theorem CategoryTheory.Bicategory.lanLiftUnit_desc_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g) {Z : c ⟶ a} (h : CategoryTheory.CategoryStruct.comp s.lift f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.lanLiftDesc s) f) h) = CategoryTheory.CategoryStruct.comp s.unit h

@[simp]

theorem CategoryTheory.Bicategory.lanLiftIsKan_desc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g) : (CategoryTheory.Bicategory.lanLiftIsKan f g).desc s = CategoryTheory.Bicategory.lanLiftDesc s

theorem CategoryTheory.Bicategory.LanLift.existsUnique {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g) : ∃! τ : CategoryTheory.Bicategory.lanLift f g ⟶ s.lift, CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g) (CategoryTheory.Bicategory.whiskerRight τ f) = s.unit

class CategoryTheory.Bicategory.LanLift.CommuteWith {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) : Prop

We say that a 1-morphism h commutes with the left Kan lift f₊ g if the whiskered left lift for f₊ g by h is a Kan lift of h ≫ g along f.

• commute : Nonempty ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h).IsKan

theorem CategoryTheory.Bicategory.LanLift.CommuteWith.of_isKan_whisker {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] (t : CategoryTheory.Bicategory.LeftLift f g) {x : B} (h : x ⟶ c) (H : (t.whisker h).IsKan) (i : t.whisker h ≅ (CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h) : CategoryTheory.Bicategory.LanLift.CommuteWith f g h

theorem CategoryTheory.Bicategory.LanLift.CommuteWith.of_lanLift_comp_iso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} {h : x ⟶ c} [CategoryTheory.Bicategory.HasLeftKanLift f (CategoryTheory.CategoryStruct.comp h g)] (i : CategoryTheory.Bicategory.lanLift f (CategoryTheory.CategoryStruct.comp h g) ≅ CategoryTheory.CategoryStruct.comp h (CategoryTheory.Bicategory.lanLift f g)) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f (CategoryTheory.CategoryStruct.comp h g)) (CategoryTheory.Bicategory.whiskerRight i.hom f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft h (CategoryTheory.Bicategory.lanLiftUnit f g)) (CategoryTheory.Bicategory.associator h (CategoryTheory.Bicategory.lanLift f g) f).inv) : CategoryTheory.Bicategory.LanLift.CommuteWith f g h

def CategoryTheory.Bicategory.LanLift.CommuteWith.isKan {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h).IsKan

Evidence that h commutes with the left Kan lift f₊ g.

Equations

• CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h = Classical.choice ⋯

instance CategoryTheory.Bicategory.LanLift.CommuteWith.instHasLeftKanLiftComp {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : CategoryTheory.Bicategory.HasLeftKanLift f (CategoryTheory.CategoryStruct.comp h g)

Equations

• ⋯ = ⋯

def CategoryTheory.Bicategory.LanLift.CommuteWith.isKanWhisker {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] (t : CategoryTheory.Bicategory.LeftLift f g) (H : t.IsKan) {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : (t.whisker h).IsKan

If h commutes with f₊ g and t is another left Kan lift of g along f, then t.whisker h is a left Kan lift of h ≫ g along f.

Equations

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

def CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g) ≅ (CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h

The isomorphism f₊ (h ≫ g) ≅ h ≫ f₊ g at the level of structured arrows.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker f g h).hom.right = CategoryTheory.Bicategory.lanLiftDesc ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h)

@[simp]

theorem CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker f g h).inv.right = (CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g))

def CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : CategoryTheory.Bicategory.lanLift f (CategoryTheory.CategoryStruct.comp h g) ≅ CategoryTheory.CategoryStruct.comp h (CategoryTheory.Bicategory.lanLift f g)

The 1-morphism h commutes with the left Kan lift f₊ g.

Equations

• CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h = CategoryTheory.Comma.rightIso (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker f g h)

@[simp]

theorem CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h).hom = CategoryTheory.Bicategory.lanLiftDesc ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h)

@[simp]

theorem CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h).inv = (CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g))

class CategoryTheory.Bicategory.HasAbsLeftKanLift {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) extends CategoryTheory.Bicategory.HasLeftKanLift f g : Prop

We say that there exists an absolute left Kan lift of g along f if any 1-morphism h commutes with the left Kan lift f₊ g.

• hasInitial : CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftLift f g)
• commute : ∀ {x : B} (h : x ⟶ c), CategoryTheory.Bicategory.LanLift.CommuteWith f g h

instance CategoryTheory.Bicategory.instCommuteWith_1 {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasAbsLeftKanLift f g] {x : B} (h : x ⟶ c) : CategoryTheory.Bicategory.LanLift.CommuteWith f g h

Equations

• ⋯ = ⋯

theorem CategoryTheory.Bicategory.LeftLift.IsAbsKan.hasAbsLeftKanLift {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) : CategoryTheory.Bicategory.HasAbsLeftKanLift f g