Structures · Algebra
ComplexShape.Associative
When we have six complex shapes c₁, c₂, c₃, c₁₂, c₂₃, c, and total functors
HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂,
HomologicalComplex₂ C c₁₂ c₃ ⥤ HomologicalComplex C c,
HomologicalComplex₂ C c₂ c₃ ⥤ HomologicalComplex C c₂₃,
HomologicalComplex₂ C c₁ c₂₂₃ ⥤ HomologicalComplex C c, we get two ways to
compute the total complex of a triple complex in HomologicalComplex₃ C c₁ c₂ c₃, then
under this assumption [Associative c₁ c₂ c₃ c₁₂ c₂₃ c], these two complexes
canonically identify (without introducing signs).
- Shape
- 6 explicit arguments · adds assoc, ε₁_eq_mul, ε₂_ε₁, ε₂_eq_mul
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 by58
- HomologicalComplex.HasGoodTrifunctor₂₃Obj
- HomologicalComplex.mapBifunctor₂₃.ιOrZero
- HomologicalComplex.mapBifunctor₂₃.ι
- HomologicalComplex.mapBifunctorAssociatorX
- HomologicalComplex.mapBifunctor₂₃.d₂
- HomologicalComplex.mapBifunctor₂₃.d₃
- HomologicalComplex.mapBifunctor₂₃.d₁
- HomologicalComplex.mapBifunctor₂₃.D₂
- HomologicalComplex.mapBifunctor₂₃.D₃
- HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom
- HomologicalComplex.mapBifunctor₂₃.ιOrZero_eq_zero
- HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc
- HomologicalComplex.mapBifunctor₂₃.ιOrZero_eq
- HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctor₂₃Desc
- HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc
- HomologicalComplex.mapBifunctor₂₃.ι_D₂
- HomologicalComplex.mapBifunctor₂₃.ι_D₃
- HomologicalComplex.mapBifunctor₂₃.ι_D₁
- HomologicalComplex.mapBifunctor₂₃.d₁_eq
- HomologicalComplex.mapBifunctor₂₃.d₂_eq
- HomologicalComplex.mapBifunctor₂₃.ι_eq
- HomologicalComplex.mapBifunctor₂₃.d₃_eq
- HomologicalComplex.mapBifunctor₂₃.d₃_eq_zero
- HomologicalComplex.mapBifunctor₂₃.d₁_eq_zero
- HomologicalComplex.mapBifunctor₂₃.d₂_eq_zero
- HomologicalComplex.ι_mapBifunctorAssociatorX_hom
- ComplexShape.assoc
- ComplexShape.Associative.assoc
- HomologicalComplex.mapBifunctor₂₃.hom_ext
- ComplexShape.associative_ε₂_eq_mul
- ComplexShape.associative_ε₂_ε₁
- ComplexShape.associative_ε₁_eq_mul
- ComplexShape.Associative.ε₂_eq_mul
- ComplexShape.ρ₂₃
- HomologicalComplex.mapBifunctorAssociatorX_hom_D₂
- ComplexShape.Associative.ε₁_eq_mul
- HomologicalComplex.mapBifunctorAssociatorX_hom_D₁
- ComplexShape.Associative.ε₂_ε₁
- HomologicalComplex.mapBifunctorAssociatorX_hom_D₃
- HomologicalComplex.mapBifunctorAssociatorX_hom_D₃_assoc
- HomologicalComplex.mapBifunctor₂₃.ιOrZero.congr_simp
- HomologicalComplex.mapBifunctor₂₃.d₃.congr_simp
- HomologicalComplex.mapBifunctor₂₃.D₂.congr_simp
- HomologicalComplex.mapBifunctor₂₃.d_eq
- HomologicalComplex.mapBifunctorAssociator
- HomologicalComplex.mapBifunctorAssociatorX.congr_simp
- HomologicalComplex.mapBifunctor₂₃.ι_D₂_assoc
- HomologicalComplex.mapBifunctor₂₃.ι_D₁_assoc
- HomologicalComplex.mapBifunctorAssociatorX_hom_D₁_assoc
- HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc.congr_simp
Ancestors0
No ancestors.