## Stream: Is there code for X?

### Topic: base change of module

#### Reid Barton (Sep 02 2020 at 22:33):

Do we have the construction $S \otimes_R M$ as an $S$-module for an $R$-module $M$?

#### Reid Barton (Sep 02 2020 at 23:00):

Or relatedly, localization of modules?

#### Johan Commelin (Sep 03 2020 at 04:09):

@Reid Barton Nope, I don't think we have that. But I wouldn't mind being proven wrong.

#### Reid Barton (Sep 09 2020 at 14:39):

So I'm mainly interested in localization of modules at the moment. I think it makes sense to treat this separately from general base change since it admits a more elementary construction/characteristic predicate. Later we could show that a map $M \to S^{-1}M$ exhibiting a module as a localization is also a map exhibiting the base change of $M$ from $R$ to $S^{-1} R$ (and vice versa).

#### Reid Barton (Sep 09 2020 at 14:41):

Is there a particular reason that the current monoid_localization seems to prefer "right fractions" $ms^{-1}$ over "left fractions $s^{-1}m$? The latter seems more convenient for modules, given mathlib's strong preference for left modules over right modules.

#### Reid Barton (Sep 09 2020 at 14:41):

I'm guessing the reason is just that we write fractions $a / b$ with the denominator on the right, but I could be missing something.

#### Reid Barton (Sep 09 2020 at 14:42):

Also, do we already have bundled morphisms of sets equipped with an action of a monoid? Like linear_map but less... linear?

#### Johan Commelin (Sep 09 2020 at 14:42):

Reid Barton said:

Also, do we already have bundled morphisms of sets equipped with an action of a monoid? Like linear_map but less... linear?

@Kenny Lau Didn't you do this?

#### Kenny Lau (Sep 09 2020 at 15:03):

docs#mul_action_hom

#### Reid Barton (Sep 09 2020 at 15:04):

Thanks. (I think the data/algebra/group_theory/ring_theory/linear_algebra directories could use some reorganization...)

#### Reid Barton (Sep 09 2020 at 16:49):

Reid Barton said:

I'm guessing the reason is just that we write fractions $a / b$ with the denominator on the right, but I could be missing something.

I found out one additional reason: it makes Lean smarter about where to insert coercions...

#### Johan Commelin (Sep 09 2020 at 16:49):

Maybe we should switch to right modules (-;

#### Adam Topaz (Sep 09 2020 at 16:52):

Maybe one should not think of localization base-change of modules as a tensor product :speechless:

#### Reid Barton (Sep 09 2020 at 16:57):

Regardless of whether I think in terms of tensor products, if I only know about left modules and I want to invert elements $s \in S \subset R$ on a module $M$, I need to have $s$ acting on the left of elements of $M$, yes?

#### Adam Topaz (Sep 09 2020 at 16:58):

Oh I see what you want. yes

#### Adam Topaz (Sep 09 2020 at 17:57):

Wait, maybe I'm not sure about what you actually want to do. If you forget about tensor products altogether, the universal property would say that for every $s \in S$ and every $m \in M$, there exists some element $m_s$ in the localization such that $s \cdot m_s = m$ (together with the usual axioms of a module over the localization). Is this what you need?

#### Adam Topaz (Sep 09 2020 at 17:59):

Note that the monoid localization is not the right notion for modules here, since that's a multiplicative operation.

#### Reid Barton (Sep 09 2020 at 20:16):

Is it intentional that we don't have instances like

instance (S : submonoid M) (X : Type*) [has_scalar M X] : has_scalar S X :=
{ smul := λ s x, (s : M) • x }


Or am I perhaps just overlooking them?

#### Kenny Lau (Sep 09 2020 at 20:27):

docs#algebra.of_subring

#### Kevin Buzzard (Sep 09 2020 at 20:57):

eew is_subring

Last updated: May 07 2021 at 23:11 UTC