_example

Mathlib.Algebra.Homology.Monoidal

URI: https://scilib.ai/kg/mathlib#HomologicalComplex._example

Lean4

noncomputable example {D : Type*} [Category D] [Preadditive D] [MonoidalCategory D] [HasZeroObject D]
    [HasFiniteCoproducts D] [((curriedTensor D).Additive)] [∀ (X : D), (((curriedTensor D).obj X).Additive)]
    [∀ (X : D), PreservesFiniteCoproducts ((curriedTensor D).obj X)]
    [∀ (X : D), PreservesFiniteCoproducts ((curriedTensor D).flip.obj X)] : MonoidalCategory (ChainComplex D ℕ) :=
  inferInstance

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

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

Разделы

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

Аффилиация

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