Free bicategories

We define the free bicategory over a quiver. In this bicategory, the 1-morphisms are freely generated by the arrows in the quiver, and the 2-morphisms are freely generated by the formal identities, the formal unitors, and the formal associators modulo the relation derived from the axioms of a bicategory.

Main definitions

• FreeBicategory B: the free bicategory over a quiver B.
• FreeBicategory.lift F: the pseudofunctor from FreeBicategory B to C associated with a prefunctor F from B to C.

def CategoryTheory.FreeBicategory (B : Type u) : Type u

Free bicategory over a quiver. Its objects are the same as those in the underlying quiver.

instance CategoryTheory.instInhabitedFreeBicategory (B : Type u) [Inhabited B] : Inhabited (FreeBicategory B)

inductive CategoryTheory.FreeBicategory.Hom {B : Type u} [Quiver B] : B → B → Type (max u v)

1-morphisms in the free bicategory.

• of {B : Type u} [Quiver B] {a b : B} (f : a ⟶ b) : Hom a b
• id {B : Type u} [Quiver B] (a : B) : Hom a a
• comp {B : Type u} [Quiver B] {a b c : B} (f : Hom a b) (g : Hom b c) : Hom a c

instance CategoryTheory.FreeBicategory.instInhabitedHomOfHom {B : Type u} [Quiver B] (a b : B) [Inhabited (a ⟶ b)] : Inhabited (Hom a b)

instance CategoryTheory.FreeBicategory.quiver {B : Type u} [Quiver B] : Quiver (FreeBicategory B)

instance CategoryTheory.FreeBicategory.categoryStruct {B : Type u} [Quiver B] : CategoryStruct.{max u v, u} (FreeBicategory B)

inductive CategoryTheory.FreeBicategory.Hom₂ {B : Type u} [Quiver B] {a b : FreeBicategory B} : (a ⟶ b) → (a ⟶ b) → Type (max u v)

Representatives of 2-morphisms in the free bicategory.

• id {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Hom₂ f f
• vcomp {B : Type u} [Quiver B] {a b : FreeBicategory B} {f g h : a ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h) : Hom₂ f h
• whisker_left {B : Type u} [Quiver B] {a b c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h) : Hom₂ (CategoryStruct.comp f g) (CategoryStruct.comp f h)
• whisker_right {B : Type u} [Quiver B] {a b c : FreeBicategory B} {f g : a ⟶ b} (h : b ⟶ c) (η : Hom₂ f g) : Hom₂ (Hom.comp f h) (Hom.comp g h)
• associator {B : Type u} [Quiver B] {a b c d : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : Hom₂ (CategoryStruct.comp (CategoryStruct.comp f g) h) (CategoryStruct.comp f (CategoryStruct.comp g h))
• associator_inv {B : Type u} [Quiver B] {a b c d : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : Hom₂ (CategoryStruct.comp f (CategoryStruct.comp g h)) (CategoryStruct.comp (CategoryStruct.comp f g) h)
• right_unitor {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Hom₂ (CategoryStruct.comp f (CategoryStruct.id b)) f
• right_unitor_inv {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Hom₂ f (CategoryStruct.comp f (CategoryStruct.id b))
• left_unitor {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Hom₂ (CategoryStruct.comp (CategoryStruct.id a) f) f
• left_unitor_inv {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Hom₂ f (CategoryStruct.comp (CategoryStruct.id a) f)

inductive CategoryTheory.FreeBicategory.Rel {B : Type u} [Quiver B] {a b : FreeBicategory B} {f g : a ⟶ b} : Hom₂ f g → Hom₂ f g → Prop

Relations between 2-morphisms in the free bicategory.

• vcomp_right {B : Type u} [Quiver B] {a b : B} {f g h : Hom a b} (η : Hom₂ f g) (θ₁ θ₂ : Hom₂ g h) : Rel θ₁ θ₂ → Rel (η.vcomp θ₁) (η.vcomp θ₂)
• vcomp_left {B : Type u} [Quiver B] {a b : B} {f g h : Hom a b} (η₁ η₂ : Hom₂ f g) (θ : Hom₂ g h) : Rel η₁ η₂ → Rel (η₁.vcomp θ) (η₂.vcomp θ)
• id_comp {B : Type u} [Quiver B] {a b : B} {f g : Hom a b} (η : Hom₂ f g) : Rel ((Hom₂.id f).vcomp η) η
• comp_id {B : Type u} [Quiver B] {a b : B} {f g : Hom a b} (η : Hom₂ f g) : Rel (η.vcomp (Hom₂.id g)) η
• assoc {B : Type u} [Quiver B] {a b : B} {f g h i : Hom a b} (η : Hom₂ f g) (θ : Hom₂ g h) (ι : Hom₂ h i) : Rel ((η.vcomp θ).vcomp ι) (η.vcomp (θ.vcomp ι))
• whisker_left {B : Type u} [Quiver B] {a b c : B} (f : Hom a b) (g h : Hom b c) (η η' : Hom₂ g h) : Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')
• whisker_left_id {B : Type u} [Quiver B] {a b c : B} (f : Hom a b) (g : Hom b c) : Rel (Hom₂.whisker_left f (Hom₂.id g)) (Hom₂.id (f.comp g))
• whisker_left_comp {B : Type u} [Quiver B] {a b c : B} (f : Hom a b) {g h i : Hom b c} (η : Hom₂ g h) (θ : Hom₂ h i) : Rel (Hom₂.whisker_left f (η.vcomp θ)) ((Hom₂.whisker_left f η).vcomp (Hom₂.whisker_left f θ))
• id_whisker_left {B : Type u} [Quiver B] {a b : B} {f g : Hom a b} (η : Hom₂ f g) : Rel (Hom₂.whisker_left (Hom.id a) η) ((Hom₂.left_unitor f).vcomp (η.vcomp (Hom₂.left_unitor_inv g)))
• comp_whisker_left {B : Type u} [Quiver B] {a b c d : B} (f : Hom a b) (g : Hom b c) {h h' : Hom c d} (η : Hom₂ h h') : Rel (Hom₂.whisker_left (f.comp g) η) ((Hom₂.associator f g h).vcomp ((Hom₂.whisker_left f (Hom₂.whisker_left g η)).vcomp (Hom₂.associator_inv f g h')))
• whisker_right {B : Type u} [Quiver B] {a b c : B} (f g : Hom a b) (h : Hom b c) (η η' : Hom₂ f g) : Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')
• id_whisker_right {B : Type u} [Quiver B] {a b c : B} (f : Hom a b) (g : Hom b c) : Rel (Hom₂.whisker_right g (Hom₂.id f)) (Hom₂.id (f.comp g))
• comp_whisker_right {B : Type u} [Quiver B] {a b c : B} {f g h : Hom a b} (i : Hom b c) (η : Hom₂ f g) (θ : Hom₂ g h) : Rel (Hom₂.whisker_right i (η.vcomp θ)) ((Hom₂.whisker_right i η).vcomp (Hom₂.whisker_right i θ))
• whisker_right_id {B : Type u} [Quiver B] {a b : B} {f g : Hom a b} (η : Hom₂ f g) : Rel (Hom₂.whisker_right (Hom.id b) η) ((Hom₂.right_unitor f).vcomp (η.vcomp (Hom₂.right_unitor_inv g)))
• whisker_right_comp {B : Type u} [Quiver B] {a b c d : B} {f f' : Hom a b} (g : Hom b c) (h : Hom c d) (η : Hom₂ f f') : Rel (Hom₂.whisker_right (g.comp h) η) ((Hom₂.associator_inv f g h).vcomp ((Hom₂.whisker_right h (Hom₂.whisker_right g η)).vcomp (Hom₂.associator f' g h)))
• whisker_assoc {B : Type u} [Quiver B] {a b c d : B} (f : Hom a b) {g g' : Hom b c} (η : Hom₂ g g') (h : Hom c d) : Rel (Hom₂.whisker_right h (Hom₂.whisker_left f η)) ((Hom₂.associator f g h).vcomp ((Hom₂.whisker_left f (Hom₂.whisker_right h η)).vcomp (Hom₂.associator_inv f g' h)))
• whisker_exchange {B : Type u} [Quiver B] {a b c : B} {f g : Hom a b} {h i : Hom b c} (η : Hom₂ f g) (θ : Hom₂ h i) : Rel ((Hom₂.whisker_left f θ).vcomp (Hom₂.whisker_right i η)) ((Hom₂.whisker_right h η).vcomp (Hom₂.whisker_left g θ))
• associator_hom_inv {B : Type u} [Quiver B] {a b c d : B} (f : Hom a b) (g : Hom b c) (h : Hom c d) : Rel ((Hom₂.associator f g h).vcomp (Hom₂.associator_inv f g h)) (Hom₂.id ((f.comp g).comp h))
• associator_inv_hom {B : Type u} [Quiver B] {a b c d : B} (f : Hom a b) (g : Hom b c) (h : Hom c d) : Rel ((Hom₂.associator_inv f g h).vcomp (Hom₂.associator f g h)) (Hom₂.id (f.comp (g.comp h)))
• left_unitor_hom_inv {B : Type u} [Quiver B] {a b : B} (f : Hom a b) : Rel ((Hom₂.left_unitor f).vcomp (Hom₂.left_unitor_inv f)) (Hom₂.id ((Hom.id a).comp f))
• left_unitor_inv_hom {B : Type u} [Quiver B] {a b : B} (f : Hom a b) : Rel ((Hom₂.left_unitor_inv f).vcomp (Hom₂.left_unitor f)) (Hom₂.id f)
• right_unitor_hom_inv {B : Type u} [Quiver B] {a b : B} (f : Hom a b) : Rel ((Hom₂.right_unitor f).vcomp (Hom₂.right_unitor_inv f)) (Hom₂.id (f.comp (Hom.id b)))
• right_unitor_inv_hom {B : Type u} [Quiver B] {a b : B} (f : Hom a b) : Rel ((Hom₂.right_unitor_inv f).vcomp (Hom₂.right_unitor f)) (Hom₂.id f)
• pentagon {B : Type u} [Quiver B] {a b c d e : B} (f : Hom a b) (g : Hom b c) (h : Hom c d) (i : Hom d e) : Rel ((Hom₂.whisker_right i (Hom₂.associator f g h)).vcomp ((Hom₂.associator f (g.comp h) i).vcomp (Hom₂.whisker_left f (Hom₂.associator g h i)))) ((Hom₂.associator (f.comp g) h i).vcomp (Hom₂.associator f g (h.comp i)))
• triangle {B : Type u} [Quiver B] {a b c : B} (f : Hom a b) (g : Hom b c) : Rel ((Hom₂.associator f (Hom.id b) g).vcomp (Hom₂.whisker_left f (Hom₂.left_unitor g))) (Hom₂.whisker_right g (Hom₂.right_unitor f))

instance CategoryTheory.FreeBicategory.homCategory {B : Type u} [Quiver B] (a b : FreeBicategory B) : Category.{max u v, max u v} (a ⟶ b)

instance CategoryTheory.FreeBicategory.bicategory {B : Type u} [Quiver B] : Bicategory (FreeBicategory B)

Bicategory structure on the free bicategory.

@[reducible, inline]

abbrev CategoryTheory.FreeBicategory.Hom₂.mk {B : Type u} [Quiver B] {a b : FreeBicategory B} {f g : a ⟶ b} (η : Hom₂ f g) : f ⟶ g

Hom₂.mk η is an abbreviation for Quot.mk Rel η.

@[simp]

theorem CategoryTheory.FreeBicategory.mk_vcomp {B : Type u} [Quiver B] {a b : FreeBicategory B} {f g h : a ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h) : (η.vcomp θ).mk = CategoryStruct.comp η.mk θ.mk

@[simp]

theorem CategoryTheory.FreeBicategory.mk_whisker_left {B : Type u} [Quiver B] {a b c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h) : (Hom₂.whisker_left f η).mk = Bicategory.whiskerLeft f η.mk

@[simp]

theorem CategoryTheory.FreeBicategory.mk_whisker_right {B : Type u} [Quiver B] {a b c : FreeBicategory B} {f g : a ⟶ b} (η : Hom₂ f g) (h : b ⟶ c) : (Hom₂.whisker_right h η).mk = Bicategory.whiskerRight η.mk h

theorem CategoryTheory.FreeBicategory.id_def {B : Type u} [Quiver B] {a : FreeBicategory B} : Hom.id a = CategoryStruct.id a

theorem CategoryTheory.FreeBicategory.comp_def {B : Type u} [Quiver B] {a b c : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) : Hom.comp f g = CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.FreeBicategory.mk_id {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Quot.mk Rel (Hom₂.id f) = CategoryStruct.id f

@[simp]

theorem CategoryTheory.FreeBicategory.mk_associator_hom {B : Type u} [Quiver B] {a b c d : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : Quot.mk Rel (Hom₂.associator f g h) = (Bicategory.associator f g h).hom

@[simp]

theorem CategoryTheory.FreeBicategory.mk_associator_inv {B : Type u} [Quiver B] {a b c d : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : Quot.mk Rel (Hom₂.associator_inv f g h) = (Bicategory.associator f g h).inv

@[simp]

theorem CategoryTheory.FreeBicategory.mk_left_unitor_hom {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Quot.mk Rel (Hom₂.left_unitor f) = (Bicategory.leftUnitor f).hom

@[simp]

theorem CategoryTheory.FreeBicategory.mk_left_unitor_inv {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Quot.mk Rel (Hom₂.left_unitor_inv f) = (Bicategory.leftUnitor f).inv

@[simp]

theorem CategoryTheory.FreeBicategory.mk_right_unitor_hom {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Quot.mk Rel (Hom₂.right_unitor f) = (Bicategory.rightUnitor f).hom

@[simp]

theorem CategoryTheory.FreeBicategory.mk_right_unitor_inv {B : Type u} [Quiver B] {a b : FreeBicategory B} (f : a ⟶ b) : Quot.mk Rel (Hom₂.right_unitor_inv f) = (Bicategory.rightUnitor f).inv

def CategoryTheory.FreeBicategory.of {B : Type u} [Quiver B] : B ⥤q FreeBicategory B

Canonical prefunctor from B to free_bicategory B.

@[simp]

theorem CategoryTheory.FreeBicategory.of_map {B : Type u} [Quiver B] (x✝ x✝¹ : B) (f : x✝ ⟶ x✝¹) : of.map f = Hom.of f

@[simp]

theorem CategoryTheory.FreeBicategory.of_obj {B : Type u} [Quiver B] (a : B) : of.obj a = id a

def CategoryTheory.FreeBicategory.liftHom {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) {a b : FreeBicategory B} : (a ⟶ b) → (F.obj a ⟶ F.obj b)

Auxiliary definition for lift.

@[simp]

theorem CategoryTheory.FreeBicategory.liftHom_id {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) (a : FreeBicategory B) : liftHom F (CategoryStruct.id a) = CategoryStruct.id (F.obj a)

@[simp]

theorem CategoryTheory.FreeBicategory.liftHom_comp {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) {a b c : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) : liftHom F (CategoryStruct.comp f g) = CategoryStruct.comp (liftHom F f) (liftHom F g)

def CategoryTheory.FreeBicategory.liftHom₂ {B : Type u₁} [Quiver B] {C : Type u₂} [Bicategory C] (F : B ⥤q C) {a b : FreeBicategory B} {f g : a ⟶ b} : Hom₂ f g → (liftHom F f ⟶ liftHom F g)

Auxiliary definition for lift.

theorem CategoryTheory.FreeBicategory.liftHom₂_congr {B : Type u₁} [Quiver B] {C : Type u₂} [Bicategory C] (F : B ⥤q C) {a b : FreeBicategory B} {f g : a ⟶ b} {η θ : Hom₂ f g} (H : Rel η θ) : liftHom₂ F η = liftHom₂ F θ

def CategoryTheory.FreeBicategory.lift {B : Type u₁} [Quiver B] {C : Type u₂} [Bicategory C] (F : B ⥤q C) : Pseudofunctor (FreeBicategory B) C

A prefunctor from a quiver B to a bicategory C can be lifted to a pseudofunctor from free_bicategory B to C.

@[simp]

theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj {B : Type u₁} [Quiver B] {C : Type u₂} [Bicategory C] (F : B ⥤q C) (a✝ : B) : (lift F).obj a✝ = F.obj a✝

@[simp]

theorem CategoryTheory.FreeBicategory.lift_mapId {B : Type u₁} [Quiver B] {C : Type u₂} [Bicategory C] (F : B ⥤q C) (x✝ : FreeBicategory B) : (lift F).mapId x✝ = Iso.refl (liftHom F (CategoryStruct.id x✝))

@[simp]

theorem CategoryTheory.FreeBicategory.lift_mapComp {B : Type u₁} [Quiver B] {C : Type u₂} [Bicategory C] (F : B ⥤q C) {a✝ b✝ c✝ : FreeBicategory B} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (lift F).mapComp x✝ x✝¹ = Iso.refl (liftHom F (CategoryStruct.comp x✝ x✝¹))

@[simp]

theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ {B : Type u₁} [Quiver B] {C : Type u₂} [Bicategory C] (F : B ⥤q C) {a✝ b✝ : FreeBicategory B} {f✝ g✝ : a✝ ⟶ b✝} (a : Quot Rel) : (lift F).map₂ a = Quot.lift (liftHom₂ F) ⋯ a

@[simp]

theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map {B : Type u₁} [Quiver B] {C : Type u₂} [Bicategory C] (F : B ⥤q C) {X✝ Y✝ : FreeBicategory B} (a✝ : X✝ ⟶ Y✝) : (lift F).map a✝ = liftHom F a✝