extClass — Mathlib

English

Compatibility: the Ext-class extClass composes with a morphism to produce the zero morphism on the given second component.

Русский

Совместимость: Ext-класс extClass компонируется с морфизмом так, чтобы получить нулевой морфизм на второй компоненте.

LaTeX

$$$(\\mathrm{Ext.mk}_0 S.g)\\circ (\\mathrm{extClass})\\circ (0) = 0$$$

Lean4

/-- The class in `Ext S.X₃ S.X₁ 1` that is attached to a short exact
short complex `S` in an abelian category. -/
noncomputable def extClass : Ext.{w} S.X₃ S.X₁ 1 :=
  by
  have := hS.hasSmallLocalizedHom_S'_X₃_K
  have := hS.hasSmallLocalizedShiftedHom_K_S'_X₁
  change SmallHom W (S').X₃ ((S').X₁⟦(1 : ℤ)⟧)
  exact (SmallHom.mkInv qis hqis).comp (SmallHom.mk W δ)

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