map

Mathlib.Algebra.Homology.ShortComplex.Exact

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

Lean4

/-- If a short complex `S` has a splitting and `F` is an additive functor, then
`S.map F` also has a splitting. -/
@[simps]
def map (s : S.Splitting) (F : C ⥤ D) [F.Additive] : (S.map F).Splitting
    where
  r := F.map s.r
  s := F.map s.s
  f_r := by
    dsimp [ShortComplex.map]
    rw [← F.map_comp, f_r, F.map_id]
  s_g := by
    dsimp [ShortComplex.map]
    simp only [← F.map_comp, s_g, F.map_id]
  id := by
    dsimp [ShortComplex.map]
    simp only [← F.map_id, ← s.id, Functor.map_comp, Functor.map_add]

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

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

Разделы

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

Аффилиация

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