Documentation

Mathlib.CategoryTheory.Bicategory.Kan.HasKan

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} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) :

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

hasInitial : Limits.HasInitial (LeftExtension f g)

Instances

theorem CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} (H : t.IsKan) :

HasLeftKanExtension f g

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

Limits.HasInitial (LeftExtension f g)

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

LeftExtension f g

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

Equations

Instances For

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

b ⟶ c

The left Kan extension of g along f.

Equations

Instances For

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

Instances For

@[simp]

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

(lanLeftExtension f g).extension = lan f g

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

g ⟶ CategoryStruct.comp f (lan f g)

The unit for the left Kan extension f⁺ g.

Equations

Instances For

@[simp]

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

(lanLeftExtension f g).unit = lanUnit f g

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

(lanLeftExtension f g).IsKan

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

Equations

Instances For

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

lan f g ⟶ s.extension

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

Equations

Instances For

@[simp]

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

CategoryStruct.comp (lanUnit f g) (whiskerLeft f (lanDesc s)) = s.unit

@[simp]

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

CategoryStruct.comp (lanUnit f g) (CategoryStruct.comp (whiskerLeft f (lanDesc s)) h) = CategoryStruct.comp s.unit h

@[simp]

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

(lanIsKan f g).desc s = lanDesc s

theorem CategoryTheory.Bicategory.Lan.existsUnique {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [HasLeftKanExtension f g] (s : LeftExtension f g) :

∃! τ : lan f g ⟶ s.extension, CategoryStruct.comp (lanUnit f g) (whiskerLeft f τ) = s.unit

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

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 ((lanLeftExtension f g).whisker h).IsKan

Instances

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

CommuteWith f g h

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

CommuteWith f g h

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

((lanLeftExtension f g).whisker h).IsKan

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

Equations

Instances For

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

HasLeftKanExtension f (CategoryStruct.comp g h)

def CategoryTheory.Bicategory.Lan.CommuteWith.isKanWhisker {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [HasLeftKanExtension f g] (t : LeftExtension f g) (H : t.IsKan) {x : B} (h : c ⟶ x) [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

Instances For

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

lanLeftExtension f (CategoryStruct.comp g h) ≅ (lanLeftExtension f g).whisker h

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

Equations

Instances For

@[simp]

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

(lanCompIsoWhisker f g h).hom.right = lanDesc ((lanLeftExtension f g).whisker h)

@[simp]

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

(lanCompIsoWhisker f g h).inv.right = (isKan f g h).desc (lanLeftExtension f (CategoryStruct.comp g h))

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

lan f (CategoryStruct.comp g h) ≅ CategoryStruct.comp (lan f g) h

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

Equations

Instances For

@[simp]

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

(lanCompIso f g h).inv = (isKan f g h).desc (lanLeftExtension f (CategoryStruct.comp g h))

@[simp]

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

(lanCompIso f g h).hom = lanDesc ((lanLeftExtension f g).whisker h)

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

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 : Limits.HasInitial (LeftExtension f g)
commute {x : B} (h : c ⟶ x) : Lan.CommuteWith f g h

Instances

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

Lan.CommuteWith f g h

theorem CategoryTheory.Bicategory.LeftExtension.IsAbsKan.hasAbsLeftKanExtension {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {t : LeftExtension f g} (H : t.IsAbsKan) :

HasAbsLeftKanExtension f g

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

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

mk' :: (

hasInitial : Limits.HasInitial (LeftLift f g)

)

Instances

theorem CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} (H : t.IsKan) :

HasLeftKanLift f g

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

Limits.HasInitial (LeftLift f g)

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

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

Equations

Instances For

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

c ⟶ b

The left Kan lift of g along f.

Equations

Instances For

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

Instances For

@[simp]

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

(lanLiftLeftLift f g).lift = lanLift f g

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

g ⟶ CategoryStruct.comp (lanLift f g) f

The unit for the left Kan lift f₊ g.

Equations

Instances For

@[simp]

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

(lanLiftLeftLift f g).unit = lanLiftUnit f g

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

(lanLiftLeftLift f g).IsKan

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

Equations

Instances For

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

lanLift f g ⟶ s.lift

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

Equations

Instances For

@[simp]

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

CategoryStruct.comp (lanLiftUnit f g) (whiskerRight (lanLiftDesc s) f) = s.unit

@[simp]

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

CategoryStruct.comp (lanLiftUnit f g) (CategoryStruct.comp (whiskerRight (lanLiftDesc s) f) h) = CategoryStruct.comp s.unit h

@[simp]

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

(lanLiftIsKan f g).desc s = lanLiftDesc s

theorem CategoryTheory.Bicategory.LanLift.existsUnique {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [HasLeftKanLift f g] (s : LeftLift f g) :

∃! τ : lanLift f g ⟶ s.lift, CategoryStruct.comp (lanLiftUnit f g) (whiskerRight τ f) = s.unit

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

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 ((lanLiftLeftLift f g).whisker h).IsKan

Instances

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

CommuteWith f g h

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

CommuteWith f g h

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

((lanLiftLeftLift f g).whisker h).IsKan

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

Equations

Instances For

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

HasLeftKanLift f (CategoryStruct.comp h g)

def CategoryTheory.Bicategory.LanLift.CommuteWith.isKanWhisker {B : Type u} [Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [HasLeftKanLift f g] (t : LeftLift f g) (H : t.IsKan) {x : B} (h : x ⟶ c) [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

Instances For

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

lanLiftLeftLift f (CategoryStruct.comp h g) ≅ (lanLiftLeftLift f g).whisker h

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

Equations

Instances For

@[simp]

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

(lanLiftCompIsoWhisker f g h).hom.right = lanLiftDesc ((lanLiftLeftLift f g).whisker h)

@[simp]

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

(lanLiftCompIsoWhisker f g h).inv.right = (isKan f g h).desc (lanLiftLeftLift f (CategoryStruct.comp h g))

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

lanLift f (CategoryStruct.comp h g) ≅ CategoryStruct.comp h (lanLift f g)

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

Equations

Instances For

@[simp]

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

(lanLiftCompIso f g h).inv = (isKan f g h).desc (lanLiftLeftLift f (CategoryStruct.comp h g))

@[simp]

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

(lanLiftCompIso f g h).hom = lanLiftDesc ((lanLiftLeftLift f g).whisker h)

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

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 : Limits.HasInitial (LeftLift f g)
commute {x : B} (h : x ⟶ c) : LanLift.CommuteWith f g h

Instances

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

LanLift.CommuteWith f g h

theorem CategoryTheory.Bicategory.LeftLift.IsAbsKan.hasAbsLeftKanLift {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {t : LeftLift f g} (H : t.IsAbsKan) :

HasAbsLeftKanLift f g