mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebra/category/Module/change_of_rings): extension of scalars

Open jjaassoonn opened this issue 3 years ago • 5 comments

Given a ring homomorphism $f : R \to S$ between commutative rings, the extension of scalars functor from $R$-module to $S$-module. In #15564 it will proven that extension of scalars $\dashv$ restriction of scalars

  • [x] depends on: #15672

Open in Gitpod

jjaassoonn avatar Jul 25 '22 01:07 jjaassoonn

Is there a reason why doc#tensor_product.left_module is not used?

erdOne avatar Jul 27 '22 13:07 erdOne

Is there a reason why doc#tensor_product.left_module is not used?

Maybe I am missing something, but to use tensor_product.left_module, M needs to be an S-module where it is an R-module?

jjaassoonn avatar Jul 28 '22 17:07 jjaassoonn

I meant that we should be able to get an S-action on S ⊗[R] M for free.

erdOne avatar Aug 02 '22 22:08 erdOne

Sorry for the late reply -- I saw your last comment before the edit and there isn't a GitHub notification for comment edits.

erdOne avatar Aug 02 '22 22:08 erdOne

This PR/issue depends on:

  • ~~leanprover-community/mathlib#15672~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Aug 10 '22 20:08 mathlib-dependent-issues-bot

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 31 '22 14:08 bors[bot]