homEquiv₀ — Mathlib

English

There is a canonical equivalence homEquiv₀: Ext X Y 0 ≃ (X ⟶ Y); this is the defining bijection between degree-zero Ext and morphisms.

Русский

Существует каноническое эквивалентность homEquiv₀: Ext X Y 0 ≃ (X ⟶ Y); это определяющая биекция между Ext нулевой степени и морфизмами.

LaTeX

$$$\\mathrm{homEquiv}_0 : Ext(X,Y,0) \\simeq \\operatorname{Hom}(X,Y)$$$

Lean4

/-- The bijection `Ext X Y 0 ≃ (X ⟶ Y)`. -/
@[simps! symm_apply]
noncomputable def homEquiv₀ : Ext X Y 0 ≃ (X ⟶ Y) :=
  (Equiv.ofBijective _ (mk₀_bijective X Y)).symm

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