Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-01 09:25 369b22a4

View on Github →

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

Estimated changes

Created src/algebraic_topology/dold_kan/functor_gamma.lean

added theorem algebraic_topology.dold_kan.is_δ₀.eq_δ₀

added theorem algebraic_topology.dold_kan.is_δ₀.iff

added def algebraic_topology.dold_kan.is_δ₀

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

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

added def algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono

added theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_comp

added theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_eq_zero

added theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_id

added theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_naturality

added theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_δ₀'

added theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_δ₀

Modified src/algebraic_topology/simplex_category.lean

added theorem simplex_category.len_lt_of_mono