English
Let S be a ShortComplex of a sequence of HomologicalComplexes in an abelian category. For each index i, the induced sequence H_i(S.X1) → H_i(S.X2) → H_i(S.X3) is exact.
Русский
Пусть S — короткий комплекс последовательности гомологических комплексов в абелеовой категории. Для каждого индекса i последовательность H_i(S.X1) → H_i(S.X2) → H_i(S.X3) точна.
LaTeX
$$$\\operatorname{Im}\\big(HomologicalComplex.homologyMap\\, S.f\\, i\\big) = \\ker\\big(HomologicalComplex.homologyMap\\, S.g\\, i\\big)$$$
Lean4
/-- Exactness of `S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i`. -/
theorem homology_exact₂ :
(ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i)
(by rw [← HomologicalComplex.homologyMap_comp, S.zero, HomologicalComplex.homologyMap_zero])).Exact :=
by
by_cases h : c.Rel i (c.next i)
· exact (snakeInput hS i _ h).L₀_exact
· have := hS.epi_g
have : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i) := fun K =>
ShortComplex.isIso_homologyι (K.sc i) (K.shape _ _ h)
have e : S.map (HomologicalComplex.homologyFunctor C c i) ≅ S.map (HomologicalComplex.opcyclesFunctor C c i) :=
ShortComplex.isoMk (asIso (S.X₁.homologyι i)) (asIso (S.X₂.homologyι i)) (asIso (S.X₃.homologyι i)) (by simp)
(by simp)
exact ShortComplex.exact_of_iso e.symm (opcycles_right_exact S hS.exact i)
