ofExactOfRetraction

Mathlib.Algebra.Homology.ShortComplex.Exact

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

Lean4

/-- This is the splitting of a short complex `S` in a balanced category induced by
a retraction of the morphism `S.f : S.X₁ ⟶ S.X₂` -/
noncomputable def ofExactOfRetraction (S : ShortComplex C) (hS : S.Exact) (r : S.X₂ ⟶ S.X₁) (f_r : S.f ≫ r = 𝟙 S.X₁)
    (hg : Epi S.g) : S.Splitting where
  r := r
  s := hS.desc (𝟙 S.X₂ - r ≫ S.f) (by simp [reassoc_of% f_r])
  f_r := f_r
  s_g := by rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero, comp_zero, sub_zero, comp_id]

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

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

Разделы

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

Аффилиация

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