English
Let A and B be chain complexes with differentials d^A and d^B, and let f: A ⟶ B be a chain map with components f_i. For all indices i, j with c.Rel i j, the square commutes: f_i ∘ d^A_{i j} = d^B_{i j} ∘ f_j.
Русский
Пусть A и B — цепные комплексы над V с дифференциалами d^A и d^B, и f: A ⟶ B — цепной отображатель с компонентами f_i. Для всех индексов i, j с c.Rel i j диаграмма коммутирует: f_i ∘ d^A_{i j} = d^B_{i j} ∘ f_j.
LaTeX
$$$\\\\forall i \\\\ j \\\\ (c.Rel \\\\ i \\\\ j) \\\\Rightarrow f.f i \\\\\\\\circ d^A_{i j} = d^B_{i j} \\\\\\\\circ f.f j$$$
Lean4
@[reassoc (attr := simp)]
theorem comm {A B : HomologicalComplex V c} (f : A.Hom B) (i j : ι) : f.f i ≫ B.d i j = A.d i j ≫ f.f j :=
by
by_cases hij : c.Rel i j
· exact f.comm' i j hij
· rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
