Mathlib Map

Structures · Algebra

TotalComplexShape

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
Shape
3 explicit arguments · adds π, ε₁, ε₂, rel₁, rel₂, ε₂_ε₁

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by273

Ancestors0

No ancestors.