English
In a short exact sequence of complexes, the boundary map δ interacts with the cycles maps in a natural way, yielding a commutative relation after transporting along homology π.
Русский
В короткой точной последовательности комплексов граница δ совместима с отображениями циклов и сохраняет каноническую совместимость после применения гомологий.
LaTeX
$$$(HomologicalComplex).\\delta\\_{i,j,hij}\\circ (S^X_3.homology\\pi_i)\\circ (S^X_3.cyclesMk\\,x_3\\,j\\,\\cdot) = (S^X_1.homology\\pi_j)\\circ (S^X_1.cyclesMk\\,x_1\\,k\\,hk\\,\\cdot).$$$
Lean4
/-- In the short exact sequence of complexes
```
0 0 0
| | |
v v v
...-> X_1,i -----> X_1,j --d--> X_1,k ->...
| | |
| f | |
v v v
...-> X_2,i --d--> X_2,j -----> X_2,k ->...
| | |
v v v
...-> X_3,i -----> X_3,j -----> X_3,k ->...
| | |
v v v
0 0 0
```
if `x₁ ∈ X_1,j` and `x₂ ∈ X_2,i` and if `f(x₁) = d(x₂)` then `d(x₁) = 0`. -/
theorem d_eq_zero_of_f_eq_d_apply (x₂ : ((forget₂ C Ab).obj (S.X₂.X i))) (x₁ : ((forget₂ C Ab).obj (S.X₁.X j)))
(hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂) (k : ι) :
((forget₂ C Ab).map (S.X₁.d j k)) x₁ = 0 := by
have := hS.mono_f
apply (Preadditive.mono_iff_injective (S.f.f k)).1 inferInstance
rw [← ConcreteCategory.forget₂_comp_apply, ← HomologicalComplex.Hom.comm, ConcreteCategory.forget₂_comp_apply, hx₁, ←
ConcreteCategory.forget₂_comp_apply, HomologicalComplex.d_comp_d, Functor.map_zero, map_zero]
rfl
