English
There is an epimorphism on the map part of the composable arrows diagram at level 3 for K when K has homology.
Русский
Для диаграммы сопоставимых стрелок на уровне 3 эпиморфизм присутствует, если у K есть гомологии.
LaTeX
$$$\text{epi}((\mathrm{composableArrows}_3 K i j).map' 2 3)$$$
Lean4
/-- The diagram `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j` is exact
when `c.Rel i j`. -/
theorem composableArrows₃_exact [CategoryWithHomology C] : (composableArrows₃ K i j).Exact :=
by
let S := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) (by simp)
let S' := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) (by simp)
let ι : S ⟶ S' :=
{ τ₁ := 𝟙 _
τ₂ := 𝟙 _
τ₃ := K.iCycles j }
have hS : S.Exact := by
rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono ι]
exact S'.exact_of_f_is_kernel (K.homologyIsKernel i j (c.next_eq' hij))
let T := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) (by simp)
let T' := ShortComplex.mk (K.toCycles i j) (K.homologyπ j) (by simp)
let π : T' ⟶ T :=
{ τ₁ := K.pOpcycles i
τ₂ := 𝟙 _
τ₃ := 𝟙 _ }
have hT : T.Exact := by
rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]
exact T'.exact_of_g_is_cokernel (K.homologyIsCokernel i j (c.prev_eq' hij))
apply ComposableArrows.exact_of_δ₀
· exact hS.exact_toComposableArrows
· exact hT.exact_toComposableArrows
