The Dold-Kan correspondence for pseudoabelian categories #
In this file, for any idempotent complete additive category C,
the Dold-Kan equivalence
Idempotents.DoldKan.Equivalence C : SimplicialObject C ≌ ChainComplex C ℕ
is obtained. It is deduced from the equivalence
Preadditive.DoldKan.Equivalence between the respective idempotent
completions of these categories using the fact that when C is idempotent complete,
then both SimplicialObject C and ChainComplex C ℕ are idempotent complete.
The construction of Idempotents.DoldKan.Equivalence uses the tools
introduced in the file Compatibility.lean. Doing so, the functor
Idempotents.DoldKan.N of the equivalence is
the composition of N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)
(defined in FunctorN.lean) and the inverse of the equivalence
ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ). The functor
Idempotents.DoldKan.Γ of the equivalence is by definition the functor
Γ₀ introduced in FunctorGamma.lean.
(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.N_obj
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(X : CategoryTheory.SimplicialObject C)
:
CategoryTheory.Idempotents.DoldKan.N.toPrefunctor.obj X = (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.toPrefunctor.obj
(AlgebraicTopology.DoldKan.N₁.toPrefunctor.obj X)
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.N_map_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
∀ {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (i : ℕ),
(CategoryTheory.Idempotents.DoldKan.N.toPrefunctor.map f).f i = CategoryTheory.CategoryStruct.comp
((CategoryTheory.Functor.objObjPreimageIso (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ))
(AlgebraicTopology.DoldKan.N₁.toPrefunctor.obj X)).hom.f.f
i)
(CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f i)
(CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk i)))
((CategoryTheory.Functor.objObjPreimageIso (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ))
(AlgebraicTopology.DoldKan.N₁.toPrefunctor.obj Y)).inv.f.f
i)))
def
CategoryTheory.Idempotents.DoldKan.N
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
The functor N for the equivalence is obtained by composing
N' : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) and the inverse
of the equivalence ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ).
Equations
- CategoryTheory.Idempotents.DoldKan.N = CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse
Instances For
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.Γ_map_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
∀ {X Y : ChainComplex C ℕ} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ),
(CategoryTheory.Idempotents.DoldKan.Γ.toPrefunctor.map f).app Δ = SimplicialObject.Splitting.desc (AlgebraicTopology.DoldKan.Γ₀.splitting X) Δ
fun (A : SimplicialObject.Splitting.IndexSet Δ) =>
CategoryTheory.CategoryStruct.comp (f.f (SimplexCategory.len A.fst.unop))
(CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan (AlgebraicTopology.DoldKan.Γ₀.splitting Y) Δ)
A)
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.Γ_obj_map
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(X : ChainComplex C ℕ)
:
∀ {X_1 Y : SimplexCategoryᵒᵖ} (θ : X_1 ⟶ Y),
(CategoryTheory.Idempotents.DoldKan.Γ.toPrefunctor.obj X).toPrefunctor.map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.Γ_obj_obj
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(X : ChainComplex C ℕ)
(Δ : SimplexCategoryᵒᵖ)
:
(CategoryTheory.Idempotents.DoldKan.Γ.toPrefunctor.obj X).toPrefunctor.obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ X Δ
def
CategoryTheory.Idempotents.DoldKan.Γ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
The functor Γ for the equivalence is Γ'.
Equations
- CategoryTheory.Idempotents.DoldKan.Γ = AlgebraicTopology.DoldKan.Γ₀
Instances For
def
CategoryTheory.Idempotents.DoldKan.isoN₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Functor.comp
(CategoryTheory.Idempotents.toKaroubiEquivalence (CategoryTheory.SimplicialObject C)).functor
CategoryTheory.Preadditive.DoldKan.equivalence.functor ≅ AlgebraicTopology.DoldKan.N₁
A reformulation of the isomorphism toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁
Equations
- CategoryTheory.Idempotents.DoldKan.isoN₁ = AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁
Instances For
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(X : CategoryTheory.SimplicialObject C)
:
(CategoryTheory.Idempotents.DoldKan.isoN₁.hom.app X).f = AlgebraicTopology.DoldKan.PInfty
def
CategoryTheory.Idempotents.DoldKan.isoΓ₀
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).functor
CategoryTheory.Preadditive.DoldKan.equivalence.inverse ≅ CategoryTheory.Functor.comp CategoryTheory.Idempotents.DoldKan.Γ
(CategoryTheory.Idempotents.toKaroubiEquivalence (CategoryTheory.SimplicialObject C)).functor
A reformulation of the canonical isomorphism
toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ≅ Γ ⋙ toKaroubi (SimplicialObject C).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(X : ChainComplex C ℕ)
:
(AlgebraicTopology.DoldKan.N₂.toPrefunctor.map (CategoryTheory.Idempotents.DoldKan.isoΓ₀.hom.app X)).f = AlgebraicTopology.DoldKan.PInfty
def
CategoryTheory.Idempotents.DoldKan.equivalence
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
The Dold-Kan equivalence for pseudoabelian categories given
by the functors N and Γ. It is obtained by applying the results in
Compatibility.lean to the equivalence Preadditive.DoldKan.Equivalence.
Equations
- CategoryTheory.Idempotents.DoldKan.equivalence = AlgebraicTopology.DoldKan.Compatibility.equivalence CategoryTheory.Idempotents.DoldKan.isoN₁ CategoryTheory.Idempotents.DoldKan.isoΓ₀
Instances For
theorem
CategoryTheory.Idempotents.DoldKan.equivalence_functor
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Idempotents.DoldKan.equivalence.functor = CategoryTheory.Idempotents.DoldKan.N
theorem
CategoryTheory.Idempotents.DoldKan.equivalence_inverse
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Idempotents.DoldKan.equivalence.inverse = CategoryTheory.Idempotents.DoldKan.Γ
theorem
CategoryTheory.Idempotents.DoldKan.hη
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
AlgebraicTopology.DoldKan.Compatibility.τ₀ = AlgebraicTopology.DoldKan.Compatibility.τ₁ CategoryTheory.Idempotents.DoldKan.isoN₁
CategoryTheory.Idempotents.DoldKan.isoΓ₀ AlgebraicTopology.DoldKan.N₁Γ₀
The natural isomorphism NΓ' satisfies the compatibility that is needed for the construction of our counit isomorphism η`
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.η_inv_app_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(X : ChainComplex C ℕ)
(i : ℕ)
:
(CategoryTheory.Idempotents.DoldKan.η.inv.app X).f i = CategoryTheory.CategoryStruct.comp
(((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.hom.app X).f i)
(((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.toPrefunctor.map
(AlgebraicTopology.DoldKan.N₁Γ₀.inv.app X)).f
i)
@[simp]
theorem
CategoryTheory.Idempotents.DoldKan.η_hom_app_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(X : ChainComplex C ℕ)
(i : ℕ)
:
(CategoryTheory.Idempotents.DoldKan.η.hom.app X).f i = CategoryTheory.CategoryStruct.comp
(((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.toPrefunctor.map
(AlgebraicTopology.DoldKan.N₁Γ₀.hom.app X)).f
i)
(((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.inv.app X).f i)
def
CategoryTheory.Idempotents.DoldKan.η
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Functor.comp CategoryTheory.Idempotents.DoldKan.Γ CategoryTheory.Idempotents.DoldKan.N ≅ CategoryTheory.Functor.id (ChainComplex C ℕ)
The counit isomorphism induced by N₁Γ₀
Equations
- CategoryTheory.Idempotents.DoldKan.η = AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso AlgebraicTopology.DoldKan.N₁Γ₀
Instances For
theorem
CategoryTheory.Idempotents.DoldKan.equivalence_counitIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Idempotents.DoldKan.equivalence.counitIso = CategoryTheory.Idempotents.DoldKan.η
theorem
CategoryTheory.Idempotents.DoldKan.hε
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
AlgebraicTopology.DoldKan.Compatibility.υ CategoryTheory.Idempotents.DoldKan.isoN₁ = AlgebraicTopology.DoldKan.Γ₂N₁
def
CategoryTheory.Idempotents.DoldKan.ε
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C) ≅ CategoryTheory.Functor.comp CategoryTheory.Idempotents.DoldKan.N CategoryTheory.Idempotents.DoldKan.Γ
The unit isomorphism induced by Γ₂N₁.
Equations
- CategoryTheory.Idempotents.DoldKan.ε = AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso CategoryTheory.Idempotents.DoldKan.isoΓ₀ AlgebraicTopology.DoldKan.Γ₂N₁
Instances For
theorem
CategoryTheory.Idempotents.DoldKan.equivalence_unitIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Idempotents.DoldKan.equivalence.unitIso = CategoryTheory.Idempotents.DoldKan.ε