Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-30 10:18 63721b2c

View on Github →

feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (#17925)

Estimated changes

Created src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean

added def category_theory.idempotents.dold_kan.N

added def category_theory.idempotents.dold_kan.equivalence

added theorem category_theory.idempotents.dold_kan.equivalence_counit_iso

added theorem category_theory.idempotents.dold_kan.equivalence_functor

added theorem category_theory.idempotents.dold_kan.equivalence_inverse

added theorem category_theory.idempotents.dold_kan.equivalence_unit_iso

added theorem category_theory.idempotents.dold_kan.hN₁

added theorem category_theory.idempotents.dold_kan.hΓ₀

added theorem category_theory.idempotents.dold_kan.hε

added theorem category_theory.idempotents.dold_kan.hη

added def category_theory.idempotents.dold_kan.Γ

added def category_theory.idempotents.dold_kan.ε

added def category_theory.idempotents.dold_kan.η

Modified src/category_theory/functor/category.lean

added theorem category_theory.nat_trans.comp_app_assoc