ofHasKernelOfHasCokernel

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

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

Lean4

/-- The chosen kernels and cokernels of the limits API give a `LeftHomologyData` -/
@[simps]
noncomputable def ofHasKernelOfHasCokernel [HasKernel S.g] [HasCokernel (kernel.lift S.g S.f S.zero)] :
    S.LeftHomologyData where
  K := kernel S.g
  H := cokernel (kernel.lift S.g S.f S.zero)
  i := kernel.ι _
  π := cokernel.π _
  wi := kernel.condition _
  hi := kernelIsKernel _
  wπ := cokernel.condition _
  hπ := cokernelIsCokernel _

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

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

Разделы

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

Аффилиация

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