English
There is a canonical morphism hom' from Ext X Y n to ShiftedHom obtained by transporting α ∈ Ext X Y n to the shifted hom space via the constructed derived-category functors.
Русский
Существует канонический морфизм hom' от Ext X Y n к ShiftedHom, получаемый переводом α в соответствующее пространство смещённых морфизмов через построенные производные functor.
LaTeX
$$$\\mathrm{hom'}(\\alpha) : \\text{ShiftedHom}( (singleFunctor C 0)\\!\\mathrm{obj} X, (singleFunctor C 0)\\!\\mathrm obj Y, n) $$$
Lean4
/-- The map from `Ext X Y n` to a `ShiftedHom` type in the *constructed* derived
category given by `HasDerivedCategory.standard`: this definition is introduced
only in order to prove properties of the abelian group structure on `Ext`-groups.
Do not use this definition: use the more general `hom` instead. -/
noncomputable abbrev hom' (α : Ext X Y n) :
letI := HasDerivedCategory.standard C
ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (n : ℤ) :=
letI := HasDerivedCategory.standard C
α.hom
