Simplicial chains with varying coefficients

This file records how the coproduct inclusion associated to a simplex behaves under a morphism of coefficient objects, and how the degreewise components of the chain maps induced by maps of simplicial sets compose with each other and with changes of coefficients.

@[simp]

theorem TauCeti.SSet.ιChainComplex_chainComplexFunctor_map_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X : SSet} {R R' : C} (f : R ⟶ R') {n : ℕ} (x : X.obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) ((((SSet.chainComplexFunctor C).map f).app X).f n) = CategoryTheory.CategoryStruct.comp f (X.ιChainComplex x)

Mapping the coefficient object of simplicial chains applies the coefficient morphism before the coproduct inclusion associated to each simplex.

@[simp]

theorem TauCeti.SSet.ιChainComplex_chainComplexFunctor_map_app_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X : SSet} {R R' : C} (f : R ⟶ R') {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : C} (h : (((SSet.chainComplexFunctor C).obj R').obj X).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (CategoryTheory.CategoryStruct.comp ((((SSet.chainComplexFunctor C).map f).app X).f n) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) h)

Mapping the coefficient object of simplicial chains applies the coefficient morphism before the coproduct inclusion associated to each simplex.

theorem TauCeti.SSet.chainComplexMap_f_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (R : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap f R).f n) ((SSet.chainComplexMap g R).f n) = (SSet.chainComplexMap (CategoryTheory.CategoryStruct.comp f g) R).f n

The degreewise components of the chain maps induced by maps of simplicial sets compose like the maps themselves.

theorem TauCeti.SSet.chainComplexMap_f_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (R : C) (n : ℕ) {Z✝ : C} (h : (Z.chainComplex R).X n ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap f R).f n) (CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap g R).f n) h) = CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (CategoryTheory.CategoryStruct.comp f g) R).f n) h

The degreewise components of the chain maps induced by maps of simplicial sets compose like the maps themselves.

theorem TauCeti.SSet.chainComplexMap_f_chainComplexFunctor_map_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {R R' : C} {X Y : SSet} (f : X ⟶ Y) (u : R ⟶ R') (n : ℕ) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap f R).f n) ((((SSet.chainComplexFunctor C).map u).app Y).f n) = CategoryTheory.CategoryStruct.comp ((((SSet.chainComplexFunctor C).map u).app X).f n) ((SSet.chainComplexMap f R').f n)

The chain maps induced by maps of simplicial sets commute, degreewise, with changes of coefficients.

theorem TauCeti.SSet.chainComplexMap_f_chainComplexFunctor_map_app_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {R R' : C} {X Y : SSet} (f : X ⟶ Y) (u : R ⟶ R') (n : ℕ) {Z : C} (h : (((SSet.chainComplexFunctor C).obj R').obj Y).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap f R).f n) (CategoryTheory.CategoryStruct.comp ((((SSet.chainComplexFunctor C).map u).app Y).f n) h) = CategoryTheory.CategoryStruct.comp ((((SSet.chainComplexFunctor C).map u).app X).f n) (CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap f R').f n) h)

The chain maps induced by maps of simplicial sets commute, degreewise, with changes of coefficients.