English
Let φ be a family of zero homomorphisms φ_i: β_i → γ. The sum map sumZeroHom φ from the direct sum ⊕_i β_i to γ, evaluated at the element that has a single nonzero component x in β_i, equals φ_i(x).
Русский
Пусть φ состоит из нулевых одомоморфизмов φ_i: β_i → γ. Тогда отображение sumZeroHom φ из прямой суммы ⊕_i β_i в γ, применённое к элементу с единственным ненулевым компонентом x в β_i, равно φ_i(x).
LaTeX
$$$ \\bigl(\\operatorname{sumZeroHom} \\ φ\\bigr)\\bigl(\\mathrm{single}(i,x)\\bigr) = φ_i(x). $$$
Lean4
@[simp]
theorem sumZeroHom_single [∀ i, Zero (β i)] [AddCommMonoid γ] (φ : ∀ i, ZeroHom (β i) γ) (i) (x : β i) :
sumZeroHom φ (single i x) = φ i x :=
by
dsimp [sumZeroHom, single, Trunc.lift_mk]
rw [Multiset.toFinset_singleton, Finset.sum_singleton, Pi.single_eq_same]
