Applying a finite sum of morphisms of abelian groups

AddCommGrpCat is preadditive, so a finite family of morphisms A ⟶ B can be summed. Mathlib supplies AddCommGrpCat.hom_add_apply for a binary sum but nothing for a Finset sum, checked against the pinned revision. A complex whose differential is an alternating sum of face maps cannot be evaluated at an element without it.

Main declarations

• AddCommGrpCat.hom_sum_apply — a finite sum of morphisms, applied;
• AddCommGrpCat.hom_sum_zsmul_apply — the alternating-sum form, where each summand carries an integer coefficient.

Implementation notes

The zsmul step of hom_sum_zsmul_apply is rfl: the ℤ-action on morphisms of abelian groups is pointwise by construction. Only the Finset sum needs an induction.

This is owned library code held against a gap in Mathlib rather than a placeholder; if Mathlib later declares these names, redeclaring them here is a hard error rather than a shadowing warning, and the fix is deleting this file.

Tags

abelian group, preadditive, finite sum

theorem AddCommGrpCat.hom_sum_apply {A B : AddCommGrpCat} {J : Type u_1} (s : Finset J) (f : J → (A ⟶ B)) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (∑ i ∈ s, f i)) a = ∑ i ∈ s, (CategoryTheory.ConcreteCategory.hom (f i)) a

A finite sum of morphisms of abelian groups is applied summand by summand.

theorem AddCommGrpCat.hom_sum_zsmul_apply {A B : AddCommGrpCat} {J : Type u_1} (s : Finset J) (c : J → ℤ) (f : J → (A ⟶ B)) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (∑ i ∈ s, c i • f i)) a = ∑ i ∈ s, c i • (CategoryTheory.ConcreteCategory.hom (f i)) a

An integer-weighted finite sum of morphisms, applied. This is the shape an alternating sum of face maps takes when evaluated at a cochain.