mathlib documentation

algebraic_topology.dold_kan.n_reflects_iso

N₁ and N₂ reflects isomorphisms #

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.

@[protected, instance]

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.