Commit 2026-08-11 15:45 c8155c79

feat(AlgebraicTopology/SimplicialSet/Homology): extension of scalars (#38965) 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. (As SimplicialObject is now an abbrev for a category of functors, SimplicialObject.whiskering is also made an abbrev here.)