kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage

Mathlib.Algebra.Homology.ShortComplex.Abelian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage

English

S.Exact is equivalent to Function.Exact f g.

Русский

Tочность S эквивалентна точности функций f и g: Function.Exact f g.

LaTeX

$$$$ S.Exact \\iff \\mathrm{Function.Exact}(f,g). $$$$

Lean4

theorem kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage :
    (kernel.ι S.g ≫ cokernel.π S.f) ≫ S.cokernelToAbelianCoimage = 0 := by simp

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

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

Разделы

Аффилиация

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