English
Alternative formulation of covariant_sequence_exact₂'. The constructed five-term short exact system built from the S.f and S.g maps, together with hS.extClass, is exact in the abelian sense.
Русский
Альтернативная формулировка covariant_sequence_exact₂'. Построенная пятиступенная точная система, составленная из отображений S.f, S.g и extClass hS, является точной в абелевой категории.
LaTeX
$$$\\big(\\mathrm{ShortComplex.mk}(\\mathrm{AddCommGrpCat.ofHom}((mk_0 S.f).postcomp X (add_zero n_0)),\\; \\mathrm{AddCommGrpCat.ofHom}((mk_0 S.g).postcomp X (add_zero n_0)),\\; \\text{proof})\\big).\\mathrm{Exact}$$$
Lean4
/-- Alternative formulation of `covariant_sequence_exact₂` -/
theorem covariant_sequence_exact₂' (n : ℕ) :
(ShortComplex.mk (AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X (add_zero n)))
(AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X (add_zero n)))
(by
ext x
dsimp
simp only [comp_assoc_of_third_deg_zero, mk₀_comp_mk₀, ShortComplex.zero, mk₀_zero, comp_zero])).Exact :=
by
letI := HasDerivedCategory.standard C
have :=
(preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₂ _
(hS.singleTriangle_distinguished) n
rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
apply
Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv) (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv)
(H := this)
all_goals ext x; apply hom_comp_singleFunctor_map_shift (C := C)
