Documentation

Mathlib.CategoryTheory.ComposableArrows

Composable arrows #

If C is a category, the type of n-simplices in the nerve of C identifies to the type of functors Fin (n + 1) ⥤ C, which can be thought as families of n composable arrows in C. In this file, we introduce and study this category ComposableArrows C n of n composable arrows in C.

If F : ComposableArrows C n, we define F.left as the leftmost object, F.right as the rightmost object, and F.hom : F.left ⟶ F.right is the canonical map.

The most significant definition in this file is the constructor F.precomp f : ComposableArrows C (n + 1) for F : ComposableArrows C n and f : X ⟶ F.left: "it shifts F towards the right and inserts f on the left". This precomp has good definitional properties.

In the namespace CategoryTheory.ComposableArrows, we provide constructors like mk₁ f, mk₂ f g, mk₃ f g h for ComposableArrows C n for small n.

TODO (@joelriou):

New simprocs that run even in dsimp have caused breakages in this file.

(e.g. dsimp can now simplify 2 + 3 to 5)

For now, we just turn off simprocs in this file. We'll soon provide finer grained options here, e.g. to turn off simprocs only in dsimp, etc.

However, hopefully it is possible to refactor the material here so that no backwards compatibility set_options are required at all

@[reducible, inline]

ComposableArrows C n is the type of functors Fin (n + 1) ⥤ C.

