Theorems · Inductive type · category theory

TotalComplexShapeSymmetry

{I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) →
          (c₁₂ : ComplexShape I₁₂) → [TotalComplexShape c₁ c₂ c₁₂] → [TotalComplexShape c₂ c₁ c₁₂] → Type (max u_1 u_2)

A total complex shape symmetry contains the data and properties which allow the identification of the two total complex functors HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂ and HomologicalComplex₂ C c₂ c₁ ⥤ HomologicalComplex C c₁₂ via the flip.

Defined in

Mathlib.Algebra.Homology.ComplexShapeSigns

Cited by

32 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TotalComplexShapeTotalComplexShape