instEpiOpcyclesMapOfF

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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

English

The homology map of the identity on K is the identity on K's homology.

Русский

Гомологическое отображение тождества на K равно тождественному отображению на гомологии K.

LaTeX

$$\mathrm{homologyMap}(\mathrm{Id}_K)\!\, i = \mathrm{Id}_{K\text{.homology}}$$

Lean4

instance [Epi (φ.f i)] : Epi (opcyclesMap φ i) :=
  epi_of_epi_fac (p_opcyclesMap φ i)

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

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

Разделы

Аффилиация

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