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} [Bicategory B] {a 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)

@[reducible, inline]

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

The extension of g along f.

Equations

• t.extension = CategoryTheory.StructuredArrow.right t

@[reducible, inline]

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

The 2-morphism filling the triangle diagram.

Equations

• t.unit = CategoryTheory.StructuredArrow.hom t

@[reducible, inline]

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

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

Equations

• CategoryTheory.Bicategory.LeftExtension.mk h unit = CategoryTheory.StructuredArrow.mk unit

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftExtension.homMk {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (η : s.extension ⟶ t.extension) (w : CategoryStruct.comp s.unit (whiskerLeft f η) = t.unit := by cat_disch) : 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

• CategoryTheory.Bicategory.LeftExtension.homMk η w = CategoryTheory.StructuredArrow.homMk η w

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.w {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (η : s ⟶ t) : CategoryStruct.comp s.unit (whiskerLeft f (StructuredArrow.Hom.right η)) = t.unit

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.w_assoc {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (η : s ⟶ t) {Z : a ⟶ c} (h : CategoryStruct.comp f (StructuredArrow.right t) ⟶ Z) : CategoryStruct.comp s.unit (CategoryStruct.comp (whiskerLeft f (StructuredArrow.Hom.right η)) h) = CategoryStruct.comp t.unit h

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

The left extension along the identity.

Equations

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

@[instance_reducible]

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

Equations

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

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftExtension.ofCompId {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f (CategoryStruct.comp g (CategoryStruct.id c))) : LeftExtension f g

Construct a left extension of g : a ⟶ c from a left extension of g ≫ 𝟙 c.

Equations

• t.ofCompId = CategoryTheory.Bicategory.LeftExtension.mk t.extension (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv t.unit)

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.ofCompId_hom {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f (CategoryStruct.comp g (CategoryStruct.id c))) : t.ofCompId.hom = CategoryStruct.comp (rightUnitor g).inv t.unit

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.ofCompId_left_as {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f (CategoryStruct.comp g (CategoryStruct.id c))) : t.ofCompId.left.as = PUnit.unit

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.ofCompId_right {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f (CategoryStruct.comp g (CategoryStruct.id c))) : t.ofCompId.right = t.extension

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftExtension.whisker {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f g) {x : B} (h : c ⟶ x) : LeftExtension f (CategoryStruct.comp g h)

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.

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whisker_extension {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f g) {x : B} (h : c ⟶ x) : (t.whisker h).extension = CategoryStruct.comp t.extension h

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whisker_unit {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f g) {x : B} (h : c ⟶ x) : (t.whisker h).unit = CategoryStruct.comp (whiskerRight t.unit h) (associator f t.extension h).hom

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftExtension.whiskering {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} (h : c ⟶ x) : Functor (LeftExtension f g) (LeftExtension f (CategoryStruct.comp g h))

Whiskering a 1-morphism is a functor.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskering_map {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} (h : c ⟶ x) {X✝ Y✝ : LeftExtension f g} (η : X✝ ⟶ Y✝) : (whiskering h).map η = homMk (whiskerRight (StructuredArrow.Hom.right η) h) ⋯

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskering_obj {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} (h : c ⟶ x) (t : LeftExtension f g) : (whiskering h).obj t = t.whisker h

def CategoryTheory.Bicategory.LeftExtension.whiskerIdCancel {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (s : LeftExtension f (CategoryStruct.comp g (CategoryStruct.id c))) {t : LeftExtension f g} (τ : s ⟶ t.whisker (CategoryStruct.id c)) : s.ofCompId ⟶ 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.

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskerIdCancel_right {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (s : LeftExtension f (CategoryStruct.comp g (CategoryStruct.id c))) {t : LeftExtension f g} (τ : s ⟶ t.whisker (CategoryStruct.id c)) : (s.whiskerIdCancel τ).right = CategoryStruct.comp (StructuredArrow.Hom.right τ) (rightUnitor t.extension).hom

def CategoryTheory.Bicategory.LeftExtension.whiskerHom {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (i : s ⟶ t) {x : B} (h : c ⟶ x) : s.whisker h ⟶ t.whisker h

Construct a morphism between whiskered extensions.

Equations

• CategoryTheory.Bicategory.LeftExtension.whiskerHom i h = CategoryTheory.StructuredArrow.homMk (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.StructuredArrow.Hom.right i) h) ⋯

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskerHom_right {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (i : s ⟶ t) {x : B} (h : c ⟶ x) : (whiskerHom i h).right = whiskerRight (StructuredArrow.Hom.right i) h

def CategoryTheory.Bicategory.LeftExtension.whiskerIso {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (i : s ≅ t) {x : B} (h : c ⟶ x) : s.whisker h ≅ t.whisker h

Construct an isomorphism between whiskered extensions.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskerIso_inv {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (i : s ≅ t) {x : B} (h : c ⟶ x) : (whiskerIso i h).inv = whiskerHom i.inv h

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskerIso_hom {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : LeftExtension f g} (i : s ≅ t) {x : B} (h : c ⟶ x) : (whiskerIso i h).hom = whiskerHom i.hom h

def CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f g) : (t.whisker (CategoryStruct.id c)).ofCompId ≅ t

The isomorphism between left extensions induced by a right unitor.

Equations

• t.whiskerOfCompIdIsoSelf = CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Bicategory.rightUnitor t.extension) ⋯

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf_inv_right {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f g) : t.whiskerOfCompIdIsoSelf.inv.right = (rightUnitor t.extension).inv

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf_hom_right {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : LeftExtension f g) : t.whiskerOfCompIdIsoSelf.hom.right = (rightUnitor t.extension).hom

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftExtension.mapIso {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') : LeftExtension f g ≌ LeftExtension f' g'

Given isomorphisms ef : f ≅ f' and eg : g ≅ g', the induced equivalence between their categories of left extensions.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftExtension.ofIso {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : LeftExtension f g) : LeftExtension f' g'

Given isomorphisms ef : f ≅ f' and eg : g ≅ g', and a left extension t : LeftExtension f g, the induced left extension t.ofIso : LeftExtension f' g'.

Equations

• CategoryTheory.Bicategory.LeftExtension.ofIso ef eg t = (CategoryTheory.Bicategory.LeftExtension.mapIso ef eg).functor.obj t

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.ofIso_extension {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : LeftExtension f g) : (ofIso ef eg t).extension = t.extension

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.ofIso_unit {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : LeftExtension f g) : (ofIso ef eg t).unit = CategoryStruct.comp eg.inv (CategoryStruct.comp t.unit (whiskerRight ef.hom t.extension))

def CategoryTheory.Bicategory.LeftExtension.whiskerOfIso {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : LeftExtension f g) {x : B} (h : c ⟶ x) : ofIso ef (whiskerRightIso eg h) (t.whisker h) ≅ (ofIso ef eg t).whisker h

Whiskering commutes with LeftExtension.ofIso.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskerOfIso_inv_right {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : LeftExtension f g) {x : B} (h : c ⟶ x) : (whiskerOfIso ef eg t h).inv.right = CategoryStruct.id (CategoryStruct.comp t.extension h)

@[simp]

theorem CategoryTheory.Bicategory.LeftExtension.whiskerOfIso_hom_right {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : LeftExtension f g) {x : B} (h : c ⟶ x) : (whiskerOfIso ef eg t h).hom.right = CategoryStruct.id (CategoryStruct.comp t.extension h)

@[reducible, inline]

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

@[reducible, inline]

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

The lift of g along f.

Equations

• t.lift = CategoryTheory.StructuredArrow.right t

@[reducible, inline]

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

The 2-morphism filling the triangle diagram.

Equations

• t.unit = CategoryTheory.StructuredArrow.hom t

@[reducible, inline]

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

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

Equations

• CategoryTheory.Bicategory.LeftLift.mk h unit = CategoryTheory.StructuredArrow.mk unit

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.homMk {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (η : s.lift ⟶ t.lift) (w : CategoryStruct.comp s.unit (whiskerRight η f) = t.unit := by cat_disch) : 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

• CategoryTheory.Bicategory.LeftLift.homMk η w = CategoryTheory.StructuredArrow.homMk η w

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.w {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (η : s ⟶ t) : CategoryStruct.comp s.unit (whiskerRight (StructuredArrow.Hom.right η) f) = t.unit

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.w_assoc {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (η : s ⟶ t) {Z : c ⟶ a} (h : CategoryStruct.comp (StructuredArrow.right t) f ⟶ Z) : CategoryStruct.comp s.unit (CategoryStruct.comp (whiskerRight (StructuredArrow.Hom.right η) f) h) = CategoryStruct.comp t.unit h

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

The left lift along the identity.

Equations

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

@[instance_reducible]

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

Equations

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

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftLift.ofIdComp {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f (CategoryStruct.comp (CategoryStruct.id c) g)) : LeftLift f g

Construct a left lift of g : c ⟶ a from a left lift of 𝟙 c ≫ g.

Equations

• t.ofIdComp = CategoryTheory.Bicategory.LeftLift.mk t.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv t.unit)

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.ofIdComp_right {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f (CategoryStruct.comp (CategoryStruct.id c) g)) : t.ofIdComp.right = t.lift

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.ofIdComp_hom {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f (CategoryStruct.comp (CategoryStruct.id c) g)) : t.ofIdComp.hom = CategoryStruct.comp (leftUnitor g).inv t.unit

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.ofIdComp_left_as {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f (CategoryStruct.comp (CategoryStruct.id c) g)) : t.ofIdComp.left.as = PUnit.unit

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftLift.whisker {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f g) {x : B} (h : x ⟶ c) : LeftLift f (CategoryStruct.comp h g)

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.

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whisker_lift {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f g) {x : B} (h : x ⟶ c) : (t.whisker h).lift = CategoryStruct.comp h t.lift

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whisker_unit {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f g) {x : B} (h : x ⟶ c) : (t.whisker h).unit = CategoryStruct.comp (whiskerLeft h t.unit) (associator h t.lift f).inv

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftLift.whiskering {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c) : Functor (LeftLift f g) (LeftLift f (CategoryStruct.comp h g))

Whiskering a 1-morphism is a functor.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskering_map {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c) {X✝ Y✝ : LeftLift f g} (η : X✝ ⟶ Y✝) : (whiskering h).map η = homMk (whiskerLeft h (StructuredArrow.Hom.right η)) ⋯

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskering_obj {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c) (t : LeftLift f g) : (whiskering h).obj t = t.whisker h

def CategoryTheory.Bicategory.LeftLift.whiskerIdCancel {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (s : LeftLift f (CategoryStruct.comp (CategoryStruct.id c) g)) {t : LeftLift f g} (τ : s ⟶ t.whisker (CategoryStruct.id c)) : s.ofIdComp ⟶ 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.

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskerIdCancel_right {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (s : LeftLift f (CategoryStruct.comp (CategoryStruct.id c) g)) {t : LeftLift f g} (τ : s ⟶ t.whisker (CategoryStruct.id c)) : (s.whiskerIdCancel τ).right = CategoryStruct.comp (StructuredArrow.Hom.right τ) (leftUnitor t.lift).hom

def CategoryTheory.Bicategory.LeftLift.whiskerHom {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (i : s ⟶ t) {x : B} (h : x ⟶ c) : s.whisker h ⟶ t.whisker h

Construct a morphism between whiskered lifts.

Equations

• CategoryTheory.Bicategory.LeftLift.whiskerHom i h = CategoryTheory.StructuredArrow.homMk (CategoryTheory.Bicategory.whiskerLeft h (CategoryTheory.StructuredArrow.Hom.right i)) ⋯

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskerHom_right {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (i : s ⟶ t) {x : B} (h : x ⟶ c) : (whiskerHom i h).right = whiskerLeft h (StructuredArrow.Hom.right i)

def CategoryTheory.Bicategory.LeftLift.whiskerIso {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (i : s ≅ t) {x : B} (h : x ⟶ c) : s.whisker h ≅ t.whisker h

Construct an isomorphism between whiskered lifts.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskerIso_inv {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (i : s ≅ t) {x : B} (h : x ⟶ c) : (whiskerIso i h).inv = whiskerHom i.inv h

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskerIso_hom {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : LeftLift f g} (i : s ≅ t) {x : B} (h : x ⟶ c) : (whiskerIso i h).hom = whiskerHom i.hom h

def CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f g) : (t.whisker (CategoryStruct.id c)).ofIdComp ≅ t

The isomorphism between left lifts induced by a left unitor.

Equations

• t.whiskerOfIdCompIsoSelf = CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Bicategory.leftUnitor t.lift) ⋯

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf_hom_right {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f g) : t.whiskerOfIdCompIsoSelf.hom.right = (leftUnitor t.lift).hom

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf_inv_right {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : LeftLift f g) : t.whiskerOfIdCompIsoSelf.inv.right = (leftUnitor t.lift).inv

@[implicit_reducible]

def CategoryTheory.Bicategory.LeftLift.mapIso {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') : LeftLift f g ≌ LeftLift f' g'

Given isomorphisms ef : f ≅ f' and eg : g ≅ g', the induced equivalence between their categories of left lifts.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Bicategory.LeftLift.ofIso {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : LeftLift f g) : LeftLift f' g'

Given isomorphisms ef : f ≅ f' and eg : g ≅ g', and a left lift t : LeftLift f g, the induced left lift t.ofIso : LeftLift f' g'.

Equations

• CategoryTheory.Bicategory.LeftLift.ofIso ef eg t = (CategoryTheory.Bicategory.LeftLift.mapIso ef eg).functor.obj t

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.ofIso_lift {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : LeftLift f g) : (ofIso ef eg t).lift = t.lift

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.ofIso_unit {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : LeftLift f g) : (ofIso ef eg t).unit = CategoryStruct.comp eg.inv (CategoryStruct.comp t.unit (whiskerLeft t.lift ef.hom))

def CategoryTheory.Bicategory.LeftLift.whiskerOfIso {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : LeftLift f g) {x : B} (h : x ⟶ c) : ofIso ef (whiskerLeftIso h eg) (t.whisker h) ≅ (ofIso ef eg t).whisker h

Whiskering commutes with LeftLift.ofIso.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskerOfIso_inv_right {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : LeftLift f g) {x : B} (h : x ⟶ c) : (whiskerOfIso ef eg t h).inv.right = CategoryStruct.id (CategoryStruct.comp h t.lift)

@[simp]

theorem CategoryTheory.Bicategory.LeftLift.whiskerOfIso_hom_right {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : LeftLift f g) {x : B} (h : x ⟶ c) : (whiskerOfIso ef eg t h).hom.right = CategoryStruct.id (CategoryStruct.comp h t.lift)

@[reducible, inline]

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

@[reducible, inline]

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

The extension of g along f.

Equations

• t.extension = CategoryTheory.CostructuredArrow.left t

@[reducible, inline]

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

The 2-morphism filling the triangle diagram.

Equations

• t.counit = CategoryTheory.CostructuredArrow.hom t

@[reducible, inline]

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

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

Equations

• CategoryTheory.Bicategory.RightExtension.mk h counit = CategoryTheory.CostructuredArrow.mk counit

@[reducible, inline]

abbrev CategoryTheory.Bicategory.RightExtension.homMk {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (η : s.extension ⟶ t.extension) (w : CategoryStruct.comp (whiskerLeft f η) t.counit = s.counit := by cat_disch) : 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

• CategoryTheory.Bicategory.RightExtension.homMk η w = CategoryTheory.CostructuredArrow.homMk η w

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.w {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (η : s ⟶ t) : CategoryStruct.comp (whiskerLeft f (CostructuredArrow.Hom.left η)) t.counit = s.counit

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.w_assoc {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (η : s ⟶ t) {Z : a ⟶ c} (h : g ⟶ Z) : CategoryStruct.comp (whiskerLeft f (CostructuredArrow.Hom.left η)) (CategoryStruct.comp t.counit h) = CategoryStruct.comp s.counit h

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

The right extension along the identity.

Equations

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

@[instance_reducible]

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

Equations

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

@[implicit_reducible]

def CategoryTheory.Bicategory.RightExtension.ofCompId {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f (CategoryStruct.comp g (CategoryStruct.id c))) : RightExtension f g

Construct a right extension of g : a ⟶ c from a right extension of g ≫ 𝟙 c.

Equations

• t.ofCompId = CategoryTheory.Bicategory.RightExtension.mk t.extension (CategoryTheory.CategoryStruct.comp t.counit (CategoryTheory.Bicategory.rightUnitor g).hom)

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.ofCompId_left {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f (CategoryStruct.comp g (CategoryStruct.id c))) : t.ofCompId.left = t.extension

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.ofCompId_hom {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f (CategoryStruct.comp g (CategoryStruct.id c))) : t.ofCompId.hom = CategoryStruct.comp t.counit (rightUnitor g).hom

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.ofCompId_right_as {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f (CategoryStruct.comp g (CategoryStruct.id c))) : t.ofCompId.right.as = PUnit.unit

@[implicit_reducible]

def CategoryTheory.Bicategory.RightExtension.whisker {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f g) {x : B} (h : c ⟶ x) : RightExtension f (CategoryStruct.comp g h)

Whisker a 1-morphism to an extension.

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

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whisker_extension {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f g) {x : B} (h : c ⟶ x) : (t.whisker h).extension = CategoryStruct.comp t.extension h

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whisker_counit {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f g) {x : B} (h : c ⟶ x) : (t.whisker h).counit = CategoryStruct.comp (associator f t.extension h).inv (whiskerRight t.counit h)

@[implicit_reducible]

def CategoryTheory.Bicategory.RightExtension.whiskering {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} (h : c ⟶ x) : Functor (RightExtension f g) (RightExtension f (CategoryStruct.comp g h))

Whiskering a 1-morphism is a functor.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskering_obj {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} (h : c ⟶ x) (t : RightExtension f g) : (whiskering h).obj t = t.whisker h

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskering_map {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} (h : c ⟶ x) {X✝ Y✝ : RightExtension f g} (η : X✝ ⟶ Y✝) : (whiskering h).map η = homMk (whiskerRight (CostructuredArrow.Hom.left η) h) ⋯

def CategoryTheory.Bicategory.RightExtension.whiskerIdCancel {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f (CategoryStruct.comp g (CategoryStruct.id c))) {s : RightExtension f g} (τ : s.whisker (CategoryStruct.id c) ⟶ t) : s ⟶ t.ofCompId

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

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskerIdCancel_left {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f (CategoryStruct.comp g (CategoryStruct.id c))) {s : RightExtension f g} (τ : s.whisker (CategoryStruct.id c) ⟶ t) : (t.whiskerIdCancel τ).left = CategoryStruct.comp (rightUnitor s.extension).inv (CostructuredArrow.Hom.left τ)

def CategoryTheory.Bicategory.RightExtension.whiskerHom {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (i : s ⟶ t) {x : B} (h : c ⟶ x) : s.whisker h ⟶ t.whisker h

Construct a morphism between whiskered extensions.

Equations

• CategoryTheory.Bicategory.RightExtension.whiskerHom i h = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CostructuredArrow.Hom.left i) h) ⋯

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskerHom_left {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (i : s ⟶ t) {x : B} (h : c ⟶ x) : (whiskerHom i h).left = whiskerRight (CostructuredArrow.Hom.left i) h

def CategoryTheory.Bicategory.RightExtension.whiskerIso {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (i : s ≅ t) {x : B} (h : c ⟶ x) : s.whisker h ≅ t.whisker h

Construct an isomorphism between whiskered extensions.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskerIso_hom {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (i : s ≅ t) {x : B} (h : c ⟶ x) : (whiskerIso i h).hom = whiskerHom i.hom h

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskerIso_inv {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {s t : RightExtension f g} (i : s ≅ t) {x : B} (h : c ⟶ x) : (whiskerIso i h).inv = whiskerHom i.inv h

def CategoryTheory.Bicategory.RightExtension.whiskerOfCompIdIsoSelf {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f g) : (t.whisker (CategoryStruct.id c)).ofCompId ≅ t

The isomorphism between right extensions induced by a right unitor.

Equations

• t.whiskerOfCompIdIsoSelf = CategoryTheory.CostructuredArrow.isoMk (CategoryTheory.Bicategory.rightUnitor t.extension) ⋯

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskerOfCompIdIsoSelf_hom_left {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f g) : t.whiskerOfCompIdIsoSelf.hom.left = (rightUnitor t.extension).hom

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskerOfCompIdIsoSelf_inv_left {B : Type u} [Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : RightExtension f g) : t.whiskerOfCompIdIsoSelf.inv.left = (rightUnitor t.extension).inv

@[implicit_reducible]

def CategoryTheory.Bicategory.RightExtension.mapIso {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') : RightExtension f g ≌ RightExtension f' g'

Given isomorphisms ef : f ≅ f' and eg : g ≅ g', the induced equivalence between their categories of right extensions.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Bicategory.RightExtension.ofIso {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : RightExtension f g) : RightExtension f' g'

Given isomorphisms ef : f ≅ f' and eg : g ≅ g', and a right extension t : RightExtension f g, the induced right extension t.ofIso : RightExtension f' g'.

Equations

• CategoryTheory.Bicategory.RightExtension.ofIso ef eg t = (CategoryTheory.Bicategory.RightExtension.mapIso ef eg).functor.obj t

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.ofIso_extension {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : RightExtension f g) : (ofIso ef eg t).extension = t.extension

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.ofIso_counit {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : RightExtension f g) : (ofIso ef eg t).counit = CategoryStruct.comp (whiskerRight ef.inv t.extension) (CategoryStruct.comp t.counit eg.hom)

def CategoryTheory.Bicategory.RightExtension.whiskerOfIso {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : RightExtension f g) {x : B} (h : c ⟶ x) : ofIso ef (whiskerRightIso eg h) (t.whisker h) ≅ (ofIso ef eg t).whisker h

Whiskering commutes with RightExtension.ofIso.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskerOfIso_hom_left {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : RightExtension f g) {x : B} (h : c ⟶ x) : (whiskerOfIso ef eg t h).hom.left = CategoryStruct.id (CategoryStruct.comp t.extension h)

@[simp]

theorem CategoryTheory.Bicategory.RightExtension.whiskerOfIso_inv_left {B : Type u} [Bicategory B] {a b c : B} {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g') (t : RightExtension f g) {x : B} (h : c ⟶ x) : (whiskerOfIso ef eg t h).inv.left = CategoryStruct.id (CategoryStruct.comp t.extension h)

@[reducible, inline]

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

@[reducible, inline]

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

The lift of g along f.

Equations

• t.lift = CategoryTheory.CostructuredArrow.left t

@[reducible, inline]

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

The 2-morphism filling the triangle diagram.

Equations

• t.counit = CategoryTheory.CostructuredArrow.hom t

@[reducible, inline]

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

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

Equations

• CategoryTheory.Bicategory.RightLift.mk h counit = CategoryTheory.CostructuredArrow.mk counit

@[reducible, inline]

abbrev CategoryTheory.Bicategory.RightLift.homMk {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (η : s.lift ⟶ t.lift) (w : CategoryStruct.comp (whiskerRight η f) t.counit = s.counit := by cat_disch) : 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

• CategoryTheory.Bicategory.RightLift.homMk η w = CategoryTheory.CostructuredArrow.homMk η w

@[simp]

theorem CategoryTheory.Bicategory.RightLift.w {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (η : s ⟶ t) : CategoryStruct.comp (whiskerRight (CostructuredArrow.Hom.left η) f) t.counit = s.counit

@[simp]

theorem CategoryTheory.Bicategory.RightLift.w_assoc {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (η : s ⟶ t) {Z : c ⟶ a} (h : g ⟶ Z) : CategoryStruct.comp (whiskerRight (CostructuredArrow.Hom.left η) f) (CategoryStruct.comp t.counit h) = CategoryStruct.comp s.counit h

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

The right lift along the identity.

Equations

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

@[instance_reducible]

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

Equations

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

@[implicit_reducible]

def CategoryTheory.Bicategory.RightLift.ofIdComp {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f (CategoryStruct.comp (CategoryStruct.id c) g)) : RightLift f g

Construct a right lift of g : c ⟶ a from a right lift of 𝟙 c ≫ g.

Equations

• t.ofIdComp = CategoryTheory.Bicategory.RightLift.mk t.lift (CategoryTheory.CategoryStruct.comp t.counit (CategoryTheory.Bicategory.leftUnitor g).hom)

@[simp]

theorem CategoryTheory.Bicategory.RightLift.ofIdComp_left {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f (CategoryStruct.comp (CategoryStruct.id c) g)) : t.ofIdComp.left = t.lift

@[simp]

theorem CategoryTheory.Bicategory.RightLift.ofIdComp_right_as {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f (CategoryStruct.comp (CategoryStruct.id c) g)) : t.ofIdComp.right.as = PUnit.unit

@[simp]

theorem CategoryTheory.Bicategory.RightLift.ofIdComp_hom {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f (CategoryStruct.comp (CategoryStruct.id c) g)) : t.ofIdComp.hom = CategoryStruct.comp t.counit (leftUnitor g).hom

@[implicit_reducible]

def CategoryTheory.Bicategory.RightLift.whisker {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f g) {x : B} (h : x ⟶ c) : RightLift f (CategoryStruct.comp h g)

Whisker a 1-morphism to a lift.

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

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whisker_lift {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f g) {x : B} (h : x ⟶ c) : (t.whisker h).lift = CategoryStruct.comp h t.lift

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whisker_counit {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f g) {x : B} (h : x ⟶ c) : (t.whisker h).counit = CategoryStruct.comp (associator h t.lift f).hom (whiskerLeft h t.counit)

@[implicit_reducible]

def CategoryTheory.Bicategory.RightLift.whiskering {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c) : Functor (RightLift f g) (RightLift f (CategoryStruct.comp h g))

Whiskering a 1-morphism is a functor.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskering_map {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c) {X✝ Y✝ : RightLift f g} (η : X✝ ⟶ Y✝) : (whiskering h).map η = homMk (whiskerLeft h (CostructuredArrow.Hom.left η)) ⋯

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskering_obj {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c) (t : RightLift f g) : (whiskering h).obj t = t.whisker h

def CategoryTheory.Bicategory.RightLift.whiskerIdCancel {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f (CategoryStruct.comp (CategoryStruct.id c) g)) {s : RightLift f g} (τ : s.whisker (CategoryStruct.id c) ⟶ t) : s ⟶ t.ofIdComp

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

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskerIdCancel_left {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f (CategoryStruct.comp (CategoryStruct.id c) g)) {s : RightLift f g} (τ : s.whisker (CategoryStruct.id c) ⟶ t) : (t.whiskerIdCancel τ).left = CategoryStruct.comp (leftUnitor s.lift).inv (CostructuredArrow.Hom.left τ)

def CategoryTheory.Bicategory.RightLift.whiskerHom {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (i : s ⟶ t) {x : B} (h : x ⟶ c) : s.whisker h ⟶ t.whisker h

Construct a morphism between whiskered lifts.

Equations

• CategoryTheory.Bicategory.RightLift.whiskerHom i h = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.Bicategory.whiskerLeft h (CategoryTheory.CostructuredArrow.Hom.left i)) ⋯

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskerHom_left {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (i : s ⟶ t) {x : B} (h : x ⟶ c) : (whiskerHom i h).left = whiskerLeft h (CostructuredArrow.Hom.left i)

def CategoryTheory.Bicategory.RightLift.whiskerIso {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (i : s ≅ t) {x : B} (h : x ⟶ c) : s.whisker h ≅ t.whisker h

Construct an isomorphism between whiskered lifts.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskerIso_inv {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (i : s ≅ t) {x : B} (h : x ⟶ c) : (whiskerIso i h).inv = whiskerHom i.inv h

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskerIso_hom {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {s t : RightLift f g} (i : s ≅ t) {x : B} (h : x ⟶ c) : (whiskerIso i h).hom = whiskerHom i.hom h

def CategoryTheory.Bicategory.RightLift.whiskerOfIdCompIsoSelf {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f g) : (t.whisker (CategoryStruct.id c)).ofIdComp ≅ t

The isomorphism between right lifts induced by a left unitor.

Equations

• t.whiskerOfIdCompIsoSelf = CategoryTheory.CostructuredArrow.isoMk (CategoryTheory.Bicategory.leftUnitor t.lift) ⋯

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskerOfIdCompIsoSelf_hom_left {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f g) : t.whiskerOfIdCompIsoSelf.hom.left = (leftUnitor t.lift).hom

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskerOfIdCompIsoSelf_inv_left {B : Type u} [Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : RightLift f g) : t.whiskerOfIdCompIsoSelf.inv.left = (leftUnitor t.lift).inv

@[implicit_reducible]

def CategoryTheory.Bicategory.RightLift.mapIso {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') : RightLift f g ≌ RightLift f' g'

Given isomorphisms ef : f ≅ f' and eg : g ≅ g', the induced equivalence between their categories of right lifts.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Bicategory.RightLift.ofIso {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : RightLift f g) : RightLift f' g'

Given isomorphisms ef : f ≅ f' and eg : g ≅ g', and a right lift t : RightLift f g, the induced right lift t.ofIso : RightLift f' g'.

Equations

• CategoryTheory.Bicategory.RightLift.ofIso ef eg t = (CategoryTheory.Bicategory.RightLift.mapIso ef eg).functor.obj t

@[simp]

theorem CategoryTheory.Bicategory.RightLift.ofIso_lift {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : RightLift f g) : (ofIso ef eg t).lift = t.lift

@[simp]

theorem CategoryTheory.Bicategory.RightLift.ofIso_counit {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : RightLift f g) : (ofIso ef eg t).counit = CategoryStruct.comp (whiskerLeft t.lift ef.inv) (CategoryStruct.comp t.counit eg.hom)

def CategoryTheory.Bicategory.RightLift.whiskerOfIso {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : RightLift f g) {x : B} (h : x ⟶ c) : ofIso ef (whiskerLeftIso h eg) (t.whisker h) ≅ (ofIso ef eg t).whisker h

Whiskering commutes with RightLift.ofIso.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskerOfIso_hom_left {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : RightLift f g) {x : B} (h : x ⟶ c) : (whiskerOfIso ef eg t h).hom.left = CategoryStruct.id (CategoryStruct.comp h t.lift)

@[simp]

theorem CategoryTheory.Bicategory.RightLift.whiskerOfIso_inv_left {B : Type u} [Bicategory B] {a b c : B} {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g') (t : RightLift f g) {x : B} (h : x ⟶ c) : (whiskerOfIso ef eg t h).inv.left = CategoryStruct.id (CategoryStruct.comp h t.lift)