map_f'

Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.LeftHomologyData.map_f'

English

The map f' after applying F matches the image of f' under F.

Русский

После применения F карта f' совпадает с изображением f' через F.

LaTeX

$$$(h.map F).f' = F.map(h.f')$$$

Lean4

@[simp]
theorem map_f' : (h.map F).f' = F.map h.f' := by rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]

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

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

Разделы

Аффилиация

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