Theorems · Definition · category theory

ComplexShape.r

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

The map I₁ × I₂ × I₃ → j that is obtained using TotalComplexShape c₁ c₂ c₁₂ and TotalComplexShape c₁₂ c₃ c when c₁ : ComplexShape I₁, c₂ : ComplexShape I₂, c₃ : ComplexShape I₃, c₁₂ : ComplexShape I₁₂ and c : ComplexShape J.

Defined in

Mathlib.Algebra.Homology.ComplexShapeSigns

Cited by

35 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TotalComplexShapeTotalComplexShape