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 gis the left Kan extension ofgalongf, and is denoted byf⁺ g.lanLift f gis the left Kan lift ofgalongf, and is denoted byf₊ g.
These notations are inspired by M. Kashiwara, P. Schapira, Categories and Sheaves.
TODO #
ran f gis the right Kan extension ofgalongf, and is denoted byf⁺⁺ g.ranLift f gis the right Kan lift ofgalongf, and is denoted byf₊₊ g.
class
CategoryTheory.Bicategory.HasLeftKanExtension
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : a ⟶ b)
(g : a ⟶ c)
:
The existence of a left Kan extension of g along f.
- hasInitial : CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftExtension f g)
Instances
theorem
CategoryTheory.Bicategory.HasLeftKanExtension.hasInitial
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
[self : CategoryTheory.Bicategory.HasLeftKanExtension f g]
:
theorem
CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension
{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)
:
instance
CategoryTheory.Bicategory.instHasInitialLeftExtensionOfHasLeftKanExtension
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
[CategoryTheory.Bicategory.HasLeftKanExtension f g]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Bicategory.lanLeftExtension
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : a ⟶ b)
(g : a ⟶ c)
[CategoryTheory.Bicategory.HasLeftKanExtension 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}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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
Instances For
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.
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.lanLeftExtension_extension
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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}
{b : B}
{c : B}
(f : a ⟶ b)
(g : a ⟶ c)
[CategoryTheory.Bicategory.HasLeftKanExtension f g]
:
The unit for the left Kan extension f⁺ g.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.lanLeftExtension_unit
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : a ⟶ b)
(g : a ⟶ c)
[CategoryTheory.Bicategory.HasLeftKanExtension f g]
:
def
CategoryTheory.Bicategory.lanIsKan
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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
Instances For
def
CategoryTheory.Bicategory.lanDesc
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.lanUnit_desc_assoc
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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)
:
@[simp]
theorem
CategoryTheory.Bicategory.lanUnit_desc
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
[CategoryTheory.Bicategory.HasLeftKanExtension f g]
(s : CategoryTheory.Bicategory.LeftExtension f g)
:
@[simp]
theorem
CategoryTheory.Bicategory.lanIsKan_desc
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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}
{b : 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}
{b : B}
{c : B}
(f : a ⟶ b)
(g : a ⟶ c)
[CategoryTheory.Bicategory.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 ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h).IsKan
Instances
theorem
CategoryTheory.Bicategory.Lan.CommuteWith.commute
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
[CategoryTheory.Bicategory.HasLeftKanExtension f g]
{x : B}
{h : c ⟶ x}
[self : CategoryTheory.Bicategory.Lan.CommuteWith f g h]
:
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}
{b : 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)
:
theorem
CategoryTheory.Bicategory.Lan.CommuteWith.of_lan_comp_iso
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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)
:
def
CategoryTheory.Bicategory.Lan.CommuteWith.isKan
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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
Instances For
instance
CategoryTheory.Bicategory.Lan.CommuteWith.instHasLeftKanExtensionComp
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Bicategory.Lan.CommuteWith.isKanWhisker
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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.
Instances For
def
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
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.
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_hom_right
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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}
{b : 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]
:
@[simp]
theorem
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_inv
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
@[simp]
theorem
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_hom
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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)
def
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
The 1-morphism h commutes with the left Kan extension f⁺ g.
Equations
Instances For
class
CategoryTheory.Bicategory.HasAbsLeftKanExtension
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : a ⟶ b)
(g : a ⟶ c)
extends
CategoryTheory.Bicategory.HasLeftKanExtension
:
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
Instances
theorem
CategoryTheory.Bicategory.HasAbsLeftKanExtension.commute
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
[self : CategoryTheory.Bicategory.HasAbsLeftKanExtension f g]
{x : B}
(h : c ⟶ x)
:
instance
CategoryTheory.Bicategory.instCommuteWith
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : a ⟶ b}
{g : a ⟶ c}
[CategoryTheory.Bicategory.HasAbsLeftKanExtension f g]
{x : B}
(h : c ⟶ x)
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Bicategory.LeftExtension.IsAbsKan.hasAbsLeftKanExtension
{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)
:
class
CategoryTheory.Bicategory.HasLeftKanLift
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : b ⟶ a)
(g : c ⟶ a)
:
The existence of a left kan lift of g along f.
- mk' :: (
- hasInitial : CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftLift f g)
- )
Instances
theorem
CategoryTheory.Bicategory.HasLeftKanLift.hasInitial
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
[self : CategoryTheory.Bicategory.HasLeftKanLift f g]
:
theorem
CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift
{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)
:
instance
CategoryTheory.Bicategory.instHasInitialLeftLiftOfHasLeftKanLift
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
[CategoryTheory.Bicategory.HasLeftKanLift f g]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Bicategory.lanLiftLeftLift
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : b ⟶ a)
(g : c ⟶ a)
[CategoryTheory.Bicategory.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}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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
Instances For
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.
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.lanLiftLeftLift_lift
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : b ⟶ a)
(g : c ⟶ a)
[CategoryTheory.Bicategory.HasLeftKanLift f g]
:
def
CategoryTheory.Bicategory.lanLiftUnit
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : b ⟶ a)
(g : c ⟶ a)
[CategoryTheory.Bicategory.HasLeftKanLift f g]
:
The unit for the left Kan lift f₊ g.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.lanLiftLeftLift_unit
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : b ⟶ a)
(g : c ⟶ a)
[CategoryTheory.Bicategory.HasLeftKanLift f g]
:
def
CategoryTheory.Bicategory.lanLiftIsKan
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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
Instances For
def
CategoryTheory.Bicategory.lanLiftDesc
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.lanLiftUnit_desc_assoc
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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)
:
@[simp]
theorem
CategoryTheory.Bicategory.lanLiftUnit_desc
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
[CategoryTheory.Bicategory.HasLeftKanLift f g]
(s : CategoryTheory.Bicategory.LeftLift f g)
:
@[simp]
theorem
CategoryTheory.Bicategory.lanLiftIsKan_desc
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
[CategoryTheory.Bicategory.HasLeftKanLift f g]
(s : CategoryTheory.Bicategory.LeftLift f g)
:
theorem
CategoryTheory.Bicategory.LanLift.existsUnique
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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}
{b : B}
{c : B}
(f : b ⟶ a)
(g : c ⟶ a)
[CategoryTheory.Bicategory.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 ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h).IsKan
Instances
theorem
CategoryTheory.Bicategory.LanLift.CommuteWith.commute
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
[CategoryTheory.Bicategory.HasLeftKanLift f g]
{x : B}
{h : x ⟶ c}
[self : CategoryTheory.Bicategory.LanLift.CommuteWith f g h]
:
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}
{b : 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)
:
theorem
CategoryTheory.Bicategory.LanLift.CommuteWith.of_lanLift_comp_iso
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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)
:
def
CategoryTheory.Bicategory.LanLift.CommuteWith.isKan
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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
Instances For
instance
CategoryTheory.Bicategory.LanLift.CommuteWith.instHasLeftKanLiftComp
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Bicategory.LanLift.CommuteWith.isKanWhisker
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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.
Instances For
def
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
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.
Instances For
@[simp]
theorem
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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}
{b : 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]
:
@[simp]
theorem
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_inv
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
@[simp]
theorem
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_hom
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
def
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : 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]
:
The 1-morphism h commutes with the left Kan lift f₊ g.
Equations
Instances For
class
CategoryTheory.Bicategory.HasAbsLeftKanLift
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
(f : b ⟶ a)
(g : c ⟶ a)
extends
CategoryTheory.Bicategory.HasLeftKanLift
:
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
Instances
theorem
CategoryTheory.Bicategory.HasAbsLeftKanLift.commute
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
[self : CategoryTheory.Bicategory.HasAbsLeftKanLift f g]
{x : B}
(h : x ⟶ c)
:
instance
CategoryTheory.Bicategory.instCommuteWith_1
{B : Type u}
[CategoryTheory.Bicategory B]
{a : B}
{b : B}
{c : B}
{f : b ⟶ a}
{g : c ⟶ a}
[CategoryTheory.Bicategory.HasAbsLeftKanLift f g]
{x : B}
(h : x ⟶ c)
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Bicategory.LeftLift.IsAbsKan.hasAbsLeftKanLift
{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)
: