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.obj Δ ⟶ s.N (Opposite.unop A.fst).len

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

Equations

• s.πSummand A = s.desc Δ fun (B : SimplicialObject.Splitting.IndexSet Δ) => if h : B = A then CategoryTheory.eqToHom ⋯ else 0

@[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 ((s.cofan Δ).inj A) (s.πSummand A) = CategoryTheory.CategoryStruct.id (SimplicialObject.Splitting.summand s.N Δ A)

@[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 (Opposite.unop A.fst).len ⟶ Z) : CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (s.πSummand A) h) = 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 B : SimplicialObject.Splitting.IndexSet Δ) (h : B ≠ A) : CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (s.πSummand B) = 0

@[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 B : SimplicialObject.Splitting.IndexSet Δ) (h : B ≠ A) {Z : C} (h✝ : s.N (Opposite.unop B.fst).len ⟶ Z) : CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (s.πSummand B) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

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.obj Δ) = ∑ A : SimplicialObject.Splitting.IndexSet Δ, CategoryTheory.CategoryStruct.comp (s.πSummand A) ((s.cofan Δ).inj A)

@[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 (X.σ i) (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk (n + 1))))) = 0

@[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 (Opposite.unop (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk (n + 1)))).fst).len ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk (n + 1))))) h) = CategoryTheory.CategoryStruct.comp 0 h

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 : ¬A.EqId) : CategoryTheory.CategoryStruct.comp ((s.cofan (Opposite.op (SimplexCategory.mk n))).inj 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.obj (Opposite.op (SimplexCategory.mk n))) : CategoryTheory.CategoryStruct.comp f (AlgebraicTopology.DoldKan.PInfty.f n) = 0 ↔ CategoryTheory.CategoryStruct.comp f (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) = 0

@[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) (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) = s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))

@[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 (Opposite.unop (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))).fst).len ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (CategoryTheory.CategoryStruct.comp (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) h) = CategoryTheory.CategoryStruct.comp (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk 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 (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (CategoryTheory.CategoryStruct.comp ((s.cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (AlgebraicTopology.DoldKan.PInfty.f n)) = AlgebraicTopology.DoldKan.PInfty.f 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 (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (CategoryTheory.CategoryStruct.comp ((s.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.PInfty.f n) h

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 : ¬A.EqId) : CategoryTheory.CategoryStruct.comp ((s.cofan (Opposite.op (SimplexCategory.mk j))).inj A) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).d j k) (s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk k))))) = 0

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

• s.nondegComplex = { X := s.N, d := s.d, shape := ⋯, d_comp_d' := ⋯ }

@[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✝ : ℕ) : s.nondegComplex.X a✝ = s.N a✝

@[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 : ℕ) : s.nondegComplex.d i j = s.d i j

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 ℕ)).obj s.nondegComplex ≅ AlgebraicTopology.DoldKan.N₁.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.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 : ℕ) : s.toKaroubiNondegComplexIsoN₁.inv.f.f n = s.πSummand (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 : ℕ) : s.toKaroubiNondegComplexIsoN₁.hom.f.f n = CategoryTheory.CategoryStruct.comp ((s.cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (AlgebraicTopology.DoldKan.PInfty.f n)

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.nondegComplexFunctor_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ S₂ : SimplicialObject.Split C} (Φ : S₁ ⟶ S₂) (n : ℕ) : (SimplicialObject.Split.nondegComplexFunctor.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.obj S = S.s.nondegComplex

noncomputable def SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : SimplicialObject.Split.nondegComplexFunctor.comp (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)) ≅ (SimplicialObject.Split.forget C).comp 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

• SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁ = CategoryTheory.NatIso.ofComponents (fun (S : SimplicialObject.Split C) => S.s.toKaroubiNondegComplexIsoN₁) ⋯

@[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 = X.s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))

@[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 ((X.s.cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (AlgebraicTopology.DoldKan.PInfty.f n)