mathlib3 documentation

category_theory.bicategory.free

Free bicategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
def category_theory.free_bicategory (B : Type u) :
Type u

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

Equations
Instances for category_theory.free_bicategory
source
@[protected, instance]
def category_theory.free_bicategory.inhabited (B : Type u) [inhabited B] :
inhabited (category_theory.free_bicategory B)
Equations
source
inductive category_theory.free_bicategory.hom {B : Type u} [quiver B] :
B → B → Type (max u v)

1-morphisms in the free bicategory.

Instances for category_theory.free_bicategory.hom
source
@[protected, instance]
def category_theory.free_bicategory.hom.inhabited {B : Type u} [quiver B] (a b : B) [inhabited (a ⟶ b)] :
inhabited (category_theory.free_bicategory.hom a b)
Equations
source
@[nolint]
inductive category_theory.free_bicategory.hom₂ {B : Type u} [quiver B] {a b : B} :
category_theory.free_bicategory.hom a b → category_theory.free_bicategory.hom a b → Type (max u v)

Representatives of 2-morphisms in the free bicategory.

Instances for category_theory.free_bicategory.hom₂
  • category_theory.free_bicategory.hom₂.has_sizeof_inst
source
inductive category_theory.free_bicategory.rel {B : Type u} [quiver B] {a b : B} {f g : category_theory.free_bicategory.hom a b} :
category_theory.free_bicategory.hom₂ f g → category_theory.free_bicategory.hom₂ f g → Prop

Relations between 2-morphisms in the free bicategory.

source
@[protected, instance]
def category_theory.free_bicategory.hom_category {B : Type u} [quiver B] (a b : B) :
category_theory.category (category_theory.free_bicategory.hom a b)
Equations
source
@[protected, instance]
def category_theory.free_bicategory.bicategory {B : Type u} [quiver B] :
category_theory.bicategory (category_theory.free_bicategory B)

Bicategory structure on the free bicategory.

Equations
source
@[simp]
theorem category_theory.free_bicategory.mk_vcomp {B : Type u} [quiver B] {a b : category_theory.free_bicategory B} {f g h : a ⟶ b} (η : category_theory.free_bicategory.hom₂ f g) (θ : category_theory.free_bicategory.hom₂ g h) :
quot.mk category_theory.free_bicategory.rel (η.vcomp θ) = quot.mk category_theory.free_bicategory.rel η ≫ quot.mk category_theory.free_bicategory.rel θ
source
@[simp]
theorem category_theory.free_bicategory.mk_whisker_left {B : Type u} [quiver B] {a b c : category_theory.free_bicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : category_theory.free_bicategory.hom₂ g h) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.whisker_left f η) = category_theory.bicategory.whisker_left f (quot.mk category_theory.free_bicategory.rel η)
source
@[simp]
theorem category_theory.free_bicategory.mk_whisker_right {B : Type u} [quiver B] {a b c : category_theory.free_bicategory B} {f g : a ⟶ b} (η : category_theory.free_bicategory.hom₂ f g) (h : b ⟶ c) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.whisker_right h η) = category_theory.bicategory.whisker_right (quot.mk category_theory.free_bicategory.rel η) h
source
theorem category_theory.free_bicategory.id_def {B : Type u} [quiver B] {a : category_theory.free_bicategory B} :
category_theory.free_bicategory.hom.id a = 𝟙 a
source
theorem category_theory.free_bicategory.comp_def {B : Type u} [quiver B] {a b c : category_theory.free_bicategory B} (f : a ⟶ b) (g : b ⟶ c) :
category_theory.free_bicategory.hom.comp f g = f ≫ g
source
@[simp]
theorem category_theory.free_bicategory.mk_id {B : Type u} [quiver B] {a b : category_theory.free_bicategory B} (f : a ⟶ b) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.id f) = 𝟙 f
source
@[simp]
theorem category_theory.free_bicategory.mk_associator_hom {B : Type u} [quiver B] {a b c d : category_theory.free_bicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.associator f g h) = (category_theory.bicategory.associator f g h).hom
source
@[simp]
theorem category_theory.free_bicategory.mk_associator_inv {B : Type u} [quiver B] {a b c d : category_theory.free_bicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.associator_inv f g h) = (category_theory.bicategory.associator f g h).inv
source
@[simp]
theorem category_theory.free_bicategory.mk_left_unitor_hom {B : Type u} [quiver B] {a b : category_theory.free_bicategory B} (f : a ⟶ b) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.left_unitor f) = (category_theory.bicategory.left_unitor f).hom
source
@[simp]
theorem category_theory.free_bicategory.mk_left_unitor_inv {B : Type u} [quiver B] {a b : category_theory.free_bicategory B} (f : a ⟶ b) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.left_unitor_inv f) = (category_theory.bicategory.left_unitor f).inv
source
@[simp]
theorem category_theory.free_bicategory.mk_right_unitor_hom {B : Type u} [quiver B] {a b : category_theory.free_bicategory B} (f : a ⟶ b) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.right_unitor f) = (category_theory.bicategory.right_unitor f).hom
source
@[simp]
theorem category_theory.free_bicategory.mk_right_unitor_inv {B : Type u} [quiver B] {a b : category_theory.free_bicategory B} (f : a ⟶ b) :
quot.mk category_theory.free_bicategory.rel (category_theory.free_bicategory.hom₂.right_unitor_inv f) = (category_theory.bicategory.right_unitor f).inv
source
@[simp]
theorem category_theory.free_bicategory.of_obj {B : Type u} [quiver B] (a : B) :
category_theory.free_bicategory.of.obj a = id a
source
@[simp]
theorem category_theory.free_bicategory.of_map {B : Type u} [quiver B] (a b : B) (f : a ⟶ b) :
category_theory.free_bicategory.of.map f = category_theory.free_bicategory.hom.of f
source
def category_theory.free_bicategory.of {B : Type u} [quiver B] :
B ⥤q category_theory.free_bicategory B

