Documentation

Mathlib.CategoryTheory.Bicategory.Free

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 #

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

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

Equations
Instances For
    source
    instance CategoryTheory.instForAllInhabitedFreeBicategory (B : Type u) [Inhabited B] :
    Inhabited (CategoryTheory.FreeBicategory B)
    Equations
    source
    inductive CategoryTheory.FreeBicategory.Hom {B : Type u} [Quiver B] :
    B → B → Type (max u v)

    1-morphisms in the free bicategory.

    Instances For
      source
      instance CategoryTheory.FreeBicategory.instInhabitedHom {B : Type u} [Quiver B] (a : B) (b : B) [Inhabited (a ⟶ b)] :
      Inhabited (CategoryTheory.FreeBicategory.Hom a b)
      Equations
      source
      instance CategoryTheory.FreeBicategory.quiver {B : Type u} [Quiver B] :
      Quiver (CategoryTheory.FreeBicategory B)
      Equations
      source
      instance CategoryTheory.FreeBicategory.categoryStruct {B : Type u} [Quiver B] :
      CategoryTheory.CategoryStruct.{max u v, u} (CategoryTheory.FreeBicategory B)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      inductive CategoryTheory.FreeBicategory.Hom₂ {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} :
      (a ⟶ b) → (a ⟶ b) → Type (max u v)

      Representatives of 2-morphisms in the free bicategory.

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

        Relations between 2-morphisms in the free bicategory.

        Instances For
          source
          instance CategoryTheory.FreeBicategory.homCategory {B : Type u} [Quiver B] (a : CategoryTheory.FreeBicategory B) (b : CategoryTheory.FreeBicategory B) :
          CategoryTheory.Category.{max u v, max u v} (a ⟶ b)
          Equations
          source
          instance CategoryTheory.FreeBicategory.bicategory {B : Type u} [Quiver B] :
          CategoryTheory.Bicategory (CategoryTheory.FreeBicategory B)

          Bicategory structure on the free bicategory.

          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[inline, reducible]
          abbrev CategoryTheory.FreeBicategory.Hom₂.mk {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {f : a ⟶ b} {g : a ⟶ b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) :
          f ⟶ g
          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_vcomp {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h) :
            CategoryTheory.FreeBicategory.Hom₂.mk (CategoryTheory.FreeBicategory.Hom₂.vcomp η θ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.Hom₂.mk η) (CategoryTheory.FreeBicategory.Hom₂.mk θ)
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_whisker_left {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : CategoryTheory.FreeBicategory.Hom₂ g h) :
            CategoryTheory.FreeBicategory.Hom₂.mk (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η) = CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.FreeBicategory.Hom₂.mk η)
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_whisker_right {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {c : CategoryTheory.FreeBicategory B} {f : a ⟶ b} {g : a ⟶ b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) (h : b ⟶ c) :
            CategoryTheory.FreeBicategory.Hom₂.mk (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.FreeBicategory.Hom₂.mk η) h
            source
            theorem CategoryTheory.FreeBicategory.comp_def {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) :
            CategoryTheory.FreeBicategory.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_id {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :
            Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.id f) = CategoryTheory.CategoryStruct.id f
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_associator_hom {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {c : CategoryTheory.FreeBicategory B} {d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
            Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator f g h) = (CategoryTheory.Bicategory.associator f g h).hom
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_associator_inv {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {c : CategoryTheory.FreeBicategory B} {d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
            Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h) = (CategoryTheory.Bicategory.associator f g h).inv
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_left_unitor_hom {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :
            Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.left_unitor f) = (CategoryTheory.Bicategory.leftUnitor f).hom
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_left_unitor_inv {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :
            Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f) = (CategoryTheory.Bicategory.leftUnitor f).inv
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_right_unitor_hom {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :
            Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.right_unitor f) = (CategoryTheory.Bicategory.rightUnitor f).hom
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.mk_right_unitor_inv {B : Type u} [Quiver B] {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :
            Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f) = (CategoryTheory.Bicategory.rightUnitor f).inv
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.of_map {B : Type u} [Quiver B] :
            ∀ (x x_1 : B) (f : x ⟶ x_1), CategoryTheory.FreeBicategory.of.map f = CategoryTheory.FreeBicategory.Hom.of f
            source
            @[simp]
            theorem CategoryTheory.FreeBicategory.of_obj {B : Type u} [Quiver B] (a : B) :
            CategoryTheory.FreeBicategory.of.obj a = id a
            source
            def CategoryTheory.FreeBicategory.of {B : Type u} [Quiver B] :
            B ⥤q CategoryTheory.FreeBicategory B

            Canonical prefunctor from B to free_bicategory B.

            Equations
            • CategoryTheory.FreeBicategory.of = { obj := id, map := fun (x x_1 : B) => CategoryTheory.FreeBicategory.Hom.of }
            Instances For
              source
              def CategoryTheory.FreeBicategory.liftHom {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} :
              (a ⟶ b) → (F.obj a ⟶ F.obj b)

              Auxiliary definition for lift.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.FreeBicategory.liftHom_id {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) (a : CategoryTheory.FreeBicategory B) :
                CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.id a) = CategoryTheory.CategoryStruct.id (F.obj a)
                source
                @[simp]
                theorem CategoryTheory.FreeBicategory.liftHom_comp {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) :
                CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.liftHom F f) (CategoryTheory.FreeBicategory.liftHom F g)
                source
                def CategoryTheory.FreeBicategory.liftHom₂ {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {f : a ⟶ b} {g : a ⟶ b} :
                CategoryTheory.FreeBicategory.Hom₂ f g → (CategoryTheory.FreeBicategory.liftHom F f ⟶ CategoryTheory.FreeBicategory.liftHom F g)

                Auxiliary definition for lift.

                Instances For
                  source
                  theorem CategoryTheory.FreeBicategory.liftHom₂_congr {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) {a : CategoryTheory.FreeBicategory B} {b : CategoryTheory.FreeBicategory B} {f : a ⟶ b} {g : a ⟶ b} {η : CategoryTheory.FreeBicategory.Hom₂ f g} {θ : CategoryTheory.FreeBicategory.Hom₂ f g} (H : CategoryTheory.FreeBicategory.Rel η θ) :
                  CategoryTheory.FreeBicategory.liftHom₂ F η = CategoryTheory.FreeBicategory.liftHom₂ F θ
                  source
                  @[simp]
                  theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_map₂ {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) :
                  ∀ {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (a_1 : Quot CategoryTheory.FreeBicategory.Rel), (CategoryTheory.FreeBicategory.lift F).toPrelaxFunctor.map₂ a_1 = Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) (_ : ∀ (η θ : CategoryTheory.FreeBicategory.Hom₂ f g), CategoryTheory.FreeBicategory.Rel η θ → CategoryTheory.FreeBicategory.liftHom₂ F η = CategoryTheory.FreeBicategory.liftHom₂ F θ) a_1
                  source
                  @[simp]
                  theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrefunctor_map {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) :
                  ∀ {X Y : CategoryTheory.FreeBicategory B} (a : X ⟶ Y), (↑(CategoryTheory.FreeBicategory.lift F).toPrelaxFunctor).map a = CategoryTheory.FreeBicategory.liftHom F a
                  source
                  @[simp]
                  theorem CategoryTheory.FreeBicategory.lift_mapComp {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) :
                  ∀ {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.FreeBicategory.lift F).mapComp f g = CategoryTheory.Iso.refl ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y : CategoryTheory.FreeBicategory B} => CategoryTheory.FreeBicategory.liftHom F }, map₂ := fun {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} => Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) (_ : ∀ (η θ : CategoryTheory.FreeBicategory.Hom₂ f g), CategoryTheory.FreeBicategory.Rel η θ → CategoryTheory.FreeBicategory.liftHom₂ F η = CategoryTheory.FreeBicategory.liftHom₂ F θ) }).map (CategoryTheory.CategoryStruct.comp f g))
                  source
                  @[simp]
                  theorem CategoryTheory.FreeBicategory.lift_mapId {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) (a : CategoryTheory.FreeBicategory B) :
                  (CategoryTheory.FreeBicategory.lift F).mapId a = CategoryTheory.Iso.refl ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y : CategoryTheory.FreeBicategory B} => CategoryTheory.FreeBicategory.liftHom F }, map₂ := fun {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} => Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) (_ : ∀ (η θ : CategoryTheory.FreeBicategory.Hom₂ f g), CategoryTheory.FreeBicategory.Rel η θ → CategoryTheory.FreeBicategory.liftHom₂ F η = CategoryTheory.FreeBicategory.liftHom₂ F θ) }).map (CategoryTheory.CategoryStruct.id a))
                  source
                  @[simp]
                  theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrefunctor_obj {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) :
                  ∀ (a : B), (↑(CategoryTheory.FreeBicategory.lift F).toPrelaxFunctor).obj a = F.obj a
                  source
                  def CategoryTheory.FreeBicategory.lift {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) :
                  CategoryTheory.Pseudofunctor (CategoryTheory.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.

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