instPreservesZeroMorphismsEval

Mathlib.Algebra.Homology.HomologicalComplex

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

English

For each index i, the evaluation functor at i preserves zero morphisms from the chain complex category to V.

Русский

Для каждого индекса i функтор оценки в i сохраняет переходы нулевых морфизмов из категории цепных комплексов в V.

LaTeX

$$$\\\\text{(eval } V c i).PreservesZeroMorphisms$$$

Lean4

instance (i : ι) : (eval V c i).PreservesZeroMorphisms where

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

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

Разделы

Аффилиация

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