Split maps between coproducts, and cokernels of maps between coproducts #
Reindexing a coproduct along an injection is split #
Let X : I → C be a family of objects of a category with zero morphisms and coproducts, and let
f : J → I be injective. Reindexing along f gives a map ∐ (X ∘ f) ⟶ ∐ X, and this file
shows that it is a split monomorphism: the retraction sends the summand indexed by f j back to
the one indexed by j, and kills the summands indexed outside the range of f.
Mathlib's CategoryTheory.Limits.MonoCoprod.mono_map'_of_injective proves the same map is a
monomorphism in a category satisfying MonoCoprod; the splitting below needs zero morphisms
instead, and is the stronger statement in the situations where both apply.
Chain complexes built as coproducts over a set of simplices, singular or simplicial, get their
degreewise splittings this way: for a pair of spaces the singular simplices of the subspace form a
subset of those of the ambient space, so the short exact sequence of chains of the pair is split in
each degree, and therefore stays exact after applying a contravariant Hom(-, M).
The kernel of the codiagonal #
Let R be an object of a preadditive category with a zero object, and let ι be a type with a
distinguished element i₀. The codiagonal Sigma.desc (fun _ ↦ 𝟙 R) : ∐ (fun _ : ι ↦ R) ⟶ R,
the identity on every summand, is a split epimorphism with section the inclusion of the summand
i₀, and its kernel is the coproduct of the summands indexed by i ≠ i₀, embedded through the
differences ι_i - ι_{i₀} of coproduct inclusions (TauCeti.sigmaιSubι). The short complex
∐_{i ≠ i₀} R ⟶ ∐_ι R ⟶ R is split (TauCeti.sigmaDescIdSplitting), which identifies the kernel
of the codiagonal with ∐_{i ≠ i₀} R (TauCeti.kernelSigmaDescIdIso).
Reduced homology in degree zero is the kernel of an augmentation of this form, so this identifies it with a coproduct indexed by the path components other than that of a chosen basepoint.
Cokernels commute with coproducts #
In a category with zero morphisms, let f i : X i ⟶ Y i be a family of morphisms with cokernels
c i, and let g : ∐ X ⟶ ∐ Y be the morphism between coproducts induced by the f i. A cokernel
of g is then a coproduct of the cokernels c i, with legs induced by the coproduct inclusions
(TauCeti.isColimitCofanMkCokernelCofork). The relative chains of a pair are the cokernel of the
map from the chains of the subspace to those of the ambient space, so this is how additivity
passes from absolute to relative chains.
Reindexing a coproduct along an injective map of index types is a split monomorphism.
The morphism ∐_{i ≠ i₀} R ⟶ ∐_ι R whose component at i is the difference ι_i - ι_{i₀}
of coproduct inclusions. It is a kernel of the codiagonal ∐_ι R ⟶ R
(TauCeti.isKernelSigmaιSubι).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The differences of coproduct inclusions are killed by the codiagonal.
The differences of coproduct inclusions are killed by the codiagonal.
The retraction of TauCeti.sigmaιSubι: the identity on the summands indexed by i ≠ i₀ and
zero on the summand indexed by i₀.
Equations
- TauCeti.sigmaιSubιRetraction R i₀ = CategoryTheory.Limits.Sigma.desc fun (i : ι) => if h : i = i₀ then 0 else CategoryTheory.Limits.Sigma.ι (fun (x : { i : ι // i ≠ i₀ }) => R) ⟨i, h⟩
Instances For
The short complex ∐_{i ≠ i₀} R ⟶ ∐_ι R ⟶ R formed by the differences of coproduct
inclusions and the codiagonal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The short complex ∐_{i ≠ i₀} R ⟶ ∐_ι R ⟶ R is split: the inclusion of the summand i₀
sections the codiagonal, and TauCeti.sigmaιSubιRetraction retracts the differences.
Equations
- TauCeti.sigmaDescIdSplitting R i₀ = { r := TauCeti.sigmaιSubιRetraction R i₀, s := CategoryTheory.Limits.Sigma.ι (fun (x : ι) => R) i₀, f_r := ⋯, s_g := ⋯, id := ⋯ }
Instances For
The differences of coproduct inclusions form a kernel of the codiagonal.
Equations
Instances For
The kernel of the codiagonal ∐_ι R ⟶ R is the coproduct of the copies of R indexed by
i ≠ i₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cokernels commute with coproducts. Let f i : X i ⟶ Y i be a family of morphisms with
cokernels c i, and let g : ∐ X ⟶ ∐ Y be the morphism between coproducts induced by the f i.
Then a cokernel c' of g is the coproduct of the cokernels c i, with legs the maps
φ i : (c i).pt ⟶ c'.pt induced by the coproduct inclusions Y i ⟶ ∐ Y.
Equations
- One or more equations did not get rendered due to their size.