shortComplex'

Mathlib.Algebra.Homology.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CommSq.shortComplex'

Lean4

/-- The short complex attached to the kernel fork of a commutative square.
(This is similar to `CommSq.shortComplex`, but with different signs.) -/
@[simps]
noncomputable def shortComplex' (sq : CommSq fst snd f g) : ShortComplex C
    where
  f := biprod.lift fst snd
  g := biprod.desc f (-g)
  zero := by simp [sq.w]

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

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

Разделы

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

Аффилиация

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