abelianImageToKernel_comp_kernel_ι

Mathlib.Algebra.Homology.ShortComplex.Abelian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι

← MathLib Explorer

English

The canonical map from the image of f to the kernel of g is mono.

Русский

Каноническое отображение образа f в ядро g моно.

LaTeX

$$$$ \\operatorname{Mono}\\big( S.abelianImageToKernel \\big). $$$$

Lean4

@[reassoc (attr := simp)]
theorem abelianImageToKernel_comp_kernel_ι : S.abelianImageToKernel ≫ kernel.ι S.g = Abelian.image.ι S.f :=
  kernel.lift_ι _ _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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