Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-05 07:05 dd1f8496

View on Github →

feat(algebraic_topology/dold_kan): the inverse functor of the Dold-Kan equivalence (#17607)

Estimated changes

Modified src/algebraic_topology/dold_kan/functor_gamma.lean

added def algebraic_topology.dold_kan.Γ₀'

added def algebraic_topology.dold_kan.Γ₀.map

added def algebraic_topology.dold_kan.Γ₀.obj.map

added theorem algebraic_topology.dold_kan.Γ₀.obj.map_epi_on_summand_id

added theorem algebraic_topology.dold_kan.Γ₀.obj.map_mono_on_summand_id

added theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand'

added theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand

added theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀'

added theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀

added def algebraic_topology.dold_kan.Γ₀.obj

added def algebraic_topology.dold_kan.Γ₀.splitting

added theorem algebraic_topology.dold_kan.Γ₀.splitting_iso_hom_eq_id

added theorem algebraic_topology.dold_kan.Γ₀.splitting_map_eq_id

added def algebraic_topology.dold_kan.Γ₀

Modified src/algebraic_topology/simplex_category.lean

Modified src/algebraic_topology/split_simplicial_object.lean

added theorem simplicial_object.splitting.index_set.fac_pull

added def simplicial_object.splitting.index_set.pull