Retracts of 1-morphisms in bicategories

If f : X ⟶ Y and f' : X' ⟶ Y' are 1-morphisms in a bicategory, we introduce a structure RetractArrow₁ f' f expressing that f' is a retract of f, and we show that if f is an equivalence, then f' is also an equivalence.

structure CategoryTheory.Bicategory.RetractArrow₁ {C : Type u} [Bicategory C] {X Y X' Y' : C} (f' : X' ⟶ Y') (f : X ⟶ Y) : Type (max v w)

A structure expressing that a 1-morphism f' : X' ⟶ Y' in a bicategory is a retract of f : X ⟶ Y.

• i₁ : X' ⟶ X

  the inclusion of the source object

• r₁ : X ⟶ X'

  the retraction to the source object

• i₂ : Y' ⟶ Y

  the inclusion of the target object

• r₂ : Y ⟶ Y'

  the retraction to the target object

• id₁ : CategoryStruct.comp self.i₁ self.r₁ ≅ CategoryStruct.id X'

  the source of f' is a retract of the source of f

• id₂ : CategoryStruct.comp self.i₂ self.r₂ ≅ CategoryStruct.id Y'

  the target of f' is a retract of the target of f

• commi : CategoryStruct.comp f' self.i₂ ≅ CategoryStruct.comp self.i₁ f

  compatibility of the inclusions

• commr : CategoryStruct.comp f self.r₂ ≅ CategoryStruct.comp self.r₁ f'

  compatibility of the retractions

• comm : CategoryStruct.comp (whiskerRight self.commi.hom self.r₂) (CategoryStruct.comp (associator self.i₁ f self.r₂).hom (whiskerLeft self.i₁ self.commr.hom)) = CategoryStruct.comp (associator f' self.i₂ self.r₂).hom (CategoryStruct.comp (whiskerLeft f' self.id₂.hom) (CategoryStruct.comp (rightUnitor f').hom (CategoryStruct.comp (leftUnitor f').inv (CategoryStruct.comp (whiskerRight self.id₁.inv f') (associator self.i₁ self.r₁ f').hom))))

theorem CategoryTheory.Bicategory.RetractArrow₁.comm_assoc {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (self : RetractArrow₁ f' f) {Z : X' ⟶ Y'} (h : CategoryStruct.comp self.i₁ (CategoryStruct.comp self.r₁ f') ⟶ Z) : CategoryStruct.comp (whiskerRight self.commi.hom self.r₂) (CategoryStruct.comp (associator self.i₁ f self.r₂).hom (CategoryStruct.comp (whiskerLeft self.i₁ self.commr.hom) h)) = CategoryStruct.comp (associator f' self.i₂ self.r₂).hom (CategoryStruct.comp (whiskerLeft f' self.id₂.hom) (CategoryStruct.comp (rightUnitor f').hom (CategoryStruct.comp (leftUnitor f').inv (CategoryStruct.comp (whiskerRight self.id₁.inv f') (CategoryStruct.comp (associator self.i₁ self.r₁ f').hom h)))))

theorem CategoryTheory.Bicategory.RetractArrow₁.comm' {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) : CategoryStruct.comp (whiskerLeft r.i₁ r.commr.inv) (CategoryStruct.comp (associator r.i₁ f r.r₂).inv (whiskerRight r.commi.inv r.r₂)) = CategoryStruct.comp (associator r.i₁ r.r₁ f').inv (CategoryStruct.comp (whiskerRight r.id₁.hom f') (CategoryStruct.comp (leftUnitor f').hom (CategoryStruct.comp (rightUnitor f').inv (CategoryStruct.comp (whiskerLeft f' r.id₂.inv) (associator f' r.i₂ r.r₂).inv))))

theorem CategoryTheory.Bicategory.RetractArrow₁.comm'_assoc {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {Z : X' ⟶ Y'} (h : CategoryStruct.comp (CategoryStruct.comp f' r.i₂) r.r₂ ⟶ Z) : CategoryStruct.comp (whiskerLeft r.i₁ r.commr.inv) (CategoryStruct.comp (associator r.i₁ f r.r₂).inv (CategoryStruct.comp (whiskerRight r.commi.inv r.r₂) h)) = CategoryStruct.comp (associator r.i₁ r.r₁ f').inv (CategoryStruct.comp (whiskerRight r.id₁.hom f') (CategoryStruct.comp (leftUnitor f').hom (CategoryStruct.comp (rightUnitor f').inv (CategoryStruct.comp (whiskerLeft f' r.id₂.inv) (CategoryStruct.comp (associator f' r.i₂ r.r₂).inv h)))))

@[implicit_reducible]

