addEquiv₀ — Mathlib

English

There is an additive bijection homAddEquiv between Ext X Y n and ShiftedHom ... establishing a natural isomorphism compatible with addition.

Русский

Существуют аддитивная биекция между Ext X Y n и ShiftedHom, задающая естественное тождество, совместимое с сложением.

LaTeX

$$$Ext(X,Y,n) \\simeq_+ ShiftedHom((S X),(S Y),n)$$$

Lean4

/-- The additive bijection `Ext X Y 0 ≃+ (X ⟶ Y)`. -/
@[simps! symm_apply]
noncomputable def addEquiv₀ : Ext X Y 0 ≃+ (X ⟶ Y)
    where
  toEquiv := homEquiv₀
  map_add' x y := by apply homEquiv₀.symm.injective (by simp [mk₀_add])

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