ext — Mathlib

English

There is a natural equivalence between Ext X Y n and ShiftedHom of the corresponding singleFunctor objects.

Русский

Существует естественное эквивалентное соответствие между Ext X Y n и ShiftedHom соответствующих объектов одиночного функторa.

LaTeX

$${n : Nat} : Equiv (Ext X Y n) (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) n.cast)$$

Lean4

@[ext]
theorem ext {n : ℕ} {α β : Ext X Y n} (h : α.hom = β.hom) : α = β :=
  homEquiv.injective h

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