def CategoryTheory.Bicategory.RetractArrow₁.map {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : RetractArrow₁ (F.map f') (F.map f)

If a 1-morphism is a retract of another, it stays so after the applicaton of a pseudofunctor.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.map_commi {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : (r.map F).commi = (F.mapComp f' r.i₂).symm ≪≫ F.map₂Iso r.commi ≪≫ F.mapComp r.i₁ f

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.map_i₂ {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : (r.map F).i₂ = F.map r.i₂

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.map_r₁ {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : (r.map F).r₁ = F.map r.r₁

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.map_i₁ {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : (r.map F).i₁ = F.map r.i₁

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.map_r₂ {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : (r.map F).r₂ = F.map r.r₂

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.map_commr {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : (r.map F).commr = (F.mapComp f r.r₂).symm ≪≫ F.map₂Iso r.commr ≪≫ F.mapComp r.r₁ f'

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.map_id₂ {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : (r.map F).id₂ = (F.mapComp r.i₂ r.r₂).symm ≪≫ F.map₂Iso r.id₂ ≪≫ F.mapId Y'

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.map_id₁ {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow₁ f' f) {D : Type u_1} [Bicategory D] (F : Pseudofunctor C D) : (r.map F).id₁ = (F.mapComp r.i₁ r.r₁).symm ≪≫ F.map₂Iso r.id₁ ≪≫ F.mapId X'

@[implicit_reducible]

def CategoryTheory.Bicategory.RetractArrow₁.equivalence {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : Equivalence X Y} (r : RetractArrow₁ f' f.hom) : Equivalence X' Y'

In a bicategory, a 1-morphism that is a retract of an equivalence is an equivalence.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.equivalence_unit {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : Equivalence X Y} (r : RetractArrow₁ f' f.hom) : r.equivalence.unit = r.id₁.symm ≪≫ whiskerLeftIso r.i₁ (leftUnitor r.r₁).symm ≪≫ whiskerLeftIso r.i₁ (whiskerRightIso f.unit r.r₁) ≪≫ whiskerLeftIso r.i₁ (associator f.hom f.inv r.r₁) ≪≫ (associator r.i₁ f.hom (CategoryStruct.comp f.inv r.r₁)).symm ≪≫ whiskerRightIso r.commi.symm (CategoryStruct.comp f.inv r.r₁) ≪≫ associator f' r.i₂ (CategoryStruct.comp f.inv r.r₁)

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.equivalence_inv {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : Equivalence X Y} (r : RetractArrow₁ f' f.hom) : r.equivalence.inv = CategoryStruct.comp r.i₂ (CategoryStruct.comp f.inv r.r₁)

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.equivalence_counit {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : Equivalence X Y} (r : RetractArrow₁ f' f.hom) : r.equivalence.counit = associator r.i₂ (CategoryStruct.comp f.inv r.r₁) f' ≪≫ whiskerLeftIso r.i₂ (associator f.inv r.r₁ f' ≪≫ whiskerLeftIso f.inv r.commr.symm ≪≫ (associator f.inv f.hom r.r₂).symm) ≪≫ whiskerLeftIso r.i₂ (whiskerRightIso f.counit r.r₂) ≪≫ whiskerLeftIso r.i₂ (leftUnitor r.r₂) ≪≫ r.id₂

@[simp]

theorem CategoryTheory.Bicategory.RetractArrow₁.equivalence_hom {C : Type u} [Bicategory C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : Equivalence X Y} (r : RetractArrow₁ f' f.hom) : r.equivalence.hom = f'

@[implicit_reducible]

def CategoryTheory.RetractArrow.toLoc {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : Bicategory.RetractArrow₁ f'.toLoc f.toLoc

A retract of morphisms in a category C induces a retract of 1-morphisms in the bicategory LocallyDiscrete C.

Equations

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

@[simp]

theorem CategoryTheory.RetractArrow.toLoc_commr {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : r.toLoc.commr = eqToIso ⋯

@[simp]

theorem CategoryTheory.RetractArrow.toLoc_i₁ {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : r.toLoc.i₁ = (Arrow.Hom.left r.i).toLoc

@[simp]

theorem CategoryTheory.RetractArrow.toLoc_r₁ {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : r.toLoc.r₁ = (Arrow.Hom.left r.r).toLoc

@[simp]

theorem CategoryTheory.RetractArrow.toLoc_r₂ {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : r.toLoc.r₂ = (Arrow.Hom.right r.r).toLoc

@[simp]

theorem CategoryTheory.RetractArrow.toLoc_commi {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : r.toLoc.commi = eqToIso ⋯

@[simp]

theorem CategoryTheory.RetractArrow.toLoc_id₁ {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : r.toLoc.id₁ = eqToIso ⋯

@[simp]

theorem CategoryTheory.RetractArrow.toLoc_id₂ {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : r.toLoc.id₂ = eqToIso ⋯

@[simp]

theorem CategoryTheory.RetractArrow.toLoc_i₂ {C : Type u_1} [Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : RetractArrow f' f) : r.toLoc.i₂ = (Arrow.Hom.right r.i).toLoc