Split simplicial objects in preadditive categories

In this file we define a functor nondegComplex : SimplicialObject.Split C ⥤ ChainComplex C ℕ when C is a preadditive category with finite coproducts, and get an isomorphism toKaroubiNondegComplexFunctorIsoN₁ : nondegComplex ⋙ toKaroubi _ ≅ forget C ⋙ DoldKan.N₁.

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

noncomputable def SimplicialObject.Splitting.πSummand {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : X.toPrefunctor.obj Δ ⟶ s.N (SimplexCategory.len A.fst.unop)

The projection on a summand of the coproduct decomposition given by a splitting of a simplicial object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimplicialObject.Splitting.cofan_inj_πSummand_eq_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : s.N (SimplexCategory.len A.fst.unop) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) (CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.πSummand s A) h) = h

@[simp]

theorem SimplicialObject.Splitting.cofan_inj_πSummand_eq_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) (SimplicialObject.Splitting.πSummand s A) = CategoryTheory.CategoryStruct.id (SimplicialObject.Splitting.summand s.N Δ A)

@[simp]

theorem SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (B : SimplicialObject.Splitting.IndexSet Δ) (h : B ≠ A) {Z : C} (h : s.N (SimplexCategory.len B.fst.unop) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) (CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.πSummand s B) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (B : SimplicialObject.Splitting.IndexSet Δ) (h : B ≠ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) (SimplicialObject.Splitting.πSummand s B) = 0

theorem SimplicialObject.Splitting.decomposition_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (Δ : SimplexCategoryᵒᵖ) : CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj Δ) = Finset.sum Finset.univ fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.πSummand s A) (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A)

@[simp]

theorem SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] {n : ℕ} (i : Fin (n + 1)) {Z : C} (h : s.N (SimplexCategory.len (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk (n + 1)))).fst.unop) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk (n + 1))))) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] {n : ℕ} (i : Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk (n + 1))))) = 0

theorem SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {n : ℕ} (A : SimplicialObject.Splitting.IndexSet (Opposite.op (SimplexCategory.mk n))) (hA : ¬SimplicialObject.Splitting.IndexSet.EqId A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s (Opposite.op (SimplexCategory.mk n))) A) (AlgebraicTopology.DoldKan.PInfty.f n) = 0

If a simplicial object X in an additive category is split, then PInfty vanishes on all the summands of X _[n] which do not correspond to the identity of [n].

theorem SimplicialObject.Splitting.comp_PInfty_eq_zero_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] {Z : C} {n : ℕ} (f : Z ⟶ X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))) : CategoryTheory.CategoryStruct.comp f (AlgebraicTopology.DoldKan.PInfty.f n) = 0 ↔ CategoryTheory.CategoryStruct.comp f (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) = 0

@[simp]

theorem SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (n : ℕ) {Z : C} (h : s.N (SimplexCategory.len (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))).fst.unop) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) h) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) h

@[simp]

theorem SimplicialObject.Splitting.PInfty_comp_πSummand_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (n : ℕ) : CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) = SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))

@[simp]

theorem SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (n : ℕ) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s (Opposite.op (SimplexCategory.mk n))) (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h)) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h

@[simp]

theorem SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (n : ℕ) : CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s (Opposite.op (SimplexCategory.mk n))) (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (AlgebraicTopology.DoldKan.PInfty.f n)) = AlgebraicTopology.DoldKan.PInfty.f n

noncomputable def SimplicialObject.Splitting.d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (i : ℕ) (j : ℕ) : s.N i ⟶ s.N j

The differentials s.d i j : s.N i ⟶ s.N j on nondegenerate simplices of a split simplicial object are induced by the differentials on the alternating face map complex.

Equations

• One or more equations did not get rendered due to their size.

theorem SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (j : ℕ) (k : ℕ) (A : SimplicialObject.Splitting.IndexSet (Opposite.op (SimplexCategory.mk j))) (hA : ¬SimplicialObject.Splitting.IndexSet.EqId A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s (Opposite.op (SimplexCategory.mk j))) A) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).d j k) (SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk k))))) = 0

@[simp]

theorem SimplicialObject.Splitting.nondegComplex_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (i : ℕ) (j : ℕ) : (SimplicialObject.Splitting.nondegComplex s).d i j = SimplicialObject.Splitting.d s i j

@[simp]

theorem SimplicialObject.Splitting.nondegComplex_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] : ∀ (a : ℕ), (SimplicialObject.Splitting.nondegComplex s).X a = s.N a

noncomputable def SimplicialObject.Splitting.nondegComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] : ChainComplex C ℕ

If s is a splitting of a simplicial object X in a preadditive category, s.nondegComplex is a chain complex which is given in degree n by the nondegenerate n-simplices of X.

Equations

• SimplicialObject.Splitting.nondegComplex s = HomologicalComplex.mk s.N (SimplicialObject.Splitting.d s)

@[simp]

theorem SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (n : ℕ) : (SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ s).inv.f.f n = SimplicialObject.Splitting.πSummand s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))

@[simp]

theorem SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] (n : ℕ) : (SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ s).hom.f.f n = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s (Opposite.op (SimplexCategory.mk n))) (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (AlgebraicTopology.DoldKan.PInfty.f n)

noncomputable def SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [CategoryTheory.Preadditive C] : (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).toPrefunctor.obj (SimplicialObject.Splitting.nondegComplex s) ≅ AlgebraicTopology.DoldKan.N₁.toPrefunctor.obj X

The chain complex s.nondegComplex attached to a splitting of a simplicial object X becomes isomorphic to the normalized Moore complex N₁.obj X defined as a formal direct factor in the category Karoubi (ChainComplex C ℕ).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimplicialObject.Split.nondegComplexFunctor_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} (Φ : S₁ ⟶ S₂) (n : ℕ) : (SimplicialObject.Split.nondegComplexFunctor.toPrefunctor.map Φ).f n = Φ.f n

@[simp]

theorem SimplicialObject.Split.nondegComplexFunctor_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S : SimplicialObject.Split C) : SimplicialObject.Split.nondegComplexFunctor.toPrefunctor.obj S = SimplicialObject.Splitting.nondegComplex S.s

noncomputable def SimplicialObject.Split.nondegComplexFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (SimplicialObject.Split C) (ChainComplex C ℕ)

The functor which sends a split simplicial object in a preadditive category to the chain complex which consists of nondegenerate simplices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : SimplicialObject.Split C) (n : ℕ) : (SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.hom.app X).f.f n = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan X.s (Opposite.op (SimplexCategory.mk n))) (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (AlgebraicTopology.DoldKan.PInfty.f n)

@[simp]

theorem SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : SimplicialObject.Split C) (n : ℕ) : (SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app X).f.f n = SimplicialObject.Splitting.πSummand X.s (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))

noncomputable def SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor.comp SimplicialObject.Split.nondegComplexFunctor (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)) ≅ CategoryTheory.Functor.comp (SimplicialObject.Split.forget C) AlgebraicTopology.DoldKan.N₁

The natural isomorphism (in Karoubi (ChainComplex C ℕ)) between the chain complex of nondegenerate simplices of a split simplicial object and the normalized Moore complex defined as a formal direct factor of the alternating face map complex.

Equations

• One or more equations did not get rendered due to their size.