Commit 2022-08-10 17:41 286d6750

View on Github →

feat(algebra/category/Module/change_of_rings): restriction of scalars (#15672) Given a ring homomorphism $f : R\to S$, there is a functor from $S$-module to $R$-module. In #15564, it will proven that extension of scalars $\dashv$ restriction of scalars

Estimated changes

Created src/algebra/category/Module/change_of_rings.lean

added def category_theory.Module.restrict_scalars.map'

added theorem category_theory.Module.restrict_scalars.map_apply

added def category_theory.Module.restrict_scalars.obj'

added theorem category_theory.Module.restrict_scalars.smul_def'

added theorem category_theory.Module.restrict_scalars.smul_def

added def category_theory.Module.restrict_scalars