moduleCatLeftHomologyData_f'_hom

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom

English

The morphism associated to f' in the left homology data equals the canonical map to cycles.

Русский

Отображение f' в левых данных гомологии равно каноническому отображению в циклы.

LaTeX

$$moduleCatLeftHomologyData.f'.hom = moduleCatToCycles$$

Lean4

@[simp]
theorem moduleCatLeftHomologyData_f'_hom : S.moduleCatLeftHomologyData.f'.hom = S.moduleCatToCycles :=
  rfl

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

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

Разделы

Аффилиация

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