Documentation

Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

The bicategory of oplax functors between two bicategories #

Given bicategories B and C, we give a bicategory structure on B ⥤ᵒᵖᴸ C whose

source
def CategoryTheory.Oplax.OplaxTrans.whiskerLeft {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) :
CategoryStruct.comp η θ ⟶ CategoryStruct.comp η ι

Left whiskering of an oplax natural transformation and a modification.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Oplax.OplaxTrans.whiskerLeft_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B) :
    (whiskerLeft η Γ).as.app a = Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
    source
    def CategoryTheory.Oplax.OplaxTrans.whiskerRight {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) :
    CategoryStruct.comp η ι ⟶ CategoryStruct.comp θ ι

    Right whiskering of an oplax natural transformation and a modification.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Oplax.OplaxTrans.whiskerRight_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B) :
      (whiskerRight Γ ι).as.app a = Bicategory.whiskerRight (Γ.as.app a) (ι.app a)
      source
      def CategoryTheory.Oplax.OplaxTrans.associator {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) :
      CategoryStruct.comp (CategoryStruct.comp η θ) ι ≅ CategoryStruct.comp η (CategoryStruct.comp θ ι)

      Associator for the vertical composition of oplax natural transformations.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Oplax.OplaxTrans.associator_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :
        (associator η θ ι).inv.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
        source
        @[simp]
        theorem CategoryTheory.Oplax.OplaxTrans.associator_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :
        (associator η θ ι).hom.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
        source
        def CategoryTheory.Oplax.OplaxTrans.leftUnitor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) :
        CategoryStruct.comp (CategoryStruct.id F) η ≅ η

        Left unitor for the vertical composition of oplax natural transformations.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Oplax.OplaxTrans.leftUnitor_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) :
          (leftUnitor η).inv.as.app a = (Bicategory.leftUnitor (η.app a)).inv
          source
          @[simp]
          theorem CategoryTheory.Oplax.OplaxTrans.leftUnitor_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) :
          (leftUnitor η).hom.as.app a = (Bicategory.leftUnitor (η.app a)).hom
          source
          def CategoryTheory.Oplax.OplaxTrans.rightUnitor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) :
          CategoryStruct.comp η (CategoryStruct.id G) ≅ η

          Right unitor for the vertical composition of oplax natural transformations.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Oplax.OplaxTrans.rightUnitor_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) :
            (rightUnitor η).hom.as.app a = (Bicategory.rightUnitor (η.app a)).hom
            source
            @[simp]
            theorem CategoryTheory.Oplax.OplaxTrans.rightUnitor_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) :
            (rightUnitor η).inv.as.app a = (Bicategory.rightUnitor (η.app a)).inv
            source
            def CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :
            Bicategory (OplaxFunctor B C)

            A bicategory structure on the oplax functors between bicategories.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerLeft_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (x✝³ x✝⁴ : x✝¹ ⟶ x✝²) (Γ : x✝³ ⟶ x✝⁴) (a : B) :
              (Bicategory.whiskerLeft η Γ).as.app a = Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :
              (Bicategory.leftUnitor η).hom.as.app a = (Bicategory.leftUnitor (η.app a)).hom
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :
              (Bicategory.leftUnitor η).inv.as.app a = (Bicategory.leftUnitor (η.app a)).inv
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ : OplaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) :
              (Bicategory.associator η θ ι).inv.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerRight_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ x✝⁴ : x✝ ⟶ x✝¹) (Γ : x✝³ ⟶ x✝⁴) (η : x✝¹ ⟶ x✝²) (a : B) :
              (Bicategory.whiskerRight Γ η).as.app a = Bicategory.whiskerRight (Γ.as.app a) (η.app a)
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :
              (Bicategory.rightUnitor η).inv.as.app a = (Bicategory.rightUnitor (η.app a)).inv
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :
              (Bicategory.rightUnitor η).hom.as.app a = (Bicategory.rightUnitor (η.app a)).hom
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ : OplaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) :
              (Bicategory.associator η θ ι).hom.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom