Commit 2022-12-05 08:18 88bca0ce

View on Github →

feat(algebraic_topology/dold_kan): N₂ reflects isomorphisms (#17577) This PR shows that N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)) reflects isomorphisms.

Estimated changes

Modified src/algebra/homology/additive.lean

Modified src/algebra/homology/homological_complex.lean

added theorem homological_complex.hom.is_iso_of_components

Modified src/algebraic_topology/alternating_face_map_complex.lean

added theorem algebraic_topology.karoubi_alternating_face_map_complex_d

Modified src/algebraic_topology/dold_kan/n_reflects_iso.lean

added theorem algebraic_topology.dold_kan.compatibility_N₂_N₁_karoubi

Modified src/category_theory/idempotents/karoubi.lean

added theorem category_theory.idempotents.karoubi.zsmul_hom