English
In a biproduct X₁ ⊞ X₂, Ext behaves in a compatible way with projections, i.e., if two Ext elements agree after composing with the left projection, they agree after composing with the right projection, hence α = β.
Русский
В биобразной конструкции X₁ ⊞ X₂ Ext распадается предсказуемо по проекциям; если два элемента Ext совпадают после композиции с левой проекцией, то они совпадают и по правой проекции, следовательно α = β.
LaTeX
$$biprod_ext: (mk₀ biprod.inl).comp α = (mk₀ biprod.inl).comp β → (mk₀ biprod.inr).comp α = (mk₀ biprod.inr).comp β → α = β$$
Lean4
theorem biprod_ext {X₁ X₂ : C} {α β : Ext (X₁ ⊞ X₂) Y n}
(h₁ : (mk₀ biprod.inl).comp α (zero_add n) = (mk₀ biprod.inl).comp β (zero_add n))
(h₂ : (mk₀ biprod.inr).comp α (zero_add n) = (mk₀ biprod.inr).comp β (zero_add n)) : α = β :=
by
letI := HasDerivedCategory.standard C
rw [Ext.ext_iff] at h₁ h₂ ⊢
simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp] at h₁ h₂
apply
BinaryCofan.IsColimit.hom_ext
(isBinaryBilimitOfPreserves (singleFunctor C 0) (BinaryBiproduct.isBilimit X₁ X₂)).isColimit
all_goals assumption
