mathlib documentation


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.

@[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.