canonical

Mathlib.Algebra.Homology.ShortComplex.Homology

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

Lean4

/-- Given a short complex `S` such that `S.HasHomology`, this is the canonical
left homology data for `S` whose `K` and `H` fields are
respectively `S.cycles` and `S.homology`. -/
@[simps!]
noncomputable def canonical [S.HasHomology] : S.LeftHomologyData
    where
  K := S.cycles
  H := S.homology
  i := S.iCycles
  π := S.homologyπ
  wi := by simp
  hi := S.cyclesIsKernel
  wπ := S.toCycles_comp_homologyπ
  hπ := S.homologyIsCokernel

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

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

Разделы

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

Аффилиация

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