leftHomologyπ

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.leftHomologyπ

Lean4

/-- The "homology class" map `S.cycles ⟶ S.leftHomology`. -/
noncomputable def leftHomologyπ : S.cycles ⟶ S.leftHomology :=
  S.leftHomologyData.π

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

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

Разделы

Аффилиация

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