mk₀_sum — Mathlib

English

Ext in the first variable commutes with biproducts: Ext of a biproduct with Y is equivalent to the product of Exts with each component.

Русский

Ext по первой переменной коммутирует с двупродуктами: Ext X с пучком c становится эквивалентным произведению Ext с каждым компонентом.

LaTeX

$$$\Ext X c.pt n \simeq_+ Π_i, Ext X (X_i) n$$$

Lean4

theorem mk₀_sum {X Y : C} {ι : Type*} [Fintype ι] (f : ι → (X ⟶ Y)) : mk₀ (∑ i, f i) = ∑ i, mk₀ (f i) :=
  map_sum addEquiv₀.symm _ _

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