Documentation

Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Bicategories of oplax functors #

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

source
def CategoryTheory.Oplax.LaxTrans.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 a lax natural transformation and a modification.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Oplax.LaxTrans.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.LaxTrans.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 a lax natural transformation and a modification.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Oplax.LaxTrans.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.LaxTrans.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 lax natural transformations.

      Instances For
        source
        @[simp]
        theorem CategoryTheory.Oplax.LaxTrans.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
        @[simp]
        theorem CategoryTheory.Oplax.LaxTrans.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
        def CategoryTheory.Oplax.LaxTrans.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 lax natural transformations.

        Instances For
          source
          @[simp]
          theorem CategoryTheory.Oplax.LaxTrans.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.LaxTrans.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.LaxTrans.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 lax natural transformations.

          Instances For
            source
            @[simp]
            theorem CategoryTheory.Oplax.LaxTrans.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.LaxTrans.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
            @[implicit_reducible]
            def CategoryTheory.Oplax.LaxTrans.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, with lax transformations.

            Instances For
              source
              @[simp]
              theorem CategoryTheory.Oplax.LaxTrans.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.LaxTrans.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.LaxTrans.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.LaxTrans.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.LaxTrans.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.LaxTrans.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.LaxTrans.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.LaxTrans.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
              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.

              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.

                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.

                  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.

                    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.

                      Instances For
                        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
                        @[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
                        @[implicit_reducible]
                        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.

                        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_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_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_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_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_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
                          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