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 CategoryTheory.SimplicialObject.Splitting.πSummand {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : 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 : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) => if h : B = A then CategoryTheory.eqToHom ⋯ else 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.SimplicialObject.Splitting.decomposition_id {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] (Δ : SimplexCategoryᵒᵖ) : CategoryStruct.id (X.obj Δ) = ∑ A : IndexSet Δ, CategoryStruct.comp (s.πSummand A) ((s.cofan Δ).inj A)

@[simp]

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

@[simp]

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

theorem CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X : SimplicialObject C} (s : X.Splitting) {n : ℕ} (A : IndexSet (Opposite.op { len := n })) (hA : ¬A.EqId) : CategoryStruct.comp ((s.cofan (Opposite.op { len := 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 CategoryTheory.SimplicialObject.Splitting.comp_PInfty_eq_zero_iff {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] {Z : C} {n : ℕ} (f : Z ⟶ X.obj (Opposite.op { len := n })) : CategoryStruct.comp f (AlgebraicTopology.DoldKan.PInfty.f n) = 0 ↔ CategoryStruct.comp f (s.πSummand (IndexSet.id (Opposite.op { len := n }))) = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.SimplicialObject.Splitting.d {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [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 CategoryTheory.SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] (j k : ℕ) (A : IndexSet (Opposite.op { len := j })) (hA : ¬A.EqId) : CategoryStruct.comp ((s.cofan (Opposite.op { len := j })).inj A) (CategoryStruct.comp ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).d j k) (s.πSummand (IndexSet.id (Opposite.op { len := k })))) = 0

noncomputable def CategoryTheory.SimplicialObject.Splitting.nondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [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. This chain complex should be thought as the normalized chain complex of X because of the isomorphism toKaroubiNondegComplexIsoN₁.

Equations

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : (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 CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] (n : ℕ) : s.toKaroubiNondegComplexIsoN₁.inv.f.f n = s.πSummand (IndexSet.id (Opposite.op { len := n }))

@[simp]

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

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_PInfty {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f AlgebraicTopology.DoldKan.PInfty = s.toKaroubiNondegComplexIsoN₁.hom.f

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_PInfty_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) : CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f (CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) = CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f h

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_inv_id_f {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f s.toKaroubiNondegComplexIsoN₁.inv.f = CategoryStruct.id s.nondegComplex

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_inv_id_f_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] {Z : ChainComplex C ℕ} (h : s.nondegComplex ⟶ Z) : CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f (CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.inv.f h) = h

noncomputable def CategoryTheory.SimplicialObject.Splitting.toNondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ s.nondegComplex

Given a splitting s of a simplicial object X in a preadditive category, this is the split epimorphism from the alternating face map complex of X to the chain complex s.nondegComplex.

Equations

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

noncomputable def CategoryTheory.SimplicialObject.Splitting.fromNondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : s.nondegComplex ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X

Given a splitting s of a simplicial object X in a preadditive category, this is the split monomormphism from the chain complex s.nondegComplex to the alternating face map complex fo X.

Equations

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

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.PInfty_toNondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty s.toNondegComplex = s.toNondegComplex

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.PInfty_toNondegComplex_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] {Z : ChainComplex C ℕ} (h : s.nondegComplex ⟶ Z) : CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (CategoryStruct.comp s.toNondegComplex h) = CategoryStruct.comp s.toNondegComplex h

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_toNondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : CategoryStruct.comp s.fromNondegComplex s.toNondegComplex = CategoryStruct.id s.nondegComplex

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_toNondegComplex_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] {Z : ChainComplex C ℕ} (h : s.nondegComplex ⟶ Z) : CategoryStruct.comp s.fromNondegComplex (CategoryStruct.comp s.toNondegComplex h) = h

theorem CategoryTheory.SimplicialObject.Splitting.toNondegComplex_f {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] (n : ℕ) : s.toNondegComplex.f n = CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (s.toKaroubiNondegComplexIsoN₁.inv.f.f n)

theorem CategoryTheory.SimplicialObject.Splitting.toNondegComplex_f_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] (n : ℕ) {Z : C} (h : s.nondegComplex.X n ⟶ Z) : CategoryStruct.comp (s.toNondegComplex.f n) h = CategoryStruct.comp (CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (s.toKaroubiNondegComplexIsoN₁.inv.f.f n)) h

theorem CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_f {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] (n : ℕ) : s.fromNondegComplex.f n = CategoryStruct.comp (s.ι n) (AlgebraicTopology.DoldKan.PInfty.f n)

theorem CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_f_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] (n : ℕ) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z) : CategoryStruct.comp (s.fromNondegComplex.f n) h = CategoryStruct.comp (CategoryStruct.comp (s.ι n) (AlgebraicTopology.DoldKan.PInfty.f n)) h

instance CategoryTheory.SimplicialObject.Splitting.isSplitEpi_toNondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : IsSplitEpi s.toNondegComplex

instance CategoryTheory.SimplicialObject.Splitting.isSplitMono_fromNondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : IsSplitMono s.fromNondegComplex

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.toNondegComplex_fromNondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : CategoryStruct.comp s.toNondegComplex s.fromNondegComplex = AlgebraicTopology.DoldKan.PInfty

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.toNondegComplex_fromNondegComplex_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) : CategoryStruct.comp s.toNondegComplex (CategoryStruct.comp s.fromNondegComplex h) = CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h

noncomputable def CategoryTheory.SimplicialObject.Splitting.homotopyEquivNondegComplex {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : HomotopyEquiv (AlgebraicTopology.AlternatingFaceMapComplex.obj X) s.nondegComplex

Given a splitting s of a simplicial object X in a preadditive category, this is the homotopy equivalence from the alternating face map complex of X to the chain complex s.nondegComplex.

Equations

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

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.homotopyEquivNondegComplex_hom {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : s.homotopyEquivNondegComplex.hom = s.toNondegComplex

@[simp]

theorem CategoryTheory.SimplicialObject.Splitting.homotopyEquivNondegComplex_inv {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) [Preadditive C] : s.homotopyEquivNondegComplex.inv = s.fromNondegComplex

noncomputable def CategoryTheory.SimplicialObject.Split.nondegComplexFunctor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] : Functor (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 CategoryTheory.SimplicialObject.Split.nondegComplexFunctor_map_f {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {S₁ S₂ : Split C} (Φ : S₁ ⟶ S₂) (n : ℕ) : (nondegComplexFunctor.map Φ).f n = Φ.f n

@[simp]

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

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

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

@[simp]

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

@[simp]

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