English
Changing universes via SmallShiftedHom preserves the homEquiv identification of Ext: the homEquiv after a universe change equals the original homEquiv.
Русский
При смене вселенных через SmallShiftedHom идентификация homEquiv сохраняется: после смены вселенной совпадает с исходной homEquiv.
LaTeX
$$$homEquiv(\chgUniv(e)) = homEquiv(e)$$$
Lean4
/-- `Ext` commutes with biproducts in its second variable. -/
noncomputable def addEquivBiproduct (X : C) {J : Type*} [Fintype J] {Y : J → C} {c : Bicone Y} (hc : c.IsBilimit)
(n : ℕ) : Ext X c.pt n ≃+ Π i, Ext X (Y i) n
where
toFun e i := e.comp (Ext.mk₀ (c.π i)) (add_zero n)
invFun e := ∑ (i : J), (e i).comp (Ext.mk₀ (c.ι i)) (add_zero n)
left_inv
_ := by
simp only [comp_assoc_of_second_deg_zero, mk₀_comp_mk₀, ← Ext.comp_sum, ← Ext.mk₀_sum, IsBilimit.total hc,
comp_mk₀_id]
right_inv
_ := by
ext i
simp only [Ext.sum_comp, comp_assoc_of_second_deg_zero, mk₀_comp_mk₀]
rw [Finset.sum_eq_single i _ (by simp), bicone_ι_π_self, comp_mk₀_id]
intro _ _ hij
rw [c.ι_π, dif_neg hij, mk₀_zero, comp_zero]
map_add' _ _ := by simp only [add_comp, Pi.add_def]
