Theorems · Inductive type · category theory

TotalComplexShape

{I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} → ComplexShape I₁ → ComplexShape I₂ → ComplexShape I₁₂ → Type (max (max u_1 u_2) u_4)

A total complex shape for three complex shapes c₁, c₂, c₁₂ on three types I₁, I₂ and I₁₂ consists of the data and properties that will allow the construction of a total complex functor HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂ which sends K to a complex which in degree i₁₂ : I₁₂ consists of the coproduct of the (K.X i₁).X i₂ such that π ⟨i₁, i₂⟩ = i₁₂.

Defined in

Mathlib.Algebra.Homology.ComplexShapeSigns

Cited by

210 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms