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.instReflectsIsomorphismsSimplicialObjectInstCategorySimplicialObjectKaroubiChainComplexPreadditiveHasZeroMorphismsNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidInstStrictOrderedSemiringToOneInstCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownInstCategoryKaroubiN₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
CategoryTheory.Functor.ReflectsIsomorphisms AlgebraicTopology.DoldKan.N₁
Equations
  • ⋯ = ⋯
source
theorem AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ (CategoryTheory.Idempotents.karoubiChainComplexEquivalence C ℕ).functor = CategoryTheory.Functor.comp (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ (CategoryTheory.Functor.comp (CategoryTheory.Idempotents.karoubiChainComplexEquivalence (CategoryTheory.Idempotents.Karoubi C) ℕ).functor (CategoryTheory.Functor.mapHomologicalComplex (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ))))
source
instance AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectInstCategorySimplicialObjectInstCategoryKaroubiChainComplexPreadditiveHasZeroMorphismsNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidInstStrictOrderedSemiringToOneInstCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownN₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
CategoryTheory.Functor.ReflectsIsomorphisms AlgebraicTopology.DoldKan.N₂

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.

Equations
  • ⋯ = ⋯