Equations
Instances For

    A wrapper for omega which prefaces it with some quick and useful attempts

    Equations
    Instances For
      @[reducible, inline]

      The ith object (with i : ℕ such that i ≤ n) of F : ComposableArrows C n.

      Equations
      • F.obj' i hi = F.obj i,
      Instances For
        @[reducible, inline]
        abbrev CategoryTheory.ComposableArrows.map' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C n) (i : ) (j : ) (hij : autoParam (i j) _auto✝) (hjn : autoParam (j n) _auto✝) :
        F.obj i, F.obj j,

        The map F.obj' i ⟶ F.obj' j when F : ComposableArrows C n, and i and j are natural numbers such that i ≤ j ≤ n.

        Equations
        Instances For
          theorem CategoryTheory.ComposableArrows.map'_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C n) (i : ) (j : ) (k : ) (hij : autoParam (i j) _auto✝) (hjk : autoParam (j k) _auto✝) (hk : autoParam (k n) _auto✝) :
          F.map' i k hk = CategoryTheory.CategoryStruct.comp (F.map' i j hij ) (F.map' j k hjk hk)
          @[reducible, inline]

          The leftmost object of F : ComposableArrows C n.

          Equations
          • F.left = F.obj' 0
          Instances For
            @[reducible, inline]

            The rightmost object of F : ComposableArrows C n.

            Equations
            • F.right = F.obj' n
            Instances For
              @[reducible, inline]

              The canonical map F.left ⟶ F.right for F : ComposableArrows C n.

              Equations
              • F.hom = F.map' 0 n
              Instances For
                @[reducible, inline]
                abbrev CategoryTheory.ComposableArrows.app' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (φ : F G) (i : ) (hi : autoParam (i n) _auto✝) :
                F.obj' i hi G.obj' i hi

                The map F.obj' i ⟶ G.obj' i induced on ith objects by a morphism F ⟶ G in ComposableArrows C n when i is a natural number such that i ≤ n.

                Equations
                Instances For
                  def CategoryTheory.ComposableArrows.Mk₁.obj {C : Type u_1} (X₀ : C) (X₁ : C) :
                  Fin 2C

                  The map which sends 0 : Fin 2 to X₀ and 1 to X₁.

                  Equations
                  Instances For

                    The obvious map obj X₀ X₁ i ⟶ obj X₀ X₁ j whenever i j : Fin 2 satisfy i ≤ j.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.ComposableArrows.mk₁_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} (f : X₀ X₁) :

                      Constructor for ComposableArrows C 1.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem CategoryTheory.ComposableArrows.homMk_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) hi) (app i + 1, ) = CategoryTheory.CategoryStruct.comp (app i, ) (G.map' i (i + 1) hi)) (i : Fin (n + 1)) :
                        def CategoryTheory.ComposableArrows.homMk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) hi) (app i + 1, ) = CategoryTheory.CategoryStruct.comp (app i, ) (G.map' i (i + 1) hi)) :
                        F G

                        Constructor for morphisms F ⟶ G in ComposableArrows C n which takes as inputs a family of morphisms F.obj i ⟶ G.obj i and the naturality condition only for the maps in Fin (n + 1) given by inequalities of the form i ≤ i + 1.

                        Equations
                        Instances For
                          @[simp]
                          theorem CategoryTheory.ComposableArrows.isoMk_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) hi) (app i + 1, ).hom = CategoryTheory.CategoryStruct.comp (app i, ).hom (G.map' i (i + 1) hi)) :
                          (CategoryTheory.ComposableArrows.isoMk app w).inv = CategoryTheory.ComposableArrows.homMk (fun (i : Fin (n + 1)) => (app i).inv)
                          @[simp]
                          theorem CategoryTheory.ComposableArrows.isoMk_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) hi) (app i + 1, ).hom = CategoryTheory.CategoryStruct.comp (app i, ).hom (G.map' i (i + 1) hi)) :
                          def CategoryTheory.ComposableArrows.isoMk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) hi) (app i + 1, ).hom = CategoryTheory.CategoryStruct.comp (app i, ).hom (G.map' i (i + 1) hi)) :
                          F G

                          Constructor for isomorphisms F ≅ G in ComposableArrows C n which takes as inputs a family of isomorphisms F.obj i ≅ G.obj i and the naturality condition only for the maps in Fin (n + 1) given by inequalities of the form i ≤ i + 1.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem CategoryTheory.ComposableArrows.ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i) (w : ∀ (i : ) (hi : i < n), F.map' i (i + 1) hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ) (CategoryTheory.CategoryStruct.comp (G.map' i (i + 1) hi) (CategoryTheory.eqToHom ))) :
                            F = G
                            @[simp]
                            theorem CategoryTheory.ComposableArrows.homMk₀_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (f : F.obj' 0 G.obj' 0 ) (i : Fin (0 + 1)) :
                            (CategoryTheory.ComposableArrows.homMk₀ f).app i = match i with | 0, isLt => f

                            Constructor for morphisms in ComposableArrows C 0.

                            Equations
                            Instances For
                              @[simp]
                              theorem CategoryTheory.ComposableArrows.isoMk₀_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (e : F.obj' 0 G.obj' 0 ) (i : Fin (0 + 1)) :
                              (CategoryTheory.ComposableArrows.isoMk₀ e).hom.app i = match i with | 0, isLt => e.hom
                              @[simp]
                              theorem CategoryTheory.ComposableArrows.isoMk₀_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (e : F.obj' 0 G.obj' 0 ) (i : Fin (0 + 1)) :
                              (CategoryTheory.ComposableArrows.isoMk₀ e).inv.app i = match i with | 0, isLt => e.inv

                              Constructor for isomorphisms in ComposableArrows C 0.

                              Equations
                              Instances For
                                @[simp]
                                theorem CategoryTheory.ComposableArrows.homMk₁_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : F.obj' 0 G.obj' 0 ) (right : F.obj' 1 G.obj' 1 ) (w : autoParam (CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) right = CategoryTheory.CategoryStruct.comp left (G.map' 0 1 )) _auto✝) (i : Fin (1 + 1)) :
                                (CategoryTheory.ComposableArrows.homMk₁ left right w).app i = match i with | 0, isLt => left | 1, isLt => right
                                def CategoryTheory.ComposableArrows.homMk₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : F.obj' 0 G.obj' 0 ) (right : F.obj' 1 G.obj' 1 ) (w : autoParam (CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) right = CategoryTheory.CategoryStruct.comp left (G.map' 0 1 )) _auto✝) :
                                F G

                                Constructor for morphisms in ComposableArrows C 1.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.ComposableArrows.isoMk₁_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : F.obj' 0 G.obj' 0 ) (right : F.obj' 1 G.obj' 1 ) (w : autoParam (CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 )) _auto✝) (i : Fin (1 + 1)) :
                                  (CategoryTheory.ComposableArrows.isoMk₁ left right w).inv.app i = match i with | 0, isLt => left.inv | 1, isLt => right.inv
                                  @[simp]
                                  theorem CategoryTheory.ComposableArrows.isoMk₁_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : F.obj' 0 G.obj' 0 ) (right : F.obj' 1 G.obj' 1 ) (w : autoParam (CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 )) _auto✝) (i : Fin (1 + 1)) :
                                  (CategoryTheory.ComposableArrows.isoMk₁ left right w).hom.app i = match i with | 0, isLt => left.hom | 1, isLt => right.hom
                                  def CategoryTheory.ComposableArrows.isoMk₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : F.obj' 0 G.obj' 0 ) (right : F.obj' 1 G.obj' 1 ) (w : autoParam (CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 )) _auto✝) :
                                  F G

                                  Constructor for isomorphisms in ComposableArrows C 1.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    The map Fin (n + 1 + 1) → C which "shifts" F.obj' to the right and inserts X in the zeroth position.

                                    Equations
                                    Instances For
                                      @[simp]

                                      Auxiliary definition for the action on maps of the functor F.precomp f. It sends 0 ≤ 1 to f and i + 1 ≤ j + 1 to F.map' i j.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X F.left) (j : ) (hj : j + 2 < n + 1 + 1) :
                                        CategoryTheory.ComposableArrows.Precomp.map F f 0 j + 2, hj = CategoryTheory.CategoryStruct.comp f (F.map' 0 (j + 1) )
                                        @[simp]
                                        theorem CategoryTheory.ComposableArrows.Precomp.map_succ_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X F.left) (i : ) (j : ) (hi : i + 1 < n + 1 + 1) (hj : j + 1 < n + 1 + 1) (hij : i + 1 j + 1) :
                                        CategoryTheory.ComposableArrows.Precomp.map F f i + 1, hi j + 1, hj hij = F.map' i j
                                        @[simp]
                                        theorem CategoryTheory.ComposableArrows.Precomp.map_one_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X F.left) (j : ) (hj : j + 1 < n + 1 + 1) :
                                        CategoryTheory.ComposableArrows.Precomp.map F f 1 j + 1, hj = F.map' 0 j
                                        @[simp]
                                        theorem CategoryTheory.ComposableArrows.precomp_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X F.left) :
                                        ∀ (a : Fin (n + 1 + 1)), (F.precomp f).obj a = CategoryTheory.ComposableArrows.Precomp.obj F X a
                                        @[simp]
                                        theorem CategoryTheory.ComposableArrows.precomp_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X F.left) :
                                        ∀ {X_1 Y : Fin (n + 1 + 1)} (g : X_1 Y), (F.precomp f).map g = CategoryTheory.ComposableArrows.Precomp.map F f X_1 Y

                                        "Precomposition" of F : ComposableArrows C n by a morphism f : X ⟶ F.left.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          def CategoryTheory.ComposableArrows.mk₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} {X₂ : C} (f : X₀ X₁) (g : X₁ X₂) :

                                          Constructor for ComposableArrows C 2.

                                          Equations
                                          Instances For
                                            def CategoryTheory.ComposableArrows.mk₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} {X₂ : C} {X₃ : C} (f : X₀ X₁) (g : X₁ X₂) (h : X₂ X₃) :

                                            Constructor for ComposableArrows C 3.

                                            Equations
                                            Instances For
                                              def CategoryTheory.ComposableArrows.mk₄ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} (f : X₀ X₁) (g : X₁ X₂) (h : X₂ X₃) (i : X₃ X₄) :

                                              Constructor for ComposableArrows C 4.

                                              Equations
                                              Instances For
                                                def CategoryTheory.ComposableArrows.mk₅ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} {X₅ : C} (f : X₀ X₁) (g : X₁ X₂) (h : X₂ X₃) (i : X₃ X₄) (j : X₄ X₅) :

                                                Constructor for ComposableArrows C 5.

                                                Equations
                                                Instances For

                                                  These examples are meant to test the good definitional properties of precomp, and that dsimp can see through.

                                                  @[simp]
                                                  theorem CategoryTheory.ComposableArrows.whiskerLeft_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {m : } (F : CategoryTheory.ComposableArrows C m) (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (X : Fin (n + 1)) :
                                                  (F.whiskerLeft Φ).obj X = F.obj (Φ.obj X)
                                                  @[simp]
                                                  theorem CategoryTheory.ComposableArrows.whiskerLeft_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {m : } (F : CategoryTheory.ComposableArrows C m) (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) :
                                                  ∀ {X Y : Fin (n + 1)} (f : X Y), (F.whiskerLeft Φ).map f = F.map (Φ.map f)

                                                  The map ComposableArrows C m → ComposableArrows C n obtained by precomposition with a functor Fin (n + 1) ⥤ Fin (m + 1).

                                                  Equations
                                                  • F.whiskerLeft Φ = Φ.comp F
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {m : } (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) :
                                                    ∀ {X Y : CategoryTheory.ComposableArrows C m} (f : X Y) (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).map f).app X_1 = f.app (Φ.obj X_1)
                                                    @[simp]
                                                    theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {m : } (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (F : CategoryTheory.ComposableArrows C m) :
                                                    ∀ {X Y : Fin (n + 1)} (f : X Y), ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).obj F).map f = F.map (Φ.map f)

                                                    The functor ComposableArrows C m ⥤ ComposableArrows C n obtained by precomposition with a functor Fin (n + 1) ⥤ Fin (m + 1).

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem Fin.succFunctor_obj (n : ) (i : Fin n) :
                                                      (Fin.succFunctor n).obj i = i.succ
                                                      @[simp]
                                                      theorem Fin.succFunctor_map (n : ) {i : Fin n} {j : Fin n} (hij : i j) :

                                                      The functor Fin n ⥤ Fin (n + 1) which sends i to i.succ.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.ComposableArrows.δ₀Functor_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } :
                                                        ∀ {X Y : CategoryTheory.ComposableArrows C (n + 1)} (f : X Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δ₀Functor.map f).app X_1 = f.app X_1.succ
                                                        @[simp]
                                                        theorem CategoryTheory.ComposableArrows.δ₀Functor_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C (n + 1)) (X : Fin (n + 1)) :
                                                        (CategoryTheory.ComposableArrows.δ₀Functor.obj F).obj X = F.obj X.succ
                                                        @[simp]
                                                        theorem CategoryTheory.ComposableArrows.δ₀Functor_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C (n + 1)) :
                                                        ∀ {X Y : Fin (n + 1)} (f : X Y), (CategoryTheory.ComposableArrows.δ₀Functor.obj F).map f = F.map (CategoryTheory.homOfLE )

                                                        The functor ComposableArrows C (n + 1) ⥤ ComposableArrows C n which forgets the first arrow.

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]

                                                          The ComposableArrows C n obtained by forgetting the first arrow.

                                                          Equations
                                                          • F.δ₀ = CategoryTheory.ComposableArrows.δ₀Functor.obj F
                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.ComposableArrows.precomp_δ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X F.left) :
                                                            (F.precomp f).δ₀ = F
                                                            @[simp]
                                                            theorem Fin.castSuccFunctor_obj (n : ) (i : Fin n) :
                                                            (Fin.castSuccFunctor n).obj i = i.castSucc
                                                            @[simp]
                                                            theorem Fin.castSuccFunctor_map (n : ) :
                                                            ∀ {X Y : Fin n} (hij : X Y), (Fin.castSuccFunctor n).map hij = hij

                                                            The functor Fin n ⥤ Fin (n + 1) which sends i to i.castSucc.

                                                            Equations
                                                            • Fin.castSuccFunctor n = { obj := fun (i : Fin n) => i.castSucc, map := fun {X Y : Fin n} (hij : X Y) => hij, map_id := , map_comp := }
                                                            Instances For
                                                              @[simp]
                                                              theorem CategoryTheory.ComposableArrows.δlastFunctor_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C (n + 1)) (X : Fin (n + 1)) :
                                                              (CategoryTheory.ComposableArrows.δlastFunctor.obj F).obj X = F.obj X.castSucc
                                                              @[simp]
                                                              theorem CategoryTheory.ComposableArrows.δlastFunctor_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C (n + 1)) :
                                                              ∀ {X Y : Fin (n + 1)} (f : X Y), (CategoryTheory.ComposableArrows.δlastFunctor.obj F).map f = F.map f
                                                              @[simp]
                                                              theorem CategoryTheory.ComposableArrows.δlastFunctor_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } :
                                                              ∀ {X Y : CategoryTheory.ComposableArrows C (n + 1)} (f : X Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δlastFunctor.map f).app X_1 = f.app X_1.castSucc

                                                              The functor ComposableArrows C (n + 1) ⥤ ComposableArrows C n which forgets the last arrow.

                                                              Equations
                                                              Instances For
                                                                @[reducible, inline]

                                                                The ComposableArrows C n obtained by forgetting the first arrow.

                                                                Equations
                                                                • F.δlast = CategoryTheory.ComposableArrows.δlastFunctor.obj F
                                                                Instances For
                                                                  def CategoryTheory.ComposableArrows.homMkSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : F.obj' 0 G.obj' 0 ) (β : F.δ₀ G.δ₀) (w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) (CategoryTheory.ComposableArrows.app' β 0 ) = CategoryTheory.CategoryStruct.comp α (G.map' 0 1 )) :
                                                                  F G

                                                                  Inductive construction of morphisms in ComposableArrows C (n + 1): in order to construct a morphism F ⟶ G, it suffices to provide α : F.obj' 0 ⟶ G.obj' 0 and β : F.δ₀ ⟶ G.δ₀ such that F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem CategoryTheory.ComposableArrows.homMkSucc_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : F.obj' 0 G.obj' 0 ) (β : F.δ₀ G.δ₀) (w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) (CategoryTheory.ComposableArrows.app' β 0 ) = CategoryTheory.CategoryStruct.comp α (G.map' 0 1 )) :
                                                                    @[simp]
                                                                    theorem CategoryTheory.ComposableArrows.homMkSucc_app_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : F.obj' 0 G.obj' 0 ) (β : F.δ₀ G.δ₀) (w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) (CategoryTheory.ComposableArrows.app' β 0 ) = CategoryTheory.CategoryStruct.comp α (G.map' 0 1 )) (i : ) (hi : i + 1 < n + 1 + 1) :
                                                                    theorem CategoryTheory.ComposableArrows.hom_ext_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} {f : F G} {g : F G} (h₀ : CategoryTheory.ComposableArrows.app' f 0 = CategoryTheory.ComposableArrows.app' g 0 ) (h₁ : CategoryTheory.ComposableArrows.δ₀Functor.map f = CategoryTheory.ComposableArrows.δ₀Functor.map g) :
                                                                    f = g
                                                                    @[simp]
                                                                    theorem CategoryTheory.ComposableArrows.isoMkSucc_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : F.obj' 0 G.obj' 0 ) (β : F.δ₀ G.δ₀) (w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) (CategoryTheory.ComposableArrows.app' β.hom 0 ) = CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 )) :
                                                                    @[simp]
                                                                    def CategoryTheory.ComposableArrows.isoMkSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : F.obj' 0 G.obj' 0 ) (β : F.δ₀ G.δ₀) (w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ) (CategoryTheory.ComposableArrows.app' β.hom 0 ) = CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 )) :
                                                                    F G

                                                                    Inductive construction of isomorphisms in ComposableArrows C (n + 1): in order to construct an isomorphism F ≅ G, it suffices to provide α : F.obj' 0 ≅ G.obj' 0 and β : F.δ₀ ≅ G.δ₀ such that F.map' 0 1 ≫ app' β.hom 0 = α.hom ≫ G.map' 0 1.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      theorem CategoryTheory.ComposableArrows.ext_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (h₀ : F.obj' 0 = G.obj' 0 ) (h : F.δ₀ = G.δ₀) (w : F.map' 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (G.map' 0 1 ) (CategoryTheory.eqToHom ))) :
                                                                      F = G
                                                                      theorem CategoryTheory.ComposableArrows.precomp_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (F : CategoryTheory.ComposableArrows C (n + 1)) :
                                                                      ∃ (F₀ : CategoryTheory.ComposableArrows C n) (X₀ : C) (f₀ : X₀ F₀.left), F = F₀.precomp f₀
                                                                      def CategoryTheory.ComposableArrows.homMk₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) :
                                                                      f g

                                                                      Constructor for morphisms in ComposableArrows C 2.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem CategoryTheory.ComposableArrows.homMk₂_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) :
                                                                        (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 0 = app₀
                                                                        @[simp]
                                                                        theorem CategoryTheory.ComposableArrows.homMk₂_app_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) :
                                                                        (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁
                                                                        @[simp]
                                                                        theorem CategoryTheory.ComposableArrows.homMk₂_app_two {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) :
                                                                        (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 2, = app₂
                                                                        @[simp]
                                                                        theorem CategoryTheory.ComposableArrows.isoMk₂_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) :
                                                                        (CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).hom = CategoryTheory.ComposableArrows.homMk₂ app₀.hom app₁.hom app₂.hom w₀ w₁
                                                                        @[simp]
                                                                        theorem CategoryTheory.ComposableArrows.isoMk₂_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) :
                                                                        (CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).inv = CategoryTheory.ComposableArrows.homMk₂ app₀.inv app₁.inv app₂.inv
                                                                        def CategoryTheory.ComposableArrows.isoMk₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) :
                                                                        f g

                                                                        Constructor for isomorphisms in ComposableArrows C 2.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          theorem CategoryTheory.ComposableArrows.ext₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (h₀ : f.obj' 0 = g.obj' 0 ) (h₁ : f.obj' 1 = g.obj' 1 ) (h₂ : f.obj' 2 = g.obj' 2 ) (w₀ : f.map' 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (g.map' 0 1 ) (CategoryTheory.eqToHom ))) (w₁ : f.map' 1 2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (g.map' 1 2 ) (CategoryTheory.eqToHom ))) :
                                                                          f = g
                                                                          theorem CategoryTheory.ComposableArrows.mk₂_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 2) :
                                                                          ∃ (X₀ : C) (X₁ : C) (X₂ : C) (f₀ : X₀ X₁) (f₁ : X₁ X₂), X = CategoryTheory.ComposableArrows.mk₂ f₀ f₁
                                                                          def CategoryTheory.ComposableArrows.homMk₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) :
                                                                          f g

                                                                          Constructor for morphisms in ComposableArrows C 3.

                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem CategoryTheory.ComposableArrows.homMk₃_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) :
                                                                            (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 0 = app₀
                                                                            @[simp]
                                                                            theorem CategoryTheory.ComposableArrows.homMk₃_app_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) :
                                                                            (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 1 = app₁
                                                                            @[simp]
                                                                            theorem CategoryTheory.ComposableArrows.homMk₃_app_two {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) :
                                                                            (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 2, = app₂
                                                                            @[simp]
                                                                            theorem CategoryTheory.ComposableArrows.homMk₃_app_three {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) :
                                                                            (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 3, = app₃
                                                                            @[simp]
                                                                            theorem CategoryTheory.ComposableArrows.isoMk₃_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) :
                                                                            (CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).inv = CategoryTheory.ComposableArrows.homMk₃ app₀.inv app₁.inv app₂.inv app₃.inv
                                                                            @[simp]
                                                                            theorem CategoryTheory.ComposableArrows.isoMk₃_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) :
                                                                            (CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).hom = CategoryTheory.ComposableArrows.homMk₃ app₀.hom app₁.hom app₂.hom app₃.hom w₀ w₁ w₂
                                                                            def CategoryTheory.ComposableArrows.isoMk₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) :
                                                                            f g

                                                                            Constructor for isomorphisms in ComposableArrows C 3.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              theorem CategoryTheory.ComposableArrows.ext₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (h₀ : f.obj' 0 = g.obj' 0 ) (h₁ : f.obj' 1 = g.obj' 1 ) (h₂ : f.obj' 2 = g.obj' 2 ) (h₃ : f.obj' 3 = g.obj' 3 ) (w₀ : f.map' 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (g.map' 0 1 ) (CategoryTheory.eqToHom ))) (w₁ : f.map' 1 2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (g.map' 1 2 ) (CategoryTheory.eqToHom ))) (w₂ : f.map' 2 3 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (g.map' 2 3 ) (CategoryTheory.eqToHom ))) :
                                                                              f = g
                                                                              theorem CategoryTheory.ComposableArrows.mk₃_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 3) :
                                                                              ∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (f₀ : X₀ X₁) (f₁ : X₁ X₂) (f₂ : X₂ X₃), X = CategoryTheory.ComposableArrows.mk₃ f₀ f₁ f₂
                                                                              def CategoryTheory.ComposableArrows.homMk₄ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) :
                                                                              f g

                                                                              Constructor for morphisms in ComposableArrows C 4.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem CategoryTheory.ComposableArrows.homMk₄_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) :
                                                                                (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 0 = app₀
                                                                                @[simp]
                                                                                theorem CategoryTheory.ComposableArrows.homMk₄_app_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) :
                                                                                (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 1 = app₁
                                                                                @[simp]
                                                                                theorem CategoryTheory.ComposableArrows.homMk₄_app_two {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) :
                                                                                (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 2, = app₂
                                                                                @[simp]
                                                                                theorem CategoryTheory.ComposableArrows.homMk₄_app_three {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) :
                                                                                (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 3, = app₃
                                                                                @[simp]
                                                                                theorem CategoryTheory.ComposableArrows.homMk₄_app_four {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) :
                                                                                (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 4, = app₄
                                                                                theorem CategoryTheory.ComposableArrows.map'_inv_eq_inv_map' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } {m : } (h : n + 1 m) {f : CategoryTheory.ComposableArrows C m} {g : CategoryTheory.ComposableArrows C m} (app : f.obj' n g.obj' n ) (app' : f.obj' (n + 1) h g.obj' (n + 1) h) (w : CategoryTheory.CategoryStruct.comp (f.map' n (n + 1) h) app'.hom = CategoryTheory.CategoryStruct.comp app.hom (g.map' n (n + 1) h)) :
                                                                                CategoryTheory.CategoryStruct.comp (g.map' n (n + 1) h) app'.inv = CategoryTheory.CategoryStruct.comp app.inv (f.map' n (n + 1) h)
                                                                                @[simp]
                                                                                theorem CategoryTheory.ComposableArrows.isoMk₄_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 )) :
                                                                                (CategoryTheory.ComposableArrows.isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).hom = CategoryTheory.ComposableArrows.homMk₄ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom w₀ w₁ w₂ w₃
                                                                                @[simp]
                                                                                theorem CategoryTheory.ComposableArrows.isoMk₄_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 )) :
                                                                                (CategoryTheory.ComposableArrows.isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).inv = CategoryTheory.ComposableArrows.homMk₄ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv
                                                                                def CategoryTheory.ComposableArrows.isoMk₄ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 )) :
                                                                                f g

                                                                                Constructor for isomorphisms in ComposableArrows C 4.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  theorem CategoryTheory.ComposableArrows.ext₄ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (h₀ : f.obj' 0 = g.obj' 0 ) (h₁ : f.obj' 1 = g.obj' 1 ) (h₂ : f.obj' 2 = g.obj' 2 ) (h₃ : f.obj' 3 = g.obj' 3 ) (h₄ : f.obj' 4 = g.obj' 4 ) (w₀ : f.map' 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (g.map' 0 1 ) (CategoryTheory.eqToHom ))) (w₁ : f.map' 1 2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (g.map' 1 2 ) (CategoryTheory.eqToHom ))) (w₂ : f.map' 2 3 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (g.map' 2 3 ) (CategoryTheory.eqToHom ))) (w₃ : f.map' 3 4 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃) (CategoryTheory.CategoryStruct.comp (g.map' 3 4 ) (CategoryTheory.eqToHom ))) :
                                                                                  f = g
                                                                                  theorem CategoryTheory.ComposableArrows.mk₄_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 4) :
                                                                                  ∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (X₄ : C) (f₀ : X₀ X₁) (f₁ : X₁ X₂) (f₂ : X₂ X₃) (f₃ : X₃ X₄), X = CategoryTheory.ComposableArrows.mk₄ f₀ f₁ f₂ f₃
                                                                                  def CategoryTheory.ComposableArrows.homMk₅ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 )) :
                                                                                  f g

                                                                                  Constructor for morphisms in ComposableArrows C 5.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.ComposableArrows.homMk₅_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 )) :
                                                                                    (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 0 = app₀
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.ComposableArrows.homMk₅_app_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 )) :
                                                                                    (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 1 = app₁
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.ComposableArrows.homMk₅_app_two {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 )) :
                                                                                    (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 2, = app₂
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.ComposableArrows.homMk₅_app_three {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 )) :
                                                                                    (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 3, = app₃
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.ComposableArrows.homMk₅_app_four {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 )) :
                                                                                    (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 4, = app₄
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.ComposableArrows.homMk₅_app_five {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 )) :
                                                                                    (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 5, = app₅
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.ComposableArrows.isoMk₅_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 )) :
                                                                                    (CategoryTheory.ComposableArrows.isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).inv = CategoryTheory.ComposableArrows.homMk₅ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv app₅.inv
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.ComposableArrows.isoMk₅_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 )) :
                                                                                    (CategoryTheory.ComposableArrows.isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).hom = CategoryTheory.ComposableArrows.homMk₅ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom app₅.hom w₀ w₁ w₂ w₃ w₄
                                                                                    def CategoryTheory.ComposableArrows.isoMk₅ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : f.obj' 0 g.obj' 0 ) (app₁ : f.obj' 1 g.obj' 1 ) (app₂ : f.obj' 2 g.obj' 2 ) (app₃ : f.obj' 3 g.obj' 3 ) (app₄ : f.obj' 4 g.obj' 4 ) (app₅ : f.obj' 5 g.obj' 5 ) (w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 )) (w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 )) (w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 )) (w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 )) (w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 )) :
                                                                                    f g

                                                                                    Constructor for isomorphisms in ComposableArrows C 5.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      theorem CategoryTheory.ComposableArrows.ext₅ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (h₀ : f.obj' 0 = g.obj' 0 ) (h₁ : f.obj' 1 = g.obj' 1 ) (h₂ : f.obj' 2 = g.obj' 2 ) (h₃ : f.obj' 3 = g.obj' 3 ) (h₄ : f.obj' 4 = g.obj' 4 ) (h₅ : f.obj' 5 = g.obj' 5 ) (w₀ : f.map' 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (g.map' 0 1 ) (CategoryTheory.eqToHom ))) (w₁ : f.map' 1 2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (g.map' 1 2 ) (CategoryTheory.eqToHom ))) (w₂ : f.map' 2 3 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (g.map' 2 3 ) (CategoryTheory.eqToHom ))) (w₃ : f.map' 3 4 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃) (CategoryTheory.CategoryStruct.comp (g.map' 3 4 ) (CategoryTheory.eqToHom ))) (w₄ : f.map' 4 5 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₄) (CategoryTheory.CategoryStruct.comp (g.map' 4 5 ) (CategoryTheory.eqToHom ))) :
                                                                                      f = g
                                                                                      theorem CategoryTheory.ComposableArrows.mk₅_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 5) :
                                                                                      ∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (X₄ : C) (X₅ : C) (f₀ : X₀ X₁) (f₁ : X₁ X₂) (f₂ : X₂ X₃) (f₃ : X₃ X₄) (f₄ : X₄ X₅), X = CategoryTheory.ComposableArrows.mk₅ f₀ f₁ f₂ f₃ f₄

                                                                                      The ith arrow of F : ComposableArrows C n.

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_exists {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (obj : Fin (n + 1)C) (mapSucc : (i : Fin n) → obj i.castSucc obj i.succ) :
                                                                                        ∃ (F : CategoryTheory.ComposableArrows C n) (e : (i : Fin (n + 1)) → F.obj i obj i), ∀ (i : ) (hi : i < n), mapSucc i, hi = CategoryTheory.CategoryStruct.comp (e i, ).inv (CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) hi) (e i + 1, ).hom)
                                                                                        noncomputable def CategoryTheory.ComposableArrows.mkOfObjOfMapSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (obj : Fin (n + 1)C) (mapSucc : (i : Fin n) → obj i.castSucc obj i.succ) :

                                                                                        Given obj : Fin (n + 1) → C and mapSucc i : obj i.castSucc ⟶ obj i.succ for all i : Fin n, this is F : ComposableArrows C n such that F.obj i is definitionally equal to obj i and such that F.map' i (i + 1) = mapSucc ⟨i, hi⟩.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (obj : Fin (n + 1)C) (mapSucc : (i : Fin n) → obj i.castSucc obj i.succ) (i : Fin (n + 1)) :
                                                                                          theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_map_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (obj : Fin (n + 1)C) (mapSucc : (i : Fin n) → obj i.castSucc obj i.succ) (i : ) (hi : autoParam (i < n) _auto✝) :
                                                                                          (CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).map' i (i + 1) hi = mapSucc i, hi
                                                                                          theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_arrow {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : } (obj : Fin (n + 1)C) (mapSucc : (i : Fin n) → obj i.castSucc obj i.succ) (i : ) (hi : autoParam (i < n) _auto✝) :
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ) (X : CategoryTheory.ComposableArrows Cᵒᵖ n) (X : Fin (n + 1)) :
                                                                                          ((CategoryTheory.ComposableArrows.opEquivalence C n).counitIso.hom.app X✝).app X = X✝.map (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.counitInv.app (Opposite.op X)).unop
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ) (X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ) :
                                                                                          (CategoryTheory.ComposableArrows.opEquivalence C n).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor) (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).inverse.comp .functor).comp (Opposite.unop X)).rightOpLeftOpIso.inv).op ((CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor (Fin (n + 1)) C) => (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc F).symm) ) (CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor (Fin (n + 1))ᵒᵖ C) => ((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.invFunIdAssoc F) )).hom.app (Opposite.unop X)).op
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ) (X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ) :
                                                                                          (CategoryTheory.ComposableArrows.opEquivalence C n).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor (Fin (n + 1)) C) => (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc F).symm) ) (CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor (Fin (n + 1))ᵒᵖ C) => ((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.invFunIdAssoc F) )).inv.app (Opposite.unop X)).op (CategoryTheory.whiskerLeft (.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor) (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).inverse.comp .functor).comp (Opposite.unop X)).rightOpLeftOpIso.hom).op
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ) (X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ) :
                                                                                          ∀ {X_1 Y : Fin (n + 1)} (f : X_1 Y), ((CategoryTheory.ComposableArrows.opEquivalence C n).functor.obj X).map f = ((Opposite.unop X).map (.functor.map (CategoryTheory.homOfLE ))).op
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ) (X : CategoryTheory.ComposableArrows Cᵒᵖ n) (X : Fin (n + 1)) :
                                                                                          ((CategoryTheory.ComposableArrows.opEquivalence C n).counitIso.inv.app X✝).app X = X✝.map (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.counit.app (Opposite.op X)).unop
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.ComposableArrows.opEquivalence_functor_map_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ) :
                                                                                          ∀ {X Y : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ} (f : X Y) (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.opEquivalence C n).functor.map f).app X_1 = (f.unop.app X_1.rev).op

                                                                                          The equivalence (ComposableArrows C n)ᵒᵖ ≌ ComposableArrows Cᵒᵖ n obtained by reversing the arrows.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            theorem CategoryTheory.Functor.mapComposableArrows_map_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (n : ) :
                                                                                            ∀ {X Y : CategoryTheory.Functor (Fin (n + 1)) C} (α : X Y) (X_1 : Fin (n + 1)), ((G.mapComposableArrows n).map α).app X_1 = G.map (α.app X_1)
                                                                                            @[simp]
                                                                                            theorem CategoryTheory.Functor.mapComposableArrows_obj_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (n : ) (F : CategoryTheory.Functor (Fin (n + 1)) C) :
                                                                                            ∀ {X Y : Fin (n + 1)} (f : X Y), ((G.mapComposableArrows n).obj F).map f = G.map (F.map f)
                                                                                            @[simp]
                                                                                            theorem CategoryTheory.Functor.mapComposableArrows_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (n : ) (F : CategoryTheory.Functor (Fin (n + 1)) C) (X : Fin (n + 1)) :
                                                                                            ((G.mapComposableArrows n).obj F).obj X = G.obj (F.obj X)

                                                                                            The functor ComposableArrows C n ⥤ ComposableArrows D n obtained by postcomposition with a functor C ⥤ D.

                                                                                            Equations
                                                                                            Instances For
                                                                                              def CategoryTheory.Functor.mapComposableArrowsOpIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (n : ) :
                                                                                              (G.mapComposableArrows n).comp (CategoryTheory.ComposableArrows.opEquivalence D n).functor.rightOp (CategoryTheory.ComposableArrows.opEquivalence C n).functor.rightOp.comp (G.op.mapComposableArrows n).op

                                                                                              The functor ComposableArrows C n ⥤ ComposableArrows D n induced by G : C ⥤ D commutes with opEquivalence.

                                                                                              Equations
                                                                                              Instances For