Documentation

Mathlib.CategoryTheory.ComposableArrows.Four

API for compositions of four arrows #

Given morphisms f₁ : i₀ ⟶ i₁, f₂ : i₁ ⟶ i₂, f₃ : i₂ ⟶ i₃, f₄ : i₃ ⟶ i₄, and their compositions f₁₂ : i₀ ⟶ i₂, f₂₃ : i₁ ⟶ i₃ and f₃₄ : i₂ ⟶ i₄, we define maps ComposableArrows.fourδ₄Toδ₃ : mk₃ f₁ f₂ f₃ ⟶ mk₂ f₁ f₂ f₃₄, fourδ₃Toδ₂ : mk₃ f₁ f₂ f₃₄ ⟶ mk₂ f₁ f₂₃ f₄, fourδ₂Toδ₁ : mk₃ f₁ f₂₃ f₄ ⟶ mk₂ f₁₂ f₃ f₄, and fourδ₁Toδ₀ : mk₃ f₁₂ f₃ f₄ ⟶ mk₂ f₂ f₃ f₄. The names are justified by the fact that ComposableArrow.mk₄ f₁ f₂ f₃ f₄ can be thought of as a 4-simplex in the simplicial set nerve C, and its faces (numbered from 0 to 4) are respectively mk₂ f₂ f₃ f₄, mk₂ f₁₂ f₃ f₄, mk₂ f₁ f₂₃ f₄, mk₂ f₁ f₂ f₃₄ and mk₂ f₁ f₂ f₃.

source
def CategoryTheory.ComposableArrows.fourδ₄Toδ₃ {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄ := by cat_disch) :
mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃₄

The morphism mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃₄ when f₃ ≫ f₃ = f₃₄.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def CategoryTheory.ComposableArrows.fourδ₃Toδ₂ {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃ := by cat_disch) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄ := by cat_disch) :
    mk₃ f₁ f₂ f₃₄ ⟶ mk₃ f₁ f₂₃ f₄

    The morphism mk₃ f₁ f₂ f₃₄ ⟶ mk₃ f₁ f₂₃ f₄ when f₂ ≫ f₂ = f₂₃ and f₃ ≫ f₃ = f₃₄.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.ComposableArrows.fourδ₂Toδ₁ {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂ := by cat_disch) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃ := by cat_disch) :
      mk₃ f₁ f₂₃ f₄ ⟶ mk₃ f₁₂ f₃ f₄

      The morphism mk₃ f₁ f₂₃ f₄ ⟶ mk₃ f₁₂ f₃ f₄ when f₁ ≫ f₂ = f₁₂ and f₂ ≫ f₂ = f₂₃.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CategoryTheory.ComposableArrows.fourδ₁Toδ₀ {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂ := by cat_disch) :
        mk₃ f₁₂ f₃ f₄ ⟶ mk₃ f₂ f₃ f₄

        The morphism mk₃ f₁₂ f₃ f₄ ⟶ mk₃ f₂ f₃ f₄ when f₁ ≫ f₂ = f₁₂.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) :
          (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 0 = CategoryStruct.id ((mk₃ f₁ f₂ f₃).obj 0)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_one {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) :
          (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 1 = CategoryStruct.id ((mk₃ f₁ f₂ f₃).obj 1)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_two {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) :
          (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 2 = CategoryStruct.id ((mk₃ f₁ f₂ f₃).obj 2)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_three {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) :
          (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 3 = f₄
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) :
          (fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 0 = CategoryStruct.id ((mk₃ f₁ f₂ f₃₄).obj 0)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_one {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) :
          (fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 1 = CategoryStruct.id ((mk₃ f₁ f₂ f₃₄).obj 1)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_two {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) :
          (fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 2 = f₃
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_three {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) :
          (fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 3 = CategoryStruct.id ((mk₃ f₁ f₂ f₃₄).obj 3)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) :
          (fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 0 = CategoryStruct.id ((mk₃ f₁ f₂₃ f₄).obj 0)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_one {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) :
          (fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 1 = f₂
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_two {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) :
          (fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 2 = CategoryStruct.id ((mk₃ f₁ f₂₃ f₄).obj 2)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_three {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) :
          (fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 3 = CategoryStruct.id ((mk₃ f₁ f₂₃ f₄).obj 3)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) :
          (fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 0 = f₁
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_one {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) :
          (fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 1 = CategoryStruct.id ((mk₃ f₁₂ f₃ f₄).obj 1)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_two {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) :
          (fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 2 = CategoryStruct.id ((mk₃ f₁₂ f₃ f₄).obj 2)
          source
          @[simp]
          theorem CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_three {C : Type u_1} [Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) :
          (fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 3 = CategoryStruct.id ((mk₃ f₁₂ f₃ f₄).obj 3)
          source
          @[reducible, inline]
          abbrev CategoryTheory.ComposableArrows.fourδ₄Toδ₃' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ i₃ i₄ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) :
          mk₃ (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE hi₂₃) ⟶ mk₃ (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE ⋯)

          Variant of fourδ₄Toδ₃ for preorders.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[reducible, inline]
            abbrev CategoryTheory.ComposableArrows.fourδ₃Toδ₂' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ i₃ i₄ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) :
            mk₃ (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE ⋯) ⟶ mk₃ (homOfLE hi₀₁) (homOfLE ⋯) (homOfLE hi₃₄)

            Variant of fourδ₃Toδ₂ for preorders.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[reducible, inline]
              abbrev CategoryTheory.ComposableArrows.fourδ₂Toδ₁' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ i₃ i₄ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) :
              mk₃ (homOfLE hi₀₁) (homOfLE ⋯) (homOfLE hi₃₄) ⟶ mk₃ (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄)

              Variant of fourδ₂Toδ₁ for preorders.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[reducible, inline]
                abbrev CategoryTheory.ComposableArrows.fourδ₁Toδ₀' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ i₃ i₄ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) :
                mk₃ (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) ⟶ mk₃ (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE hi₃₄)

                Variant of fourδ₁Toδ₀ for preorders.

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