English
There is a bijection between Hom(X,Y) and Ext X Y 0, realized by sending a morphism f to mk₀ f and conversely by taking the hom-equivalence inverse.
Русский
Существует биекция между Hom(X,Y) и Ext X Y 0, реализованная отображением f ↦ mk₀ f и обратной картой через обратную связку Hom Equiv.
LaTeX
$$$\\operatorname{Hom}(X,Y) \\cong \\operatorname{Ext}(X,Y,0)$ bijectively via f \\mapsto mk_0 f$$
Lean4
theorem mk₀_bijective : Function.Bijective (mk₀ (X := X) (Y := Y)) :=
by
letI := HasDerivedCategory.standard C
have h : (singleFunctor C 0).FullyFaithful := Functor.FullyFaithful.ofFullyFaithful _
let e : (X ⟶ Y) ≃ Ext X Y 0 := (h.homEquiv.trans (ShiftedHom.homEquiv _ (by simp))).trans homEquiv.symm
have he : e.toFun = mk₀ := by
ext f : 1
dsimp [e]
apply homEquiv.injective
apply (Equiv.apply_symm_apply _ _).trans
symm
apply SmallShiftedHom.equiv_mk₀
rw [← he]
exact e.bijective
