Theorems · Definition · category theory
CategoryTheory.Preadditive.DoldKan.equivalence
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Preadditive C] →
[CategoryTheory.Limits.HasFiniteCoproducts C] →
CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C) ≌
CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)The Dold-Kan equivalence Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ)
for additive categories.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Oppositestatement · cited by 8,081
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- SimplexCategorystatement · cited by 2,204
- ComplexShape.downstatement · cited by 605
- CategoryTheory.Equivalencestatement · cited by 601
- CategoryTheory.SimplicialObjectstatement and proof · cited by 548
- ChainComplexstatement · cited by 350
- CategoryTheory.Idempotents.Karoubistatement and proof · cited by 233
- CategoryTheory.Limits.HasFiniteCoproductsstatement and proof · cited by 110
- AlgebraicTopology.DoldKan.N₂Γ₂proof · cited by 6
- AlgebraicTopology.DoldKan.Γ₂N₂proof · cited by 3
Cited by10
Results whose statement or proof uses this declaration.
- CategoryTheory.Idempotents.DoldKan.isoN₁statement · cited by 3
- CategoryTheory.Idempotents.DoldKan.isoΓ₀statement · cited by 2
- CategoryTheory.Idempotents.DoldKan.hεstatement and proof · cited by 1
- CategoryTheory.Idempotents.DoldKan.hηstatement · cited by 1
- CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_fstatement · cited by 1
- CategoryTheory.Preadditive.DoldKan.equivalence_unitIsostatement and proof · cited by 1
- CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_fstatement · cited by 0
- CategoryTheory.Preadditive.DoldKan.equivalence_counitIsostatement and proof · cited by 0
- CategoryTheory.Preadditive.DoldKan.equivalence_functorstatement and proof · cited by 0
- CategoryTheory.Preadditive.DoldKan.equivalence_inversestatement and proof · cited by 0