comp_add — Mathlib

English

For all n, there is an additive bijection homAddEquiv: Ext X Y n →+ ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (n : ℤ).

Русский

Для каждого n существует аддитивная биекция homAddEquiv: Ext X Y n →+ ShiftedHom(...)(n : ℤ).

LaTeX

$$$Ext(X,Y,n) \\xrightarrow{\\mathrm{homAddEquiv}} ShiftedHom( (S_0 X), (S_0 Y), n)$$$

Lean4

@[simp]
theorem comp_add (α : Ext X Y n) {m : ℕ} (β₁ β₂ : Ext Y Z m) {p : ℕ} (h : n + m = p) :
    α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h := by letI := HasDerivedCategory.standard C; ext;
  simp [this, add_hom']

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