Commit 2022-12-10 16:28 19d6240d

View on Github →

feat(algebraic_topology/dold-kan): The Dold-Kan equivalence for additive categories (#17640) This PR defines the Dold-Kan equivalence karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ) between the idempotent completions of the categories simplicial_object C and chain_complex C ℕ when C is an additive category.

Estimated changes

Created src/algebraic_topology/dold_kan/equivalence_additive.lean

added def category_theory.preadditive.dold_kan.N

added def category_theory.preadditive.dold_kan.equivalence

added def category_theory.preadditive.dold_kan.Γ

Modified src/algebraic_topology/dold_kan/n_comp_gamma.lean

added def algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂

added theorem algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂_nat_trans

added theorem algebraic_topology.dold_kan.identity_N₂

added theorem algebraic_topology.dold_kan.identity_N₂_objectwise

added def algebraic_topology.dold_kan.Γ₂N₁

added def algebraic_topology.dold_kan.Γ₂N₂.nat_trans

added theorem algebraic_topology.dold_kan.Γ₂N₂.nat_trans_app_f_app

added def algebraic_topology.dold_kan.Γ₂N₂