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

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Idempotents.DoldKan.N_map {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), CategoryTheory.Idempotents.DoldKan.N.map f = (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁.map f)
    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
    noncomputable 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 Γ'.

    Equations
    • CategoryTheory.Idempotents.DoldKan.Γ = AlgebraicTopology.DoldKan.Γ₀
    Instances For
      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_1 Y : SimplexCategoryᵒᵖ} (θ : X_1 ⟶ Y), (CategoryTheory.Idempotents.DoldKan.Γ.obj X).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ
      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 Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting X).desc Δ fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryTheory.CategoryStruct.comp (f.f (Opposite.unop A.fst).len) (((AlgebraicTopology.DoldKan.Γ₀.splitting Y).cofan Δ).inj A)
      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
      noncomputable 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.Idempotents.toKaroubiEquivalence (CategoryTheory.SimplicialObject C)).functor.comp 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
        source
        @[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
        source
        noncomputable 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.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).functor.comp CategoryTheory.Preadditive.DoldKan.equivalence.inverse ≅ CategoryTheory.Idempotents.DoldKan.Γ.comp (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
          source
          @[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₂.map (CategoryTheory.Idempotents.DoldKan.isoΓ₀.hom.app X)).f = AlgebraicTopology.DoldKan.PInfty
          source
          noncomputable 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.

          Equations
          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.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 η`

            source
            noncomputable 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.Idempotents.DoldKan.Γ.comp CategoryTheory.Idempotents.DoldKan.N ≅ CategoryTheory.Functor.id (ChainComplex C ℕ)

            The counit isomorphism induced by N₁Γ₀

            Equations
            Instances For
              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 : ℕ) :
              (CategoryTheory.Idempotents.DoldKan.η.hom.app X).f i = CategoryTheory.CategoryStruct.comp (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app X)).f i) (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.inv.app X).f i)
              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 : ℕ) :
              (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.map (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app X)).f i)
              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.Idempotents.DoldKan.isoN₁ = AlgebraicTopology.DoldKan.Γ₂N₁
              source
              noncomputable 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.Idempotents.DoldKan.N.comp CategoryTheory.Idempotents.DoldKan.Γ

              The unit isomorphism induced by Γ₂N₁.

              Equations
              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.ε