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

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

• AlgebraicTopology.DoldKan.Isδ₀ i = (Δ.len = Δ'.len + 1 ∧ (SimplexCategory.Hom.toOrderHom i) 0 ≠ 0)

theorem AlgebraicTopology.DoldKan.Isδ₀.iff {j : ℕ} {i : Fin (j + 2)} : AlgebraicTopology.DoldKan.Isδ₀ (SimplexCategory.δ i) ↔ i = 0

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

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

• AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ A = K.X (Opposite.unop A.fst).len

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

• AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ = ∐ fun (A : SimplicialObject.Splitting.IndexSet Δ) => AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ A

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

• AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i = if h : Δ = Δ' then CategoryTheory.eqToHom ⋯ else if h : AlgebraicTopology.DoldKan.Isδ₀ i then K.d Δ.len Δ'.len else 0

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)

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

@[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

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

@[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)

@[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)

@[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

@[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)

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.

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)

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

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)

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

@[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 θ

@[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 Δ

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.

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.

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)

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

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)

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

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)

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 Δ')))

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

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)

@[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)

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.

@[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

@[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

@[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)

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.

@[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 θ

@[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 Δ

@[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)

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

• AlgebraicTopology.DoldKan.Γ₀ = AlgebraicTopology.DoldKan.Γ₀'.comp (SimplicialObject.Split.forget C)

@[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)

@[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 θ

@[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 Δ

@[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)

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

• AlgebraicTopology.DoldKan.Γ₂ = (CategoryTheory.Idempotents.functorExtension₂ (ChainComplex C ℕ) (CategoryTheory.SimplicialObject C)).obj AlgebraicTopology.DoldKan.Γ₀

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

@[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

@[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)))