Canonical prefunctor from B to free_bicategory B.

Equations
source
@[simp]
def category_theory.free_bicategory.lift_hom {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.category_struct C] (F : B ⥤q C) {a b : B} :
category_theory.free_bicategory.hom a b → (F.obj a ⟶ F.obj b)

Auxiliary definition for lift.

Equations
source
@[simp]
theorem category_theory.free_bicategory.lift_hom_id {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.category_struct C] (F : B ⥤q C) (a : category_theory.free_bicategory B) :
category_theory.free_bicategory.lift_hom F (𝟙 a) = 𝟙 (F.obj a)
source
@[simp]
theorem category_theory.free_bicategory.lift_hom_comp {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.category_struct C] (F : B ⥤q C) {a b c : category_theory.free_bicategory B} (f : a ⟶ b) (g : b ⟶ c) :
category_theory.free_bicategory.lift_hom F (f ≫ g) = category_theory.free_bicategory.lift_hom F f ≫ category_theory.free_bicategory.lift_hom F g
source
@[simp]
def category_theory.free_bicategory.lift_hom₂ {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) {a b : B} {f g : category_theory.free_bicategory.hom a b} :
category_theory.free_bicategory.hom₂ f g → (category_theory.free_bicategory.lift_hom F f ⟶ category_theory.free_bicategory.lift_hom F g)

Auxiliary definition for lift.

Equations
source
theorem category_theory.free_bicategory.lift_hom₂_congr {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) {a b : B} {f g : category_theory.free_bicategory.hom a b} {η θ : category_theory.free_bicategory.hom₂ f g} (H : category_theory.free_bicategory.rel η θ) :
category_theory.free_bicategory.lift_hom₂ F η = category_theory.free_bicategory.lift_hom₂ F θ
source
@[simp]
theorem category_theory.free_bicategory.lift_map {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) (a b : category_theory.free_bicategory B) (ᾰ : category_theory.free_bicategory.hom a b) :
(category_theory.free_bicategory.lift F).map ᾰ = category_theory.free_bicategory.lift_hom F ᾰ
source
@[simp]
theorem category_theory.free_bicategory.lift_obj {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) (ᾰ : B) :
(category_theory.free_bicategory.lift F).obj ᾰ = F.obj ᾰ
source
@[simp]
theorem category_theory.free_bicategory.lift_map₂ {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) (a b : category_theory.free_bicategory B) (f g : a ⟶ b) (a_1 : quot (λ (η θ : category_theory.free_bicategory.hom₂ f g), category_theory.free_bicategory.rel η θ)) :
(category_theory.free_bicategory.lift F).map₂ a_1 = quot.lift (category_theory.free_bicategory.lift_hom₂ F) _ a_1
source
@[simp]
theorem category_theory.free_bicategory.lift_map_comp {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) (a b c : category_theory.free_bicategory B) (f : a ⟶ b) (g : b ⟶ c) :
(category_theory.free_bicategory.lift F).map_comp f g = category_theory.iso.refl (category_theory.free_bicategory.lift_hom F (f ≫ g))
source
def category_theory.free_bicategory.lift {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) :
category_theory.pseudofunctor (category_theory.free_bicategory B) C

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

Equations
source
@[simp]
theorem category_theory.free_bicategory.lift_map_id {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) (a : category_theory.free_bicategory B) :
(category_theory.free_bicategory.lift F).map_id a = category_theory.iso.refl (category_theory.free_bicategory.lift_hom F (𝟙 a))