Finite support in a supplied coproduct

For a particular coproduct whose summands vanish outside a finite set, the sum of its canonical projection-inclusion endomorphisms is the identity. Thus incoming maps are determined by those finitely many projections. The converse identifies the exact support premise needed by this finite identity. No ambient finite-coproduct assumption or replacement coproduct is introduced.

Main results

• CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_of_isZero_all gives the finite projection-inclusion identity for every chosen equality instance; CategoryTheory.Limits.Sigma.isZero_of_sum_π_ι_eq_id_of_not_mem_all and CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_iff_isZero_all give its universal converse and characterization; CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_of_isZero selects one without requiring a caller instance, and CategoryTheory.Limits.Sigma.isZero_of_sum_π_ι_eq_id_of_not_mem gives its converse, and CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_iff_isZero gives the selected characterization.
• CategoryTheory.Limits.Sigma.hom_ext_of_finite_support compares incoming maps on a finite set containing every nonzero summand.
• CategoryTheory.Limits.Sigma.hom_eq_zero_of_finite_support detects a zero incoming map.

Implementation notes

The universal identity, converse, and iff preserve the caller's equality instance, which determines the literal CategoryTheory.Limits.Sigma.π. Incoming-map extensionality uses that identity. The three caller-free statements choose classical equality as specializations of the universal results.

References

Mathlib's CategoryTheory.Limits.Sigma.π, CategoryTheory.Limits.Sigma.ι_π_eq_id, and CategoryTheory.Limits.Sigma.ι_π_of_ne supply the projection laws.

Tags

coproduct, finite support, projection, zero object

The universal results quantify over the equality instance so callers may instantiate them with precisely the projections appearing in their statement.

theorem CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_of_isZero_all {C : Type u} [Category.{v, u} C] [Preadditive C] {I : Type w} (f : I → C) [HasCoproduct f] [DecidableEq I] (s : Finset I) (hz : ∀ i ∉ s, IsZero (f i)) : ∑ i ∈ s, CategoryStruct.comp (π f i) (ι f i) = CategoryStruct.id (∐ f)

The identity holds for every equality decision procedure defining the literal CategoryTheory.Limits.Sigma.π; finite support is the only restriction on summands.

theorem CategoryTheory.Limits.Sigma.isZero_of_sum_π_ι_eq_id_of_not_mem_all {C : Type u} [Category.{v, u} C] [Preadditive C] {I : Type w} (f : I → C) [HasCoproduct f] [DecidableEq I] (s : Finset I) (hid : ∑ i ∈ s, CategoryStruct.comp (π f i) (ι f i) = CategoryStruct.id (∐ f)) (j : I) (hj : j ∉ s) : IsZero (f j)

Compose the claimed identity with the inclusion of an omitted summand. Every cross term vanishes by orthogonality, forcing that summand's identity morphism to vanish.

theorem CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_iff_isZero_all {C : Type u} [Category.{v, u} C] [Preadditive C] {I : Type w} (f : I → C) [HasCoproduct f] [DecidableEq I] (s : Finset I) : ∑ i ∈ s, CategoryStruct.comp (π f i) (ι f i) = CategoryStruct.id (∐ f) ↔ ∀ i ∉ s, IsZero (f i)

Combine the inclusion test for the forward identity with the omitted summand obstruction for the converse, retaining the caller's projection convention in both directions.

theorem CategoryTheory.Limits.Sigma.hom_ext_of_finite_support {C : Type u} [Category.{v, u} C] [Preadditive C] {I : Type w} (f : I → C) [HasCoproduct f] [DecidableEq I] (s : Finset I) (hz : ∀ i ∉ s, IsZero (f i)) {A : C} {x y : A ⟶ ∐ f} (h : ∀ i ∈ s, CategoryStruct.comp x (π f i) = CategoryStruct.comp y (π f i)) : x = y

Compose with the finite projection-inclusion identity for the given projection convention to compare incoming maps on their nonzero support.

theorem CategoryTheory.Limits.Sigma.hom_eq_zero_of_finite_support {C : Type u} [Category.{v, u} C] [Preadditive C] {I : Type w} (f : I → C) [HasCoproduct f] [DecidableEq I] (s : Finset I) (hz : ∀ i ∉ s, IsZero (f i)) {A : C} (x : A ⟶ ∐ f) (h : ∀ i ∈ s, CategoryStruct.comp x (π f i) = 0) : x = 0

Specialize CategoryTheory.Limits.Sigma.hom_ext_of_finite_support to comparison with the zero map. The projection convention remains the caller's.

theorem CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_of_isZero {C : Type u} [Category.{v, u} C] [Preadditive C] {I : Type w} (f : I → C) [HasCoproduct f] (s : Finset I) (hz : ∀ i ∉ s, IsZero (f i)) : ∑ i ∈ s, CategoryStruct.comp (π f i) (ι f i) = CategoryStruct.id (∐ f)

Specialize CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_of_isZero_all using classical equality so callers need not supply a decidability instance; the universal theorem supplies the coproduct-inclusion argument.

theorem CategoryTheory.Limits.Sigma.isZero_of_sum_π_ι_eq_id_of_not_mem {C : Type u} [Category.{v, u} C] [Preadditive C] {I : Type w} (f : I → C) [HasCoproduct f] (s : Finset I) (hid : ∑ i ∈ s, CategoryStruct.comp (π f i) (ι f i) = CategoryStruct.id (∐ f)) (j : I) (hj : j ∉ s) : IsZero (f j)

Specialize CategoryTheory.Limits.Sigma.isZero_of_sum_π_ι_eq_id_of_not_mem_all using classical equality. The universal converse supplies the omitted-summand argument.

theorem CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_iff_isZero {C : Type u} [Category.{v, u} C] [Preadditive C] {I : Type w} (f : I → C) [HasCoproduct f] (s : Finset I) : ∑ i ∈ s, CategoryStruct.comp (π f i) (ι f i) = CategoryStruct.id (∐ f) ↔ ∀ i ∉ s, IsZero (f i)

Specialize CategoryTheory.Limits.Sigma.sum_π_ι_eq_id_iff_isZero_all using classical equality; the universal characterization contains the omitted-summand obstruction.