ofHom

Mathlib.Algebra.Homology.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#ChainComplex.ofHom

Lean4

/-- A constructor for chain maps between `α`-indexed chain complexes built using `ChainComplex.of`,
from a dependently typed collection of morphisms.
-/
@[simps]
def ofHom (f : ∀ i : α, X i ⟶ Y i) (comm : ∀ i : α, f (i + 1) ≫ d_Y i = d_X i ≫ f i) : of X d_X sq_X ⟶ of Y d_Y sq_Y :=
  { f
    comm' := fun n m => by
      by_cases h : n = m + 1
      · subst h
        simpa using comm m
      · rw [of_d_ne X _ _ h, of_d_ne Y _ _ h]
        simp }

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

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

Разделы

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

Аффилиация

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