Commit 2022-12-07 20:30 5f68029a

View on Github →

feat(algebraic_topology/dold_kan): the counit isomorphism of the Dold-Kan equivalence (#17633) This PR constructs the counit isomorphism N₂Γ₂ : Γ₂ ⋙ N₂ ≅ 𝟭 (karoubi (chain_complex C ℕ)) of the Dold-Kan equivalence.

Estimated changes

Modified src/algebraic_topology/dold_kan/gamma_comp_n.lean

added def algebraic_topology.dold_kan.N₂Γ₂

added theorem algebraic_topology.dold_kan.N₂Γ₂_compatible_with_N₁Γ₀

added theorem algebraic_topology.dold_kan.N₂Γ₂_inv_app_f_f

Modified src/category_theory/idempotents/functor_extension.lean

added theorem category_theory.idempotents.whiskering_left_obj_preimage_app