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

@[inline, reducible]

abbrev CategoryTheory.Bicategory.LeftExtension {B : Type u} [CategoryTheory.Bicategory B] {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

• CategoryTheory.Bicategory.LeftExtension f g = CategoryTheory.StructuredArrow g (CategoryTheory.Bicategory.precomp c f)

@[inline, reducible]

abbrev CategoryTheory.Bicategory.LeftExtension.extension {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ c} (t : CategoryTheory.Bicategory.LeftExtension f g) : b ⟶ c

The extension of g along f.

Equations

• CategoryTheory.Bicategory.LeftExtension.extension t = t.right

@[inline, reducible]

abbrev CategoryTheory.Bicategory.LeftExtension.unit {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ c} (t : CategoryTheory.Bicategory.LeftExtension f g) : g ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Bicategory.LeftExtension.extension t)

The 2-morphism filling the triangle diagram.

Equations

• CategoryTheory.Bicategory.LeftExtension.unit t = t.hom

def CategoryTheory.Bicategory.LeftExtension.alongId {B : Type u} [CategoryTheory.Bicategory B] {a : B} {c : B} (g : a ⟶ c) : CategoryTheory.Bicategory.LeftExtension (CategoryTheory.CategoryStruct.id a) g

The left extension along the identity.

Equations

• CategoryTheory.Bicategory.LeftExtension.alongId g = CategoryTheory.StructuredArrow.mk (CategoryTheory.Bicategory.leftUnitor g).inv

instance CategoryTheory.Bicategory.LeftExtension.instInhabitedLeftExtensionIdToCategoryStruct {B : Type u} [CategoryTheory.Bicategory B] {a : B} {c : B} {g : a ⟶ c} : Inhabited (CategoryTheory.Bicategory.LeftExtension (CategoryTheory.CategoryStruct.id a) g)

Equations

• CategoryTheory.Bicategory.LeftExtension.instInhabitedLeftExtensionIdToCategoryStruct = { default := CategoryTheory.Bicategory.LeftExtension.alongId g }

@[inline, reducible]

abbrev CategoryTheory.Bicategory.LeftLift {B : Type u} [CategoryTheory.Bicategory B] {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

• CategoryTheory.Bicategory.LeftLift f g = CategoryTheory.StructuredArrow g (CategoryTheory.Bicategory.postcomp c f)

@[inline, reducible]

abbrev CategoryTheory.Bicategory.LeftLift.lift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} (t : CategoryTheory.Bicategory.LeftLift f g) : c ⟶ b

The lift of g along f.

Equations

• CategoryTheory.Bicategory.LeftLift.lift t = t.right

@[inline, reducible]

abbrev CategoryTheory.Bicategory.LeftLift.unit {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} (t : CategoryTheory.Bicategory.LeftLift f g) : g ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.LeftLift.lift t) f

The 2-morphism filling the triangle diagram.

Equations

• CategoryTheory.Bicategory.LeftLift.unit t = t.hom

def CategoryTheory.Bicategory.LeftLift.alongId {B : Type u} [CategoryTheory.Bicategory B] {a : B} {c : B} (g : c ⟶ a) : CategoryTheory.Bicategory.LeftLift (CategoryTheory.CategoryStruct.id a) g

The left lift along the identity.

Equations

• CategoryTheory.Bicategory.LeftLift.alongId g = CategoryTheory.StructuredArrow.mk (CategoryTheory.Bicategory.rightUnitor g).inv

instance CategoryTheory.Bicategory.LeftLift.instInhabitedLeftLiftIdToCategoryStruct {B : Type u} [CategoryTheory.Bicategory B] {a : B} {c : B} {g : c ⟶ a} : Inhabited (CategoryTheory.Bicategory.LeftLift (CategoryTheory.CategoryStruct.id a) g)

Equations

• CategoryTheory.Bicategory.LeftLift.instInhabitedLeftLiftIdToCategoryStruct = { default := CategoryTheory.Bicategory.LeftLift.alongId g }

@[inline, reducible]

abbrev CategoryTheory.Bicategory.RightExtension {B : Type u} [CategoryTheory.Bicategory B] {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

• CategoryTheory.Bicategory.RightExtension f g = CategoryTheory.CostructuredArrow (CategoryTheory.Bicategory.precomp c f) g

@[inline, reducible]

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

The extension of g along f.

Equations

• CategoryTheory.Bicategory.RightExtension.extension t = t.left

@[inline, reducible]

abbrev CategoryTheory.Bicategory.RightExtension.counit {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ c} (t : CategoryTheory.Bicategory.RightExtension f g) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Bicategory.RightExtension.extension t) ⟶ g

The 2-morphism filling the triangle diagram.

Equations

• CategoryTheory.Bicategory.RightExtension.counit t = t.hom

def CategoryTheory.Bicategory.RightExtension.alongId {B : Type u} [CategoryTheory.Bicategory B] {a : B} {c : B} (g : a ⟶ c) : CategoryTheory.Bicategory.RightExtension (CategoryTheory.CategoryStruct.id a) g

The right extension along the identity.

Equations

• CategoryTheory.Bicategory.RightExtension.alongId g = CategoryTheory.CostructuredArrow.mk (CategoryTheory.Bicategory.leftUnitor g).hom

instance CategoryTheory.Bicategory.RightExtension.instInhabitedRightExtensionIdToCategoryStruct {B : Type u} [CategoryTheory.Bicategory B] {a : B} {c : B} {g : a ⟶ c} : Inhabited (CategoryTheory.Bicategory.RightExtension (CategoryTheory.CategoryStruct.id a) g)

Equations

• CategoryTheory.Bicategory.RightExtension.instInhabitedRightExtensionIdToCategoryStruct = { default := CategoryTheory.Bicategory.RightExtension.alongId g }

@[inline, reducible]

abbrev CategoryTheory.Bicategory.RightLift {B : Type u} [CategoryTheory.Bicategory B] {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

• CategoryTheory.Bicategory.RightLift f g = CategoryTheory.CostructuredArrow (CategoryTheory.Bicategory.postcomp c f) g

@[inline, reducible]

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

The lift of g along f.

Equations

• CategoryTheory.Bicategory.RightLift.lift t = t.left

@[inline, reducible]

abbrev CategoryTheory.Bicategory.RightLift.counit {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b ⟶ a} {g : c ⟶ a} (t : CategoryTheory.Bicategory.RightLift f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.RightLift.lift t) f ⟶ g

The 2-morphism filling the triangle diagram.

Equations

• CategoryTheory.Bicategory.RightLift.counit t = t.hom

def CategoryTheory.Bicategory.RightLift.alongId {B : Type u} [CategoryTheory.Bicategory B] {a : B} {c : B} (g : c ⟶ a) : CategoryTheory.Bicategory.RightLift (CategoryTheory.CategoryStruct.id a) g

The right lift along the identity.

Equations

• CategoryTheory.Bicategory.RightLift.alongId g = CategoryTheory.CostructuredArrow.mk (CategoryTheory.Bicategory.rightUnitor g).hom

instance CategoryTheory.Bicategory.RightLift.instInhabitedRightLiftIdToCategoryStruct {B : Type u} [CategoryTheory.Bicategory B] {a : B} {c : B} {g : c ⟶ a} : Inhabited (CategoryTheory.Bicategory.RightLift (CategoryTheory.CategoryStruct.id a) g)

Equations

• CategoryTheory.Bicategory.RightLift.instInhabitedRightLiftIdToCategoryStruct = { default := CategoryTheory.Bicategory.RightLift.alongId g }