hι'

Mathlib.Algebra.Homology.ShortComplex.RightHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.RightHomologyData.hι'

Lean4

/-- For `h : S.RightHomologyData`, this is a restatement of `h.hι`, saying that
`ι : h.H ⟶ h.Q` is a kernel of `h.g' : h.Q ⟶ S.X₃`. -/
def hι' : IsLimit (KernelFork.ofι h.ι h.ι_g') :=
  h.hι

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

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

Разделы

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

Аффилиация

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