English
Let C be an abelian category with a derived category. For every morphism f: X → Y, the hom component of the extension mk₀ f is the shifted-hom element given by ShiftedHom.mk₀ applied to the image of f under the 0-th derived functor, i.e. mk₀ f .hom equals ShiftedHom.mk₀ _ (proof) ((singleFunctor C 0).map f).
Русский
Пусть C — абелова категория с производным образом. Для любой стрелки f: X → Y гом-компонента расширения mk₀ f равна соответствующему элементу в shifted-hom, полученному из отображения f под нулевой производной functor: mk₀ f .hom = ShiftedHom.mk₀ _ (доказательство) ((singleFunctor C 0).map f).
LaTeX
$$$ (mk_0 f).hom = \\mathrm{ShiftedHom.mk_0}\\_{ }\\,\\_\\, ((\\text{singleFunctor } C\\ 0).map\\ f) $$$
Lean4
@[simp]
theorem mk₀_hom [HasDerivedCategory.{w'} C] (f : X ⟶ Y) :
(mk₀ f).hom = ShiftedHom.mk₀ _ (by simp) ((singleFunctor C 0).map f) := by apply SmallShiftedHom.equiv_mk₀
