Lean4
/-- When summing over an `ZeroHom`, the decidability assumption is not needed, and the result is
also an `ZeroHom`.
-/
def sumZeroHom [∀ i, Zero (β i)] [AddCommMonoid γ] (φ : ∀ i, ZeroHom (β i) γ) : ZeroHom (Π₀ i, β i) γ
where
toFun
f :=
(f.support'.lift fun s => ∑ i ∈ Multiset.toFinset s.1, φ i (f i)) <|
by
rintro ⟨sx, hx⟩ ⟨sy, hy⟩
dsimp only [Subtype.coe_mk, toFun_eq_coe] at *
have H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset := Finset.inter_subset_left
have H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset := Finset.inter_subset_right
refine (Finset.sum_subset H1 ?_).symm.trans ((Finset.sum_congr rfl ?_).trans (Finset.sum_subset H2 ?_))
· intro i H1 H2
rw [Finset.mem_inter] at H2
simp only [Multiset.mem_toFinset] at H1 H2
convert map_zero (φ i)
exact (hy i).resolve_left (mt (And.intro H1) H2)
· intro i _
rfl
· intro i H1 H2
rw [Finset.mem_inter] at H2
simp only [Multiset.mem_toFinset] at H1 H2
convert map_zero (φ i)
exact (hx i).resolve_left (mt (fun H3 => And.intro H3 H1) H2)
map_zero' := by simp only [toFun_eq_coe, coe_zero, Pi.zero_apply, map_zero, Finset.sum_const_zero]; rfl
