Documentation

Mathlib.CategoryTheory.Functor.Quadrifunctor

Quadrifunctors obtained by composition of multifunctors #

Given a bifunctor F : C₁ ⥤ C₂₃₄ ⥤ E and a trifunctor G : C₂ ⥤ C₃ ⥤ C₄ ⥤ C₂₃₄, we define the quadrifunctor trifunctorComp₂₃₄ F G : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E.

Similarly, given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃₄ ⥤ E and a bifunctor G : C₃ ⥤ C₄ ⥤ C₃₄, we define the quadrifunctor trifunctorComp₃₄ F G : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E.

source
@[implicit_reducible]
def CategoryTheory.trifunctorComp₂₃₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂₃₄ E)) (G : Functor C₂ (Functor C₃ (Functor C₄ C₂₃₄))) :
Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))

Given a bifunctor F : C₁ ⥤ C₂₃₄ ⥤ E and a trifunctor G : C₂ ⥤ C₃ ⥤ C₄ ⥤ C₂₃₄, this is the quadrifunctor C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E obtained by composition.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.trifunctorComp₂₃₄_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂₃₄ E)) (G : Functor C₂ (Functor C₃ (Functor C₄ C₂₃₄))) (X₁ : C₁) :
    (trifunctorComp₂₃₄ F G).obj X₁ = (Functor.postcompose₃.obj (F.obj X₁)).obj G
    source
    @[simp]
    theorem CategoryTheory.trifunctorComp₂₃₄_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂₃₄ E)) (G : Functor C₂ (Functor C₃ (Functor C₄ C₂₃₄))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) :
    (trifunctorComp₂₃₄ F G).map f = (Functor.postcompose₃.map (F.map f)).app G
    source
    @[implicit_reducible]
    def CategoryTheory.trifunctorComp₂₃₄FunctorObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂₃₄ E)) :
    Functor (Functor C₂ (Functor C₃ (Functor C₄ C₂₃₄))) (Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))

    Auxiliary definition for trifunctorComp₂₃₄Functor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.trifunctorComp₂₃₄FunctorObj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂₃₄ E)) (G : Functor C₂ (Functor C₃ (Functor C₄ C₂₃₄))) :
      (trifunctorComp₂₃₄FunctorObj F).obj G = trifunctorComp₂₃₄ F G
      source
      @[simp]
      theorem CategoryTheory.trifunctorComp₂₃₄FunctorObj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂₃₄ E)) {G G' : Functor C₂ (Functor C₃ (Functor C₄ C₂₃₄))} (τ : G ⟶ G') (X₁ : C₁) :
      ((trifunctorComp₂₃₄FunctorObj F).map τ).app X₁ = (Functor.postcompose₃.obj (F.obj X₁)).map τ
      source
      @[implicit_reducible]
      def CategoryTheory.trifunctorComp₂₃₄FunctorMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] {F F' : Functor C₁ (Functor C₂₃₄ E)} (τ : F ⟶ F') :
      trifunctorComp₂₃₄FunctorObj F ⟶ trifunctorComp₂₃₄FunctorObj F'

      Auxiliary definition for trifunctorComp₂₃₄Functor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.trifunctorComp₂₃₄FunctorMap_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] {F F' : Functor C₁ (Functor C₂₃₄ E)} (τ : F ⟶ F') (G : Functor C₂ (Functor C₃ (Functor C₄ C₂₃₄))) (X₁ : C₁) :
        ((trifunctorComp₂₃₄FunctorMap τ).app G).app X₁ = (Functor.postcompose₃.map (τ.app X₁)).app G
        source
        @[implicit_reducible]
        def CategoryTheory.trifunctorComp₂₃₄Functor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] :
        Functor (Functor C₁ (Functor C₂₃₄ E)) (Functor (Functor C₂ (Functor C₃ (Functor C₄ C₂₃₄))) (Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))))

        The functor (C₁ ⥤ C₂₃₄ ⥤ E) ⥤ (C₂ ⥤ C₃ ⥤ C₄ ⥤ C₂₃₄) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E which sends F : C₁ ⥤ C₂₃₄ ⥤ E and G : C₂ ⥤ C₃ ⥤ C₄ ⥤ C₂₃₄ to trifunctorComp₂₃₄ F G.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.trifunctorComp₂₃₄Functor_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂₃₄ E)) :
          trifunctorComp₂₃₄Functor.obj F = trifunctorComp₂₃₄FunctorObj F
          source
          @[simp]
          theorem CategoryTheory.trifunctorComp₂₃₄Functor_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃₄ : Type u_5} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} C₂₃₄] [Category.{v_7, u_7} E] {X✝ Y✝ : Functor C₁ (Functor C₂₃₄ E)} (τ : X✝ ⟶ Y✝) :
          trifunctorComp₂₃₄Functor.map τ = trifunctorComp₂₃₄FunctorMap τ
          source
          @[implicit_reducible]
          def CategoryTheory.trifunctorComp₃₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂ (Functor C₃₄ E))) (G : Functor C₃ (Functor C₄ C₃₄)) :
          Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))

          Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃₄ ⥤ E and a bifunctor G : C₃ ⥤ C₄ ⥤ C₃₄, this is the quadrifunctor C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E obtained by composition.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.trifunctorComp₃₄_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂ (Functor C₃₄ E))) (G : Functor C₃ (Functor C₄ C₃₄)) (X₁ : C₁) :
            (trifunctorComp₃₄ F G).obj X₁ = bifunctorComp₂₃ (F.obj X₁) G
            source
            @[simp]
            theorem CategoryTheory.trifunctorComp₃₄_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂ (Functor C₃₄ E))) (G : Functor C₃ (Functor C₄ C₃₄)) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) :
            (trifunctorComp₃₄ F G).map f = (bifunctorComp₂₃Functor.map (F.map f)).app G
            source
            @[implicit_reducible]
            def CategoryTheory.trifunctorComp₃₄FunctorObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂ (Functor C₃₄ E))) :
            Functor (Functor C₃ (Functor C₄ C₃₄)) (Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))

            Auxiliary definition for trifunctorComp₃₄Functor.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.trifunctorComp₃₄FunctorObj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂ (Functor C₃₄ E))) {G G' : Functor C₃ (Functor C₄ C₃₄)} (τ : G ⟶ G') (X₁ : C₁) :
              ((trifunctorComp₃₄FunctorObj F).map τ).app X₁ = (bifunctorComp₂₃Functor.obj (F.obj X₁)).map τ
              source
              @[simp]
              theorem CategoryTheory.trifunctorComp₃₄FunctorObj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂ (Functor C₃₄ E))) (G : Functor C₃ (Functor C₄ C₃₄)) :
              (trifunctorComp₃₄FunctorObj F).obj G = trifunctorComp₃₄ F G
              source
              @[implicit_reducible]
              def CategoryTheory.trifunctorComp₃₄FunctorMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] {F F' : Functor C₁ (Functor C₂ (Functor C₃₄ E))} (τ : F ⟶ F') :
              trifunctorComp₃₄FunctorObj F ⟶ trifunctorComp₃₄FunctorObj F'

              Auxiliary definition for trifunctorComp₃₄Functor.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.trifunctorComp₃₄FunctorMap_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] {F F' : Functor C₁ (Functor C₂ (Functor C₃₄ E))} (τ : F ⟶ F') (G : Functor C₃ (Functor C₄ C₃₄)) (X₁ : C₁) :
                ((trifunctorComp₃₄FunctorMap τ).app G).app X₁ = (bifunctorComp₂₃Functor.map (τ.app X₁)).app G
                source
                @[implicit_reducible]
                def CategoryTheory.trifunctorComp₃₄Functor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] :
                Functor (Functor C₁ (Functor C₂ (Functor C₃₄ E))) (Functor (Functor C₃ (Functor C₄ C₃₄)) (Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))))

                The functor (C₁ ⥤ C₂ ⥤ C₃₄ ⥤ E) ⥤ (C₃ ⥤ C₄ ⥤ C₃₄) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E which sends F : C₁ ⥤ C₂ ⥤ C₃₄ ⥤ E and G : C₃ ⥤ C₄ ⥤ C₃₄ to trifunctorComp₃₄ F G.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.trifunctorComp₃₄Functor_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] (F : Functor C₁ (Functor C₂ (Functor C₃₄ E))) :
                  trifunctorComp₃₄Functor.obj F = trifunctorComp₃₄FunctorObj F
                  source
                  @[simp]
                  theorem CategoryTheory.trifunctorComp₃₄Functor_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₃₄ : Type u_6} {E : Type u_7} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_6, u_6} C₃₄] [Category.{v_7, u_7} E] {X✝ Y✝ : Functor C₁ (Functor C₂ (Functor C₃₄ E))} (τ : X✝ ⟶ Y✝) :
                  trifunctorComp₃₄Functor.map τ = trifunctorComp₃₄FunctorMap τ