hasKernel

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.HasLeftHomology.hasKernel

English

If S has left homology, then the kernel of g has a kernel (i.e., there exists a kernel object for g).

Русский

Если у S есть левая гомология, существует ядро отображения g.

LaTeX

$$$HasKernel(S.g)$$$

Lean4

theorem hasKernel [S.HasLeftHomology] : HasKernel S.g :=
  ⟨⟨⟨_, S.leftHomologyData.hi⟩⟩⟩

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

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

Разделы

Аффилиация

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