ofExactOfSection

Mathlib.Algebra.Homology.ShortComplex.Exact

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

Lean4

/-- This is the splitting of a short complex `S` in a balanced category induced by
a section of the morphism `S.g : S.X₂ ⟶ S.X₃` -/
noncomputable def ofExactOfSection (S : ShortComplex C) (hS : S.Exact) (s : S.X₃ ⟶ S.X₂) (s_g : s ≫ S.g = 𝟙 S.X₃)
    (hf : Mono S.f) : S.Splitting
    where
  r := hS.lift (𝟙 S.X₂ - S.g ≫ s) (by simp [s_g])
  s := s
  f_r := by rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id, zero_assoc, zero_comp, sub_zero, id_comp]
  s_g := s_g

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

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

Разделы

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

Аффилиация

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