homAddEquiv — Mathlib

English

The additive equivalence homAddEquiv is compatible with the underlying coe; it preserves addition via the hom-equivalence to ShiftedHom.

Русский

Аддитивная эквивалентность homAddEquiv совместима с базовым отображением; она сохраняет сложение через эквивалентность гом к ShiftedHom.

LaTeX

$$$\\mathrm{homAddEquiv} : Ext(X,Y,n) \\to_+ ShiftedHom(...)$ and its coherence with addition$$

Lean4

/-- When an instance of `[HasDerivedCategory.{w'} C]` is available, this is the additive
bijection between `Ext.{w} X Y n` and a type of morphisms in the derived category. -/
noncomputable def homAddEquiv {n : ℕ} :
    Ext.{w} X Y n ≃+ ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (n : ℤ)
    where
  toEquiv := homEquiv
  map_add' := by simp

Похожие утверждения