Documentation

Mathlib.AlgebraicTopology.DoldKan.Normalized

Comparison with the normalized Moore complex functor #

In this file, we show that when the category A is abelian, there is an isomorphism N₁_iso_normalizedMooreComplex_comp_toKaroubi between the functor N₁ : SimplicialObject A ⥤ Karoubi (ChainComplex A ℕ) defined in FunctorN.lean and the composition of normalizedMooreComplex A with the inclusion ChainComplex A ℕ ⥤ Karoubi (ChainComplex A ℕ).

This isomorphism shall be used in Equivalence.lean in order to obtain the Dold-Kan equivalence CategoryTheory.Abelian.DoldKan.equivalence : SimplicialObject A ≌ ChainComplex A ℕ with a functor (definitionally) equal to normalizedMooreComplex A.

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

@[simp]
theorem AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) (n : ) :
(AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X).f n = (match n with | 0 => | n.succ => Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X k.succ)).factorThru (AlgebraicTopology.DoldKan.PInfty.f n)

PInfty factors through the normalized Moore complex

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    When the category A is abelian, the functor N₁ : SimplicialObject A ⥤ Karoubi (ChainComplex A ℕ) defined using PInfty identifies to the composition of the normalized Moore complex functor and the inclusion in the Karoubi envelope.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For