Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-07 10:57 5b828414

View on Github →

feat(algebraic_topology/dold_kan): starting the definition of the counit isomorphism of the Dold-Kan equivalence (#17619) This PR constructs a natural isomorphism N₁Γ₀ : Γ₀ ⋙ N₁ ≅ to_karoubi (chain_complex C ℕ).

Estimated changes

Modified src/algebraic_topology/dold_kan/functor_gamma.lean

added theorem algebraic_topology.dold_kan.P_infty_on_Γ₀_splitting_summand_eq_self

added theorem algebraic_topology.dold_kan.higher_faces_vanish.on_Γ₀_summand_id

added def algebraic_topology.dold_kan.Γ₂

Created src/algebraic_topology/dold_kan/gamma_comp_n.lean

added def algebraic_topology.dold_kan.N₁Γ₀

added theorem algebraic_topology.dold_kan.N₁Γ₀_app

added theorem algebraic_topology.dold_kan.N₁Γ₀_hom_app

added theorem algebraic_topology.dold_kan.N₁Γ₀_hom_app_f_f

added theorem algebraic_topology.dold_kan.N₁Γ₀_inv_app

added theorem algebraic_topology.dold_kan.N₁Γ₀_inv_app_f_f

added theorem algebraic_topology.dold_kan.N₂Γ₂_to_karoubi

added def algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso

added def algebraic_topology.dold_kan.Γ₀'_comp_nondeg_complex_functor

added def algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso