English
The long exact sequence of Ext attached to a short exact sequence S is exact in the strong sense when interpreted in the derived setting.
Русский
Длинная точная последовательность Ext, прикрепленная к короткой точной последовательности S, точна в строгом смысле при рассмотрении в производном окружении.
LaTeX
$$$\\mathrm{covariant\\_Sequence\\_exact} = \\text{Exact}$$$
Lean4
@[simp]
theorem extClass_hom [HasDerivedCategory.{w'} C] : hS.extClass.hom = hS.singleδ :=
by
change SmallShiftedHom.equiv W Q hS.extClass = _
dsimp [extClass, SmallShiftedHom.equiv]
erw [SmallHom.equiv_comp, Iso.homToEquiv_apply]
rw [SmallHom.equiv_mkInv, SmallHom.equiv_mk]
dsimp [singleδ, triangleOfSESδ]
rw [Category.assoc, Category.assoc, Category.assoc, singleFunctorsPostcompQIso_hom_hom,
singleFunctorsPostcompQIso_inv_hom, NatTrans.id_app, Category.id_comp, NatTrans.id_app]
simp only [SingleFunctors.postcomp, Functor.comp_obj]
unfold CochainComplex.singleFunctors
rw [Functor.map_id, Category.comp_id]
rfl
