Zulip Chat Archive

Stream: Is there code for X?

Topic: base change of module


view this post on Zulip Reid Barton (Sep 02 2020 at 22:33):

Do we have the construction SRMS \otimes_R M as an SS-module for an RR-module MM?

view this post on Zulip Reid Barton (Sep 02 2020 at 23:00):

Or relatedly, localization of modules?

view this post on Zulip 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.

view this post on Zulip 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 MS1MM \to S^{-1}M exhibiting a module as a localization is also a map exhibiting the base change of MM from RR to S1RS^{-1} R (and vice versa).

view this post on Zulip Reid Barton (Sep 09 2020 at 14:41):

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

view this post on Zulip Reid Barton (Sep 09 2020 at 14:41):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 09 2020 at 15:03):

docs#mul_action_hom

view this post on Zulip 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...)

view this post on Zulip Reid Barton (Sep 09 2020 at 16:49):

Reid Barton said:

I'm guessing the reason is just that we write fractions a/ba / 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...

view this post on Zulip Johan Commelin (Sep 09 2020 at 16:49):

Maybe we should switch to right modules (-;

view this post on Zulip Adam Topaz (Sep 09 2020 at 16:52):

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

view this post on Zulip 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 sSRs \in S \subset R on a module MM, I need to have ss acting on the left of elements of MM, yes?

view this post on Zulip Adam Topaz (Sep 09 2020 at 16:58):

Oh I see what you want. yes

view this post on Zulip 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 sSs \in S and every mMm \in M, there exists some element msm_s in the localization such that sms=ms \cdot m_s = m (together with the usual axioms of a module over the localization). Is this what you need?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 09 2020 at 20:27):

docs#algebra.of_subring

view this post on Zulip Kevin Buzzard (Sep 09 2020 at 20:57):

eew is_subring


Last updated: May 07 2021 at 23:11 UTC