HasTotal

Mathlib.Algebra.Homology.TotalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex₂.HasTotal

Lean4

/-- A bicomplex has a total bicomplex if for any `i₁₂ : I₁₂`, the coproduct
of the objects `(K.X i₁).X i₂` such that `ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂` exists. -/
abbrev HasTotal :=
  K.toGradedObject.HasMap (ComplexShape.π c₁ c₂ c₁₂)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru