Extension of scalars

If X is a simplicial set, R₁ →+* R₂ is a morphism of commutative rings, and M₁ is a R₁-module, then the chain complex of R₂-modules of X with coefficients in R₂ ⊗[R₁] M₁ identifies to the extensions of scalars of the chain complex of R₁-modules of X with coefficients in M₁. In this file, we obtain a formulation of this result where the extension of scalars functor ModuleCat R₁ ⥤ ModuleCat R₂ is replaced by an arbitrary functor F : C ⥤ D which commutes with coproducts.

noncomputable def SSet.chainComplexFunctorObjCompMapIso {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasCoproducts D] (F : CategoryTheory.Functor C D) [F.Additive] [∀ (T : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete T) F] (R : C) : ((chainComplexFunctor C).obj R).comp (F.mapHomologicalComplex (ComplexShape.down ℕ)) ≅ (chainComplexFunctor D).obj (F.obj R)

The chain complex functor commutes with the "extension of scalars". More precisely, if F : C ⥤ D is a functor which commutes with arbitrary coproducts, R : C and X : SSet, then the chain complex of X with coefficients in F.obj R is obtained by applying F to the chain complex of X with coefficients in R.

Equations

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

@[simp]

theorem SSet.map_ιChainComplex_chainComplexFunctorObjCompMapIso_hom_app_f {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasCoproducts D] (X : SSet) (F : CategoryTheory.Functor C D) [F.Additive] [∀ (T : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete T) F] {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (F.map (X.ιChainComplex x)) (((chainComplexFunctorObjCompMapIso F R).hom.app X).f n) = X.ιChainComplex x

@[simp]

theorem SSet.map_ιChainComplex_chainComplexFunctorObjCompMapIso_hom_app_f_assoc {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasCoproducts D] (X : SSet) (F : CategoryTheory.Functor C D) [F.Additive] [∀ (T : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete T) F] {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : D} (h : (((chainComplexFunctor D).obj (F.obj R)).obj X).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (X.ιChainComplex x)) (CategoryTheory.CategoryStruct.comp (((chainComplexFunctorObjCompMapIso F R).hom.app X).f n) h) = CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) h