mathlib3 documentation

algebraic_topology.dold_kan.n_reflects_iso

N₁ and N₂ reflects isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

source
@[protected, instance]
def algebraic_topology.dold_kan.N₁.category_theory.reflects_isomorphisms {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] :
category_theory.reflects_isomorphisms algebraic_topology.dold_kan.N₁
source
theorem algebraic_topology.dold_kan.compatibility_N₂_N₁_karoubi {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] :
algebraic_topology.dold_kan.N₂ ⋙ (category_theory.idempotents.karoubi_chain_complex_equivalence C ℕ).functor = category_theory.idempotents.karoubi_functor_category_embedding simplex_categoryᵒᵖ C ⋙ algebraic_topology.dold_kan.N₁ ⋙ (category_theory.idempotents.karoubi_chain_complex_equivalence (category_theory.idempotents.karoubi C) ℕ).functor ⋙ (category_theory.idempotents.karoubi_karoubi.equivalence C).inverse.map_homological_complex (complex_shape.down ℕ)
source
@[protected, instance]
def algebraic_topology.dold_kan.N₂.category_theory.reflects_isomorphisms {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] :
category_theory.reflects_isomorphisms algebraic_topology.dold_kan.N₂

We deduce that N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)) reflects isomorphisms from the fact that N₁ : simplicial_object (karoubi C) ⥤ karoubi (chain_complex (karoubi C) ℕ) does.