English
Summing morphisms inside Ext via mk0 commutes with Ext mk0: the Ext of a sum of maps equals the sum of Exts of each map.
Русский
Суммирование отображений внутри Ext через mk0 сохраняется: Ext сумм отображений равен сумме Ext от каждого отображения.
LaTeX
$$$\Ext^0(X\,,\,Y,\sum_i f_i) = \sum_i Ext^0(X\,,\,Y, f_i)$$$
Lean4
/-- `Ext` commutes with biproducts in its first variable. -/
noncomputable def biproductAddEquiv {J : Type*} [Fintype J] {X : J → C} {c : Bicone X} (hc : c.IsBilimit) (Y : C)
(n : ℕ) : Ext c.pt Y n ≃+ Π i, Ext (X i) Y n
where
toFun e i := (Ext.mk₀ (c.ι i)).comp e (zero_add n)
invFun e := ∑ (i : J), (Ext.mk₀ (c.π i)).comp (e i) (zero_add n)
left_inv
x := by
simp only [← comp_assoc_of_second_deg_zero, mk₀_comp_mk₀]
rw [← Ext.sum_comp, ← Ext.mk₀_sum, IsBilimit.total hc, mk₀_id_comp]
right_inv
_ := by
ext i
simp only [Ext.comp_sum, ← comp_assoc_of_second_deg_zero, mk₀_comp_mk₀]
rw [Finset.sum_eq_single i _ (by simp), bicone_ι_π_self, mk₀_id_comp]
intro _ _ hij
rw [c.ι_π, dif_neg hij.symm, mk₀_zero, zero_comp]
map_add' _ _ := by simp only [comp_add, Pi.add_def]
