base change of module

Stream: Is there code for X?

[Reid Barton]

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

[Reid Barton]

Or relatedly, localization of modules?

[Johan Commelin]

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

[Reid Barton]

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]

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]

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]

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

[Johan Commelin]

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]

docs#mul_action_hom

[Reid Barton]

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

[Reid Barton]

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]

Maybe we should switch to right modules (-;

[Adam Topaz]

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

[Reid Barton]

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]

Oh I see what you want. yes

[Adam Topaz]

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]

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

[Reid Barton]

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]

docs#algebra.of_subring

[Kevin Buzzard]

eew is_subring