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 #

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

Equations
Instances For
    inductive CategoryTheory.FreeBicategory.Hom {B : Type u} [Quiver B] :
    BBType (max u v)

    1-morphisms in the free bicategory.

    Instances For
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      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

        Relations between 2-morphisms in the free bicategory.

        Instances For

          Bicategory structure on the free bicategory.

          Equations
          • One or more equations did not get rendered due to their size.
          @[reducible, inline]
          Equations
          • η.mk = Quot.mk CategoryTheory.FreeBicategory.Rel η
          Instances For
            @[simp]
            theorem CategoryTheory.FreeBicategory.of_obj {B : Type u} [Quiver B] (a : B) :
            CategoryTheory.FreeBicategory.of.obj a = id a
            @[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

            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
              @[simp]
              @[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} (x : a b) (x_1 : b c), (CategoryTheory.FreeBicategory.lift F).mapComp x x_1 = CategoryTheory.Iso.refl ({ 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) , map₂_id := , map₂_comp := }.map (CategoryTheory.CategoryStruct.comp x x_1))

              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