s_r

Mathlib.Algebra.Homology.ShortComplex.Exact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.Splitting.s_r

← MathLib Explorer

English

The object X₂ is zero if and only if f = 0 and g = 0.

Русский

Объект X₂ нулевой тогда и только тогда, когда f = 0 и g = 0.

LaTeX

$$\mathrm{IsZero}(S.X_2) \iff (S.f = 0 \land S.g = 0)$$

Lean4

@[reassoc (attr := simp)]
theorem s_r (s : S.Splitting) : s.s ≫ s.r = 0 := by
  have := s.epi_g
  simp only [← cancel_epi S.g, comp_zero, g_s_assoc, sub_comp, id_comp, assoc, f_r, comp_id, sub_self]

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

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

Разделы

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

Аффилиация

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