zero_hom — Mathlib

English

The zero extension has zero hom; i.e., 0 ∈ Ext X Y n maps to the zero morphism in the shifted hom space.

Русский

Нулевое расширение имеет нулевой морфизм: ноль в Ext X Y n соответствует нулевому морфизму в shifted-hom пространстве.

LaTeX

$$$0: Ext(X,Y,n)\\to ShiftedHom(\\ldots)\\quad (0) = 0$$$

Lean4

@[simp]
theorem zero_hom : (0 : Ext X Y n).hom = 0 := by
  let β : Ext 0 Y n := 0
  have hβ : β.hom = 0 := by apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src
  have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by simp [β]
  rw [this, comp_hom, hβ, ShiftedHom.comp_zero]

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