Documentation

Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Construction of the inverse functor of the Dold-Kan equivalence #

In this file, we construct the functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C which shall be the inverse functor of the Dold-Kan equivalence in the case of abelian categories, and more generally pseudoabelian categories.

By definition, when K is a chain_complex, Γ₀.obj K is a simplicial object which sends Δ : SimplexCategoryᵒᵖ to a certain coproduct indexed by the set Splitting.IndexSet Δ whose elements consists of epimorphisms e : Δ.unop ⟶ Δ'.unop (with Δ' : SimplexCategoryᵒᵖ); the summand attached to such an e is K.X Δ'.unop.len. By construction, Γ₀.obj K is a split simplicial object whose splitting is Γ₀.splitting K.

We also construct Γ₂ : Karoubi (ChainComplex C ℕ) ⥤ Karoubi (SimplicialObject C) which shall be an equivalence for any additive category C.

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

source
def AlgebraicTopology.DoldKan.Isδ₀ {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [CategoryTheory.Mono i] :
Prop

Isδ₀ i is a simple condition used to check whether a monomorphism i in SimplexCategory identifies to the coface map δ 0.

Equations
Instances For
    source
    theorem AlgebraicTopology.DoldKan.Isδ₀.iff {j : ℕ} {i : Fin (j + 2)} :
    AlgebraicTopology.DoldKan.Isδ₀ (SimplexCategory.δ i) ↔ i = 0
    source
    theorem AlgebraicTopology.DoldKan.Isδ₀.eq_δ₀ {n : ℕ} {i : SimplexCategory.mk n ⟶ SimplexCategory.mk (n + 1)} [CategoryTheory.Mono i] (hi : AlgebraicTopology.DoldKan.Isδ₀ i) :
    i = SimplexCategory.δ 0
    source
    def AlgebraicTopology.DoldKan.Γ₀.Obj.summand {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ) (A : SimplicialObject.Splitting.IndexSet Δ) :
    C

    In the definition of (Γ₀.obj K).obj Δ as a direct sum indexed by A : Splitting.IndexSet Δ, the summand summand K Δ A is K.X A.1.len.

    Equations
    Instances For
      source
      def AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ) [CategoryTheory.Limits.HasFiniteCoproducts C] :
      C

      The functor Γ₀ sends a chain complex K to the simplicial object which sends Δ to the direct sum of the objects summand K Δ A for all A : Splitting.IndexSet Δ

      Equations
      Instances For
        source
        def AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) {Δ' : SimplexCategory} {Δ : SimplexCategory} (i : Δ' ⟶ Δ) [CategoryTheory.Mono i] :
        K.X Δ.len ⟶ K.X Δ'.len

        A monomorphism i : Δ' ⟶ Δ induces a morphism K.X Δ.len ⟶ K.X Δ'.len which is the identity if Δ = Δ', the differential on the complex K if i = δ 0, and zero otherwise.

        Equations
        Instances For
          source
          theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) (Δ : SimplexCategory) :
          AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.CategoryStruct.id Δ) = CategoryTheory.CategoryStruct.id (K.X Δ.len)
          source
          theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [CategoryTheory.Mono i] (hi : AlgebraicTopology.DoldKan.Isδ₀ i) :
          AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i = K.d Δ.len Δ'.len
          source
          @[simp]
          theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) {n : ℕ} :
          AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ 0) = K.d (n + 1) n
          source
          theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [CategoryTheory.Mono i] (h₁ : Δ ≠ Δ') (h₂ : ¬AlgebraicTopology.DoldKan.Isδ₀ i) :
          AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i = 0
          source
          @[simp]
          theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {K : ChainComplex C ℕ} {K' : ChainComplex C ℕ} (f : K ⟶ K') {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ ⟶ Δ') [CategoryTheory.Mono i] :
          CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (f.f Δ.len) = CategoryTheory.CategoryStruct.comp (f.f Δ'.len) (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K' i)
          source
          @[simp]
          theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {K : ChainComplex C ℕ} {K' : ChainComplex C ℕ} (f : K ⟶ K') {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ ⟶ Δ') [CategoryTheory.Mono i] {Z : C} (h : K'.X Δ.len ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (CategoryTheory.CategoryStruct.comp (f.f Δ.len) h) = CategoryTheory.CategoryStruct.comp (f.f Δ'.len) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K' i) h)
          source
          @[simp]
          theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) {Δ : SimplexCategory} {Δ' : SimplexCategory} {Δ'' : SimplexCategory} (i' : Δ'' ⟶ Δ') (i : Δ' ⟶ Δ) [CategoryTheory.Mono i'] [CategoryTheory.Mono i] :
          CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i') = AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.CategoryStruct.comp i' i)
          source
          @[simp]
          theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) {Δ : SimplexCategory} {Δ' : SimplexCategory} {Δ'' : SimplexCategory} (i' : Δ'' ⟶ Δ') (i : Δ' ⟶ Δ) [CategoryTheory.Mono i'] [CategoryTheory.Mono i] {Z : C} (h : K.X Δ''.len ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i') h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.CategoryStruct.comp i' i)) h
          source
          def AlgebraicTopology.DoldKan.Γ₀.Obj.map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) {Δ' : SimplexCategoryᵒᵖ} {Δ : SimplexCategoryᵒᵖ} (θ : Δ ⟶ Δ') :
          AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ ⟶ AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ'

          The simplicial morphism on the simplicial object Γ₀.obj K induced by a morphism Δ' → Δ in SimplexCategory is defined on each summand associated to an A : Splitting.IndexSet Δ in terms of the epi-mono factorisation of θ ≫ A.e.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategoryᵒᵖ} {Δ' : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {θ : Δ ⟶ Δ'} {Δ'' : SimplexCategory} {e : Opposite.unop Δ' ⟶ Δ''} {i : Δ'' ⟶ Opposite.unop A.fst} [CategoryTheory.Epi e] [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A) (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (SimplicialObject.Splitting.IndexSet.mk e))
            source
            theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategoryᵒᵖ} {Δ' : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {θ : Δ ⟶ Δ'} {Δ'' : SimplexCategory} {e : Opposite.unop Δ' ⟶ Δ''} {i : Δ'' ⟶ Opposite.unop A.fst} [CategoryTheory.Epi e] [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e) {Z : C} (h : AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ' ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (SimplicialObject.Splitting.IndexSet.mk e)) h)
            source
            theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategoryᵒᵖ} {Δ' : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A) (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e))) (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (A.pull θ))
            source
            theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategoryᵒᵖ} {Δ' : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Z : C} (h : AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ' ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (A.pull θ)) h)
            source
            def AlgebraicTopology.DoldKan.Γ₀.obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) :
            CategoryTheory.SimplicialObject C

            The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, on objects.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem AlgebraicTopology.DoldKan.Γ₀.obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) :
              ∀ {X Y : SimplexCategoryᵒᵖ} (θ : X ⟶ Y), (AlgebraicTopology.DoldKan.Γ₀.obj K).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ
              source
              @[simp]
              theorem AlgebraicTopology.DoldKan.Γ₀.obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ) :
              (AlgebraicTopology.DoldKan.Γ₀.obj K).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ
              source
              def AlgebraicTopology.DoldKan.Γ₀.splitting {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) :
              SimplicialObject.Splitting (AlgebraicTopology.DoldKan.Γ₀.obj K)

              By construction, the simplicial Γ₀.obj K is equipped with a splitting.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategoryᵒᵖ} {Δ' : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Δ'' : SimplexCategory} {e : Opposite.unop Δ' ⟶ Δ''} {i : Δ'' ⟶ Opposite.unop A.fst} [CategoryTheory.Epi e] [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e) :
                CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A) ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (SimplicialObject.Splitting.IndexSet.mk e))
                source
                theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategoryᵒᵖ} {Δ' : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Δ'' : SimplexCategory} {e : Opposite.unop Δ' ⟶ Δ''} {i : Δ'' ⟶ Opposite.unop A.fst} [CategoryTheory.Epi e] [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e) {Z : C} (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj Δ' ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (SimplicialObject.Splitting.IndexSet.mk e)) h)
                source
                theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategoryᵒᵖ} {Δ' : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') :
                CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A) ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e))) (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (A.pull θ))
                source
                theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategoryᵒᵖ} {Δ' : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Z : C} (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj Δ' ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e))) (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (A.pull θ)) h)
                source
                theorem AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [CategoryTheory.Mono i] :
                CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ))) ((AlgebraicTopology.DoldKan.Γ₀.obj K).map i.op) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ')))
                source
                theorem AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [CategoryTheory.Mono i] {Z : C} (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj (Opposite.op Δ') ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ))) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map i.op) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ'))) h)
                source
                theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategory} {Δ' : SimplexCategory} (e : Δ' ⟶ Δ) [CategoryTheory.Epi e] :
                CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ))) ((AlgebraicTopology.DoldKan.Γ₀.obj K).map e.op) = ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj (SimplicialObject.Splitting.IndexSet.mk e)
                source
                theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ : SimplexCategory} {Δ' : SimplexCategory} (e : Δ' ⟶ Δ) [CategoryTheory.Epi e] {Z : C} (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj (Opposite.op Δ') ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ))) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map e.op) h) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj (SimplicialObject.Splitting.IndexSet.mk e)) h
                source
                def AlgebraicTopology.DoldKan.Γ₀.map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] {K : ChainComplex C ℕ} {K' : ChainComplex C ℕ} (f : K ⟶ K') :
                AlgebraicTopology.DoldKan.Γ₀.obj K ⟶ AlgebraicTopology.DoldKan.Γ₀.obj K'

                The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, on morphisms.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem AlgebraicTopology.DoldKan.Γ₀.map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] {K : ChainComplex C ℕ} {K' : ChainComplex C ℕ} (f : K ⟶ K') (Δ : SimplexCategoryᵒᵖ) :
                  (AlgebraicTopology.DoldKan.Γ₀.map f).app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting K).desc Δ fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryTheory.CategoryStruct.comp (f.f (Opposite.unop A.fst).len) (((AlgebraicTopology.DoldKan.Γ₀.splitting K').cofan Δ).inj A)
                  source
                  def AlgebraicTopology.DoldKan.Γ₀' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
                  CategoryTheory.Functor (ChainComplex C ℕ) (SimplicialObject.Split C)

                  The functor Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject.Split C that induces Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, which shall be the inverse functor of the Dold-Kan equivalence for abelian or pseudo-abelian categories.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem AlgebraicTopology.DoldKan.Γ₀'_map_F {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] {K : ChainComplex C ℕ} {K' : ChainComplex C ℕ} (f : K ⟶ K') :
                    (AlgebraicTopology.DoldKan.Γ₀'.map f).F = AlgebraicTopology.DoldKan.Γ₀.map f
                    source
                    @[simp]
                    theorem AlgebraicTopology.DoldKan.Γ₀'_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) :
                    AlgebraicTopology.DoldKan.Γ₀'.obj K = SimplicialObject.Split.mk' (AlgebraicTopology.DoldKan.Γ₀.splitting K)
                    source
                    @[simp]
                    theorem AlgebraicTopology.DoldKan.Γ₀'_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] {K : ChainComplex C ℕ} {K' : ChainComplex C ℕ} (f : K ⟶ K') (i : ℕ) :
                    (AlgebraicTopology.DoldKan.Γ₀'.map f).f i = f.f i
                    source
                    def AlgebraicTopology.DoldKan.Γ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
                    CategoryTheory.Functor (ChainComplex C ℕ) (CategoryTheory.SimplicialObject C)

                    The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, which is the inverse functor of the Dold-Kan equivalence when C is an abelian category, or more generally a pseudoabelian category.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem AlgebraicTopology.DoldKan.Γ₀_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
                      ∀ {X Y : ChainComplex C ℕ} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ), (AlgebraicTopology.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 AlgebraicTopology.DoldKan.Γ₀_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) :
                      ∀ {X_1 Y : SimplexCategoryᵒᵖ} (θ : X_1 ⟶ Y), (AlgebraicTopology.DoldKan.Γ₀.obj X).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ
                      source
                      @[simp]
                      theorem AlgebraicTopology.DoldKan.Γ₀_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ) :
                      (AlgebraicTopology.DoldKan.Γ₀.obj X).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ X Δ
                      source
                      def AlgebraicTopology.DoldKan.Γ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
                      CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)) (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))

                      The extension of Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C on the idempotent completions. It shall be an equivalence of categories for any additive category C.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem AlgebraicTopology.DoldKan.Γ₂_obj_p_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)) (Δ : SimplexCategoryᵒᵖ) :
                        (AlgebraicTopology.DoldKan.Γ₂.obj P).p.app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting P.X).desc Δ fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryTheory.CategoryStruct.comp (P.p.f (Opposite.unop A.fst).len) (((AlgebraicTopology.DoldKan.Γ₀.splitting P.X).cofan Δ).inj A)
                        source
                        @[simp]
                        theorem AlgebraicTopology.DoldKan.Γ₂_obj_X_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)) (Δ : SimplexCategoryᵒᵖ) :
                        (AlgebraicTopology.DoldKan.Γ₂.obj P).X.obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ P.X Δ
                        source
                        @[simp]
                        theorem AlgebraicTopology.DoldKan.Γ₂_obj_X_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)) :
                        ∀ {X Y : SimplexCategoryᵒᵖ} (θ : X ⟶ Y), (AlgebraicTopology.DoldKan.Γ₂.obj P).X.map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map P.X θ
                        source
                        @[simp]
                        theorem AlgebraicTopology.DoldKan.Γ₂_map_f_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
                        ∀ {X Y : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ), (AlgebraicTopology.DoldKan.Γ₂.map f).f.app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting X.X).desc Δ fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryTheory.CategoryStruct.comp (f.f.f (Opposite.unop A.fst).len) (((AlgebraicTopology.DoldKan.Γ₀.splitting Y.X).cofan Δ).inj A)
                        source
                        theorem AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (n : ℕ) :
                        AlgebraicTopology.DoldKan.HigherFacesVanish (n + 1) (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op (SimplexCategory.mk (n + 1)))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk (n + 1)))))
                        source
                        @[simp]
                        theorem AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) {n : ℕ} :
                        CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (AlgebraicTopology.DoldKan.PInfty.f n) = ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))
                        source
                        @[simp]
                        theorem AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) {n : ℕ} {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj (AlgebraicTopology.DoldKan.Γ₀.obj K)).X n ⟶ Z) :
                        CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) h