Documentation

Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

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.)

source
@[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.obj X = (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.obj (AlgebraicTopology.DoldKan.N₁.obj X)
source
@[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 : ℕ), HomologicalComplex.Hom.f (CategoryTheory.Idempotents.DoldKan.N.map f) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f (CategoryTheory.Functor.objObjPreimageIso (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)) (AlgebraicTopology.DoldKan.N₁.obj X)).hom.f i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty i) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk i))) (HomologicalComplex.Hom.f (CategoryTheory.Functor.objObjPreimageIso (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)) (AlgebraicTopology.DoldKan.N₁.obj Y)).inv.f i)))
source
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] :
CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (ChainComplex 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 ℕ).

Instances For
    source
    @[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.Γ.map f).app Δ = SimplicialObject.Splitting.desc (AlgebraicTopology.DoldKan.Γ₀.splitting X) Δ fun A => CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f (SimplexCategory.len A.fst.unop)) (SimplicialObject.Splitting.ιSummand (AlgebraicTopology.DoldKan.Γ₀.splitting Y) A)
    source
    @[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 Y : SimplexCategoryᵒᵖ} (θ : X ⟶ Y), (CategoryTheory.Idempotents.DoldKan.Γ.obj X).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ
    source
    @[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.Γ.obj X).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ X Δ
    source
    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 (ChainComplex C ℕ) (CategoryTheory.SimplicialObject C)

    The functor Γ for the equivalence is Γ'.

    Instances For
      source
      theorem CategoryTheory.Idempotents.DoldKan.hN₁ {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₁
      source
      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] :
      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
      source
      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] :
      CategoryTheory.SimplicialObject C ≌ ChainComplex 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.

      Instances For
        source
        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
        source
        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.Γ
        source
        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.eqToIso (_ : CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubiEquivalence (CategoryTheory.SimplicialObject C)).functor CategoryTheory.Preadditive.DoldKan.equivalence.functor = AlgebraicTopology.DoldKan.N₁)) (CategoryTheory.eqToIso (_ : 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)) AlgebraicTopology.DoldKan.N₁Γ₀

        The natural isomorphism NΓ' satisfies the compatibility that is needed for the construction of our counit isomorphism η`

        source
        @[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 : ℕ) :
        HomologicalComplex.Hom.f (CategoryTheory.Idempotents.DoldKan.η.inv.app X) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.hom.app X) i) (HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app X)) i)
        source
        @[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 : ℕ) :
        HomologicalComplex.Hom.f (CategoryTheory.Idempotents.DoldKan.η.hom.app X) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app X)) i) (HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.inv.app X) i)
        source
        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₁Γ₀

        Instances For
          source
          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.η
          source
          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.eqToIso (_ : CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubiEquivalence (CategoryTheory.SimplicialObject C)).functor CategoryTheory.Preadditive.DoldKan.equivalence.functor = AlgebraicTopology.DoldKan.N₁)) = AlgebraicTopology.DoldKan.Γ₂N₁
          source
          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₁.

          Instances For
            source
            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.ε