English
For a fixed index i and a zero homomorphism φ: β_i → γ, the sumZeroHom over the Pi-single at i, φ, equals φ composed with the projection to the i-th coordinate.
Русский
Для фиксированного индекса i и нулевого одоморфизма φ: β_i → γ, сумма sumZeroHom на Pi.single i φ равна композиции φ с проекцией на i-ю координату.
LaTeX
$$$ \\operatorname{sumZeroHom}(\\Pi\\text{.single } i \\, φ) = φ \\circ {\\text{toFun}} := { toFun := (· i), map_zero' := rfl }. $$$
Lean4
@[simp]
theorem sumZeroHom_piSingle [∀ i, Zero (β i)] [AddCommMonoid γ] (i) (φ : ZeroHom (β i) γ) :
sumZeroHom (Pi.single i φ) = φ.comp { toFun := (· i), map_zero' := rfl } :=
by
ext ⟨f, sf, hf⟩
change (∑ i ∈ _, _) = _
dsimp
rw [Finset.sum_eq_single i (fun j _ hji => ?_) (fun hi => ?_), Pi.single_eq_same]
· simp [hji]
· simp [(hf i).resolve_left (by simpa using hi)]
