Commit 2021-05-15 08:16 5da114c4View on Github →
feat(algebraic_topology): the Moore complex of a simplicial object (#6308)
We construct the normalized Moore complex, as a functor
simplicial_object C ⥤ chain_complex C ℕ,
for any abelian category
n-th object is intersection of
the kernels of
X.δ i : X.obj n ⟶ X.obj (n-1), for
i = 1, ..., n.
The differentials are induced from
which maps each of these intersections of kernels to the next.
This functor is one direction of the Dold-Kan equivalence, which we're still working towards.
added theorem chain_complex.of_d_ne
added def chain_complex.of_hom
added theorem algebraic_topology.normalized_Moore_complex.d_squared