Theorems · Theorem · category theory

ComplexShape.assoc

∀ {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) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₁₂ c₃ c]
  [inst_2 : TotalComplexShape c₂ c₃ c₂₃] [inst_3 : TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))

Defined in

Mathlib.Algebra.Homology.ComplexShapeSigns

Cited by

2 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TotalComplexShapeTotalComplexShapeTotalComplexShapeTotalComplexShapeComplexShape.Associative