# Extensions and lifts in bicategories #

We introduce the concept of extensions and lifts within the bicategorical framework. These concepts are defined by commutative diagrams in the (1-)categorical context. Within the bicategorical framework, commutative diagrams are replaced by 2-morphisms. Depending on the orientation of the 2-morphisms, we define both left and right extensions (likewise for lifts). The use of left and right here is a common one in the theory of Kan extensions.

## Implementation notes #

We define extensions and lifts as objects in certain comma categories (StructuredArrow for left, and CostructuredArrow for right). See the file CategoryTheory.StructuredArrow for properties about these categories. We introduce some intuitive aliases. For example, LeftExtension.extension is an alias for Comma.right.

## References #

• https://ncatlab.org/nlab/show/lifts+and+extensions
• https://ncatlab.org/nlab/show/Kan+extension
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftExtension {B : Type u} {a : B} {b : B} {c : B} (f : a b) (g : a c) :
Type (max v w)

Triangle diagrams for (left) extensions.

  b
△ \
|   \ extension  △
f |     \          | unit
|       ◿
a - - - ▷ c
g

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftExtension.extension {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} :
b c

The extension of g along f.

Equations
• t.extension = t.right
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftExtension.unit {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} :

The 2-morphism filling the triangle diagram.

Equations
• t.unit = t.hom
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftExtension.mk {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (h : b c) (unit : ) :

Construct a left extension from a 1-morphism and a 2-morphism.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftExtension.homMk {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (η : s.extension t.extension) (w : = t.unit) :
s t

To construct a morphism between left extensions, we need a 2-morphism between the extensions, and to check that it is compatible with the units.

Equations
Instances For
@[simp]
theorem CategoryTheory.Bicategory.LeftExtension.w_assoc {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (η : s t) {Z : a c} (h : Z) :
=
@[simp]
theorem CategoryTheory.Bicategory.LeftExtension.w {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (η : s t) :
def CategoryTheory.Bicategory.LeftExtension.alongId {B : Type u} {a : B} {c : B} (g : a c) :

The left extension along the identity.

Equations
Instances For
instance CategoryTheory.Bicategory.LeftExtension.instInhabitedId {B : Type u} {a : B} {c : B} {g : a c} :
Equations
• CategoryTheory.Bicategory.LeftExtension.instInhabitedId = { default := }
def CategoryTheory.Bicategory.LeftExtension.whisker {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} {x : B} (h : c x) :

Whisker a 1-morphism to an extension.

  b
△ \
|   \ extension  △
f |     \          | unit
|       ◿
a - - - ▷ c - - - ▷ x
g         h

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Bicategory.LeftExtension.whisker_extension {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} {x : B} (h : c x) :
(t.whisker h).extension = CategoryTheory.CategoryStruct.comp t.extension h
@[simp]
theorem CategoryTheory.Bicategory.LeftExtension.whisker_unit {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} {x : B} (h : c x) :
@[simp]
theorem CategoryTheory.Bicategory.LeftExtension.whiskering_obj {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} {x : B} (h : c x) :
= t.whisker h
@[simp]
theorem CategoryTheory.Bicategory.LeftExtension.whiskering_map {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} {x : B} (h : c x) :
∀ {X Y : } (η : X Y),
def CategoryTheory.Bicategory.LeftExtension.whiskering {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} {x : B} (h : c x) :

Whiskering a 1-morphism is a functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Bicategory.LeftExtension.whiskerIdCancel_right {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (τ : s.whisker t.whisker ) :
def CategoryTheory.Bicategory.LeftExtension.whiskerIdCancel {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (τ : s.whisker t.whisker ) :
s t

Define a morphism between left extensions by cancelling the whiskered identities.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftLift {B : Type u} {a : B} {b : B} {c : B} (f : b a) (g : c a) :
Type (max v w)

Triangle diagrams for (left) lifts.

            b
◹ |
lift /   |      △
/     | f    | unit
/       ▽
c - - - ▷ a
g

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftLift.lift {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : ) :
c b

The lift of g along f.

Equations
• t.lift = t.right
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftLift.unit {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : ) :
g

The 2-morphism filling the triangle diagram.

Equations
• t.unit = t.hom
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftLift.mk {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (h : c b) (unit : ) :

Construct a left lift from a 1-morphism and a 2-morphism.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftLift.homMk {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : } {t : } (η : s.lift t.lift) (w : = t.unit) :
s t

To construct a morphism between left lifts, we need a 2-morphism between the lifts, and to check that it is compatible with the units.

Equations
Instances For
@[simp]
theorem CategoryTheory.Bicategory.LeftLift.w_assoc {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : } {t : } (h : s t) {Z : c a} (h : Z) :
=
@[simp]
theorem CategoryTheory.Bicategory.LeftLift.w {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : } {t : } (h : s t) :
def CategoryTheory.Bicategory.LeftLift.alongId {B : Type u} {a : B} {c : B} (g : c a) :

The left lift along the identity.

Equations
Instances For
instance CategoryTheory.Bicategory.LeftLift.instInhabitedId {B : Type u} {a : B} {c : B} {g : c a} :
Equations
• CategoryTheory.Bicategory.LeftLift.instInhabitedId = { default := }
def CategoryTheory.Bicategory.LeftLift.whisker {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : ) {x : B} (h : x c) :

Whisker a 1-morphism to a lift.

                    b
◹ |
lift /   |      △
/     | f    | unit
/       ▽
x - - - ▷ c - - - ▷ a
h         g

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Bicategory.LeftLift.whisker_lift {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : ) {x : B} (h : x c) :
(t.whisker h).lift =
@[simp]
theorem CategoryTheory.Bicategory.LeftLift.whisker_unit {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : ) {x : B} (h : x c) :
(t.whisker h).unit = CategoryTheory.CategoryStruct.comp () ().inv
@[simp]
theorem CategoryTheory.Bicategory.LeftLift.whiskering_obj {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {x : B} (h : x c) (t : ) :
= t.whisker h
@[simp]
theorem CategoryTheory.Bicategory.LeftLift.whiskering_map {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {x : B} (h : x c) :
∀ {X Y : } (η : X Y),
def CategoryTheory.Bicategory.LeftLift.whiskering {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {x : B} (h : x c) :

Whiskering a 1-morphism is a functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Bicategory.LeftLift.whiskerIdCancel_right {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : } {t : } (τ : s.whisker t.whisker ) :
def CategoryTheory.Bicategory.LeftLift.whiskerIdCancel {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : } {t : } (τ : s.whisker t.whisker ) :
s t

Define a morphism between left lifts by cancelling the whiskered identities.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightExtension {B : Type u} {a : B} {b : B} {c : B} (f : a b) (g : a c) :
Type (max v w)

Triangle diagrams for (right) extensions.

  b
△ \
|   \ extension  | counit
f |     \          ▽
|       ◿
a - - - ▷ c
g

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightExtension.extension {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} :
b c

The extension of g along f.

Equations
• t.extension = t.left
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightExtension.counit {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} :

The 2-morphism filling the triangle diagram.

Equations
• t.counit = t.hom
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightExtension.mk {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (h : b c) (counit : ) :

Construct a right extension from a 1-morphism and a 2-morphism.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightExtension.homMk {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (η : s.extension t.extension) (w : = s.counit) :
s t

To construct a morphism between right extensions, we need a 2-morphism between the extensions, and to check that it is compatible with the counits.

Equations
Instances For
@[simp]
theorem CategoryTheory.Bicategory.RightExtension.w_assoc {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (η : s t) {Z : a c} (h : g Z) :
@[simp]
theorem CategoryTheory.Bicategory.RightExtension.w {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a c} (η : s t) :
def CategoryTheory.Bicategory.RightExtension.alongId {B : Type u} {a : B} {c : B} (g : a c) :

The right extension along the identity.

Equations
Instances For
instance CategoryTheory.Bicategory.RightExtension.instInhabitedId {B : Type u} {a : B} {c : B} {g : a c} :
Equations
• CategoryTheory.Bicategory.RightExtension.instInhabitedId = { default := }
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightLift {B : Type u} {a : B} {b : B} {c : B} (f : b a) (g : c a) :
Type (max v w)

Triangle diagrams for (right) lifts.

            b
◹ |
lift /   |      | counit
/     | f    ▽
/       ▽
c - - - ▷ a
g

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightLift.lift {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : ) :
c b

The lift of g along f.

Equations
• t.lift = t.left
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightLift.counit {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : ) :
g

The 2-morphism filling the triangle diagram.

Equations
• t.counit = t.hom
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightLift.mk {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} (h : c b) (counit : ) :

Construct a right lift from a 1-morphism and a 2-morphism.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Bicategory.RightLift.homMk {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : } {t : } (η : s.lift t.lift) (w : = s.counit) :
s t

To construct a morphism between right lifts, we need a 2-morphism between the lifts, and to check that it is compatible with the counits.

Equations
Instances For
@[simp]
theorem CategoryTheory.Bicategory.RightLift.w_assoc {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : } {t : } (h : s t) {Z : c a} (h : g Z) :
@[simp]
theorem CategoryTheory.Bicategory.RightLift.w {B : Type u} {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : } {t : } (h : s t) :
def CategoryTheory.Bicategory.RightLift.alongId {B : Type u} {a : B} {c : B} (g : c a) :

The right lift along the identity.

Equations
Instances For
instance CategoryTheory.Bicategory.RightLift.instInhabitedId {B : Type u} {a : B} {c : B} {g : c a} :
Equations
• CategoryTheory.Bicategory.RightLift.instInhabitedId = { default := }