Theorems · Inductive type · category theory

ComplexShape.Associative

{I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {I₁₂ : Type u_4} →
        {I₂₃ : Type u_5} →
          {J : Type u_6} →
            (c₁ : ComplexShape I₁) →
              (c₂ : ComplexShape I₂) →
                (c₃ : ComplexShape I₃) →
                  (c₁₂ : ComplexShape I₁₂) →
                    (c₂₃ : ComplexShape I₂₃) →
                      (c : ComplexShape J) →
                        [TotalComplexShape c₁ c₂ c₁₂] →
                          [TotalComplexShape c₁₂ c₃ c] →
                            [TotalComplexShape c₂ c₃ c₂₃] → [TotalComplexShape c₁ c₂₃ c] → Prop

When we have six complex shapes c₁, c₂, c₃, c₁₂, c₂₃, c, and total functors HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂, HomologicalComplex₂ C c₁₂ c₃ ⥤ HomologicalComplex C c, HomologicalComplex₂ C c₂ c₃ ⥤ HomologicalComplex C c₂₃, HomologicalComplex₂ C c₁ c₂₂₃ ⥤ HomologicalComplex C c, we get two ways to compute the total complex of a triple complex in HomologicalComplex₃ C c₁ c₂ c₃, then under this assumption [Associative c₁ c₂ c₃ c₁₂ c₂₃ c], these two complexes canonically identify (without introducing signs).

Defined in

Mathlib.Algebra.Homology.ComplexShapeSigns

Cited by

46 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TotalComplexShapeTotalComplexShapeTotalComplexShapeTotalComplexShape