The monoidal structure of the Dold–Kan correspondence #
Let C be a preadditive monoidal category whose tensor product is additive in each variable
(CategoryTheory.MonoidalPreadditive C), with finite coproducts and idempotent complete, for
instance the category of modules over a commutative ring. Mathlib's Dold–Kan equivalence
CategoryTheory.Idempotents.DoldKan.equivalence : SimplicialObject C ≌ ChainComplex C ℕ has
functor the normalized chains N and inverse Γ. This file makes N oplax monoidal through
the Alexander–Whitney map, and hence Γ lax monoidal as its right adjoint. The lax structure
of Γ is what composes the simplicial mapping objects Γ(τ_{≥0} Hom(x, y)) of the simplicial
enrichment of a differential graded category (J. Lurie, Higher Algebra, Construction 1.3.1.13).
The normalized chains N X are the direct summand of the alternating face map complex of X
cut out by the idempotent PInfty, whose kernel is spanned by the degenerate simplices, with
inclusion CategoryTheory.Idempotents.DoldKan.inclusionN and projection
CategoryTheory.Idempotents.DoldKan.PInftyToN, bundled as the retract
CategoryTheory.Idempotents.DoldKan.retractN. For an abelian category C this summand is
isomorphic to the normalized Moore complex
(AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi). The key point is
that the Alexander–Whitney map of CategoryTheory.SimplicialObject.alexanderWhitney preserves
degenerate chains
(CategoryTheory.SimplicialObject.QInfty_comp_alexanderWhitney_comp_tensorHom_PInfty): every
summand of the Alexander–Whitney map of a degenerate simplex has a degenerate front or back face.
The comultiplication of the alternating face map complex therefore passes to the retract N
(CategoryTheory.Functor.OplaxMonoidal.ofRetract).
Main definitions and results #
CategoryTheory.SimplicialObject.PInfty_comp_alexanderWhitney_comp_tensorHom_PInfty: up to the projection onto normalized chains, the Alexander–Whitney map only depends on normalized chains.CategoryTheory.Idempotents.DoldKan.oplaxMonoidalN: the Alexander–Whitney oplax monoidal structure on the normalized chain functorN, with comultiplicationCategoryTheory.Idempotents.DoldKan.N_δand counitCategoryTheory.Idempotents.DoldKan.N_η.CategoryTheory.Idempotents.DoldKan.laxMonoidalΓ: the induced lax monoidal structure on the Dold–Kan functorΓ, with unitCategoryTheory.Idempotents.DoldKan.Γ_εand tensoratorCategoryTheory.Idempotents.DoldKan.Γ_μ.
References #
- C. Weibel, An Introduction to Homological Algebra, Section 8.5.
- S. Schwede and B. Shipley, Equivalences of monoidal model categories, Algebr. Geom. Topol. 3 (2003).
- J. Lurie, Higher Algebra, Construction 1.3.1.13.
The Alexander–Whitney map preserves degenerate chains: composed with the projection
PInfty ⊗ PInfty onto normalized chains, it vanishes on the degenerate part QInfty of the
chains of A ⊗ B.
The Alexander–Whitney map preserves degenerate chains: composed with the projection
PInfty ⊗ PInfty onto normalized chains, it vanishes on the degenerate part QInfty of the
chains of A ⊗ B.
The Alexander–Whitney map followed by the projection PInfty ⊗ PInfty onto normalized chains
only depends on the normalized part of the chains of A ⊗ B.
The Alexander–Whitney map followed by the projection PInfty ⊗ PInfty onto normalized chains
only depends on the normalized part of the chains of A ⊗ B.
The projection PInfty onto normalized chains does not change the counit of the alternating
face map complex functor, which lives in degree zero where PInfty is the identity.
The inclusion of the normalized chains N X of the pseudoabelian Dold–Kan correspondence
into the alternating face map complex of X, as the direct summand cut out by PInfty.
By definition N = N₁ ⋙ (toKaroubiEquivalence _).inverse, so N.obj X is the object of chain
complexes corresponding to the formal direct summand N₁.obj X of the Karoubi envelope, whose
underlying complex is the alternating face map complex of X with idempotent PInfty
(AlgebraicTopology.DoldKan.N₁_obj_p); the counit of toKaroubiEquivalence identifies the two.
Instances For
The projection of the alternating face map complex of X onto the normalized chains N X
of the pseudoabelian Dold–Kan correspondence.
Instances For
The normalized chains are a retract of the alternating face map complex.
The normalized chains are a retract of the alternating face map complex.
The idempotent of the alternating face map complex cutting out the normalized chains is
PInfty.
The idempotent of the alternating face map complex cutting out the normalized chains is
PInfty.
The projection onto normalized chains is unchanged by first applying PInfty.
The projection onto normalized chains is unchanged by first applying PInfty.
Normalized chains are fixed by PInfty.
Normalized chains are fixed by PInfty.
The normalized chain functor is a retract of the alternating face map complex functor, with
inclusion CategoryTheory.Idempotents.DoldKan.inclusionN and projection
CategoryTheory.Idempotents.DoldKan.PInftyToN.
Instances For
The inclusion of the normalized chains retract.
The projection of the normalized chains retract.
The Alexander–Whitney oplax monoidal structure on normalized chains: the normalized
chain functor N of the Dold–Kan correspondence is oplax monoidal, with comultiplication the
Alexander–Whitney map restricted to normalized chains and projected back onto them
(CategoryTheory.Idempotents.DoldKan.N_δ), and counit the counit of the alternating face map
complex (the identity of 𝟙_ C in degree zero) restricted to normalized chains
(CategoryTheory.Idempotents.DoldKan.N_η).
The comultiplication of the normalized chain functor: the Alexander–Whitney map of the alternating face map complexes, restricted to and projected onto normalized chains.
The counit of the normalized chain functor: the counit of the alternating face map complex,
the identity of 𝟙_ C in degree zero, restricted to normalized chains.
On normalized chains, the comultiplication of N is the Alexander–Whitney map followed by
the projection onto normalized chains.
On normalized chains, the comultiplication of N is the Alexander–Whitney map followed by
the projection onto normalized chains.
The lax monoidal structure of the Dold–Kan functor Γ from chain complexes to
simplicial objects: it is the mate, along the Dold–Kan equivalence, of the Alexander–Whitney
oplax monoidal structure of the normalized chain functor N
(CategoryTheory.Idempotents.DoldKan.Γ_ε and CategoryTheory.Idempotents.DoldKan.Γ_μ).
The unit of the lax monoidal functor Γ is the transpose of the counit of N along the
Dold–Kan equivalence.
The tensorator of the lax monoidal functor Γ is the transpose of the comultiplication of
N along the Dold–Kan equivalence.