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.instInhabitedFreeBicategory (B : Type u) [Inhabited B] :
    Inhabited (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.instInhabitedHomOfHom {B : Type u} [Quiver B] (a b : B) [Inhabited (a ⟶ b)] :
      Inhabited (Hom a b)
      Equations
      source
      instance CategoryTheory.FreeBicategory.quiver {B : Type u} [Quiver B] :
      Quiver (FreeBicategory B)
      Equations
      source
      instance CategoryTheory.FreeBicategory.categoryStruct {B : Type u} [Quiver B] :
      CategoryStruct.{max u v, u} (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 b : 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 b : FreeBicategory B} {f g : a ⟶ b} :
        Hom₂ f g → 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 b : FreeBicategory B) :
          Category.{max u v, max u v} (a ⟶ b)
          Equations
          source
          instance CategoryTheory.FreeBicategory.bicategory {B : Type u} [Quiver B] :
          Bicategory (FreeBicategory B)

          Bicategory structure on the free bicategory.

          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[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
          Equations
          Instances For
            source
            @[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
            source
            @[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
            source
            @[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
            source
            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
            source
            @[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
            source
            @[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
            source
            @[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
            source
            @[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
            source
            @[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
            source
            @[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
            source
            @[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
            source
            def CategoryTheory.FreeBicategory.of {B : Type u} [Quiver B] :
            B ⥤q FreeBicategory B

            Canonical prefunctor from B to free_bicategory B.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.FreeBicategory.of_obj {B : Type u} [Quiver B] (a : B) :
              of.obj a = id a
              source
              @[simp]
              theorem CategoryTheory.FreeBicategory.of_map {B : Type u} [Quiver B] (x✝ x✝¹ : B) (f : x✝ ⟶ x✝¹) :
              of.map f = Hom.of f
              source
              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.

              Equations
              Instances For
                source
                @[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)
                source
                @[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)
                source
                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.

                Instances For
                  source
                  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 θ
                  source
                  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.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[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✝
                    source
                    @[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 ({ obj := F.obj, map := fun {X Y : FreeBicategory B} => liftHom F, map₂ := fun {a b : FreeBicategory B} {f g : a ⟶ b} => Quot.lift (liftHom₂ F) ⋯, map₂_id := ⋯, map₂_comp := ⋯ }.map (CategoryStruct.comp x✝ x✝¹))
                    source
                    @[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 ({ obj := F.obj, map := fun {X Y : FreeBicategory B} => liftHom F, map₂ := fun {a b : FreeBicategory B} {f g : a ⟶ b} => Quot.lift (liftHom₂ F) ⋯, map₂_id := ⋯, map₂_comp := ⋯ }.map (CategoryStruct.id x✝))
                    source
                    @[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
                    source
                    @[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✝