Documentation

Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

N₁ and N₂ reflects isomorphisms #

In this file, it is shown that the functors N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) and N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)) reflect isomorphisms for any preadditive category C.

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

source
instance AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
AlgebraicTopology.DoldKan.N₁.ReflectsIsomorphisms
source
theorem AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
AlgebraicTopology.DoldKan.N₂.comp (CategoryTheory.Idempotents.karoubiChainComplexEquivalence C ℕ).functor = (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).comp (AlgebraicTopology.DoldKan.N₁.comp ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence (CategoryTheory.Idempotents.Karoubi C) ℕ).functor.comp ((CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ))))
source
instance AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
AlgebraicTopology.DoldKan.N₂.ReflectsIsomorphisms

We deduce that N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)) reflects isomorphisms from the fact that N₁ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) does.