Zulip Chat Archive

Stream: maths

Topic: localization map for modules


view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 12:33):

Given a ring R and a localization S of R, I can find in ring_theory\localization the definition of the localization map f : R -> S as a ring homomorphism, and also the localization of an ideal I < R as an ideal of R. But I can't find the corresponding localization map f : I -> f(I) (as a R-linear map, say). Is it pertinent to add this definition to ring_theory\localization?

view this post on Zulip Johan Commelin (Oct 28 2020 at 12:39):

I think Reid Barton is working on generalizing localization

view this post on Zulip Johan Commelin (Oct 28 2020 at 12:39):

But you are right that atm we don't have this for modules

view this post on Zulip Reid Barton (Oct 28 2020 at 12:46):

If it's just I -> f(I) as an R-linear map you want, I assume you can construct it using generic stuff about ideals (since this doesn't depend on f being a localization). What I think we don't have is the universal property for the S-module f(I).

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 13:10):

Well, atm I would need this for ideals, but it would make more sense to add this for arbitrary modules. If you're working on this, at any rate, I can use the result for ideals for now.

view this post on Zulip Adam Topaz (Oct 28 2020 at 13:53):

There are really two constructions going on here. It just so happens that they agree in the case of localization since localizations are flat.

view this post on Zulip Adam Topaz (Oct 28 2020 at 13:54):

But last time I checked mathlib didn't have base-change of modules. Is that still the case?

view this post on Zulip Johan Commelin (Oct 28 2020 at 13:56):

There is a PR

view this post on Zulip Johan Commelin (Oct 28 2020 at 13:56):

But I'm working on too many things atm.

view this post on Zulip Johan Commelin (Oct 28 2020 at 13:57):

#4773

view this post on Zulip Johan Commelin (Oct 28 2020 at 13:57):

Reid suggests that we try characteristic predicates, so the PR needs some work

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:00):

Adam Topaz said:

There are really two constructions going on here. It just so happens that they agree in the case of localization since localizations are flat.

I agree that localizations are flat, but to simply say that S1MS^{-1}M is an RR-module through the structural map turning S1RS^{-1}R into an RR-algebra this is not needed (where I have changed notations slightly, SS is now the localizing monoid)

view this post on Zulip Reid Barton (Oct 28 2020 at 14:03):

In this case I think there are really three constructions here!

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:03):

True...

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:04):

Oh, what I meant was this: If AA is a commutative ring, ABA \to B a commutative flat AA-algebra and MM is an AA-module, and NN a submodule of MM, then the base-change BANB \otimes_A N is canonicaally isomorphic to the BB-submodule of BAMB \otimes_A M generated by the image of NN.

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:06):

At any rate, what's your suggestion for the quickest way to say that if II is an ideal of RR which is f.g. (or noetherian, since I am assuming RR is), then the fractional ideal f(I)f(I) is also noetherian as a RR-module, where ff is a localization map?

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:07):

Since I am localizing at non-zero-divisors, the map If(I)I\to f(I) is injective, and this would give me the result, but this map is not yet in mathlib, hence my question.

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:07):

Oh, you're literally looking at the image of II, and not the submodule it generates?

view this post on Zulip Reid Barton (Oct 28 2020 at 14:08):

I'd be surprised if the map is not in mathlib, I think you might just be looking in the wrong place...?

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:08):

Reid Barton said:

I'd be surprised if the map is not in mathlib, I think you might just be looking in the wrong place...?

Well, this happens to me very often, so it is highly possible.

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:08):

Adam Topaz said:

Oh, you're literally looking at the image of II, and not the submodule it generates?

Yes

view this post on Zulip Reid Barton (Oct 28 2020 at 14:09):

Oh, I didn't realize this either

view this post on Zulip Johan Commelin (Oct 28 2020 at 14:09):

Hmm, can't you use submodule.map anyway?

view this post on Zulip Johan Commelin (Oct 28 2020 at 14:10):

And then prove that it the span step doesn't do anything.

view this post on Zulip Reid Barton (Oct 28 2020 at 14:11):

So isn't the question just about the following situation? R a ring, f : M -> N a map of R-modules, I a submodule of M, and you want the map I -> f(I) as a map of R-modules.

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:12):

Yes, because to apply @Johan Commelin 's suggestion I need a submodule map

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:12):

(I could also do with the map of rings looking at an ideal as a submodule of RR, this is probably what he meant)

view this post on Zulip Reid Barton (Oct 28 2020 at 14:13):

Where in fact M = R, N is a localization of R (along the map f), but you don't care about the fact that N is again a ring.

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:13):

An ideal is defined as a submodule of the ring, so by definition I : submodule A A.

view this post on Zulip Reid Barton (Oct 28 2020 at 14:13):

Right and now I realize this is what Johan was suggesting too.

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:13):

If ABA \to B is the localization, you would just need to use docs#submodule.map which would have type
submodule A A \to submodule A B.

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:14):

This is of course assuming that the localzation B has an A-module instance somewhere in mathlib, and the localzation map A \to B can be considered as an A-linear map, which it should :)

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:14):

I agree, I got trapped in thinking about generalizing this to modules and forgot that an ideal is a submodule of the ring itself...

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:14):

Adam Topaz said:

This is of course assuming that the localzation B has an A-module instance somewhere in mathlib, which it should :smile:

Yes, I think I've seen it recently: it is docs#localization_map.lin_coe

view this post on Zulip Reid Barton (Oct 28 2020 at 14:15):

Then I guess somewhere there ought to be the factorization of an R-module map through its image

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:20):

Great, I think it worked. Thanks!

view this post on Zulip Reid Barton (Oct 28 2020 at 14:21):

How did you end up getting the map from the submodule to its image?

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 14:21):

Reid Barton said:

How did you end up getting the map from the submodule to its image?

I am still working on it, I'll soon be back with an answer or a question... :wink:

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 18:49):

(deleted)

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 18:49):

Filippo A. E. Nuccio said:

Reid Barton said:

How did you end up getting the map from the submodule to its image?

I am still working on it, I'll soon be back with an answer or a question... :wink:

This is what I ended up doing: given the localization map g : R -> K and an ideal J in R, I defined
1) the restriction of g to J
let res_g := linear_map.dom_restrict g.lin_coe J,
2) Its image
let g_of_J := linear_map.range_restrict res_g,
obtaining
g_of_J: ↥J →ₗ[R₁] ↥(res_g.range) := res_g.range_restrict
and finally I proved
have h_im_g : res_g.range = (J : fractional_ideal g),
which is pretty straightforward.

view this post on Zulip Johan Commelin (Oct 28 2020 at 18:53):

Can't you combine (1) and (2) with submodule.map?

view this post on Zulip Johan Commelin (Oct 28 2020 at 18:53):

submodule.map g.lin_coe J? Or something like that.

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 18:54):

Let me try

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 18:55):

Well, but it does not give me the map, only the submodule (whereas I also need the map, later on, to apply that a sujection sends noetherian to noetherian).

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 18:55):

(Have to run -- sorry!)

view this post on Zulip Johan Commelin (Oct 28 2020 at 18:56):

Aah, ok.

view this post on Zulip Johan Commelin (Oct 28 2020 at 18:56):

In that case you might need to do what you did

view this post on Zulip Johan Commelin (Oct 28 2020 at 18:57):

But isn't everything in sight noetherian in your application?

view this post on Zulip Anne Baanen (Oct 28 2020 at 18:58):

(Isn't linear_map.cod_restrict \circ linear_map.dom_restrict called linear_map.restrict?)

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 20:39):

Johan Commelin said:

Aah, ok.

Well, almost: the field of fractions K is certainly not noetherian, but this is were the localization map g takes values. Hence I need to "modify" it so that it takes values into its image, which is noetherian. Given Macron's recent announcements, I guess I'll have time to do so in the coming days... :wink:

view this post on Zulip Filippo A. E. Nuccio (Oct 28 2020 at 20:40):

Anne Baanen said:

(Isn't linear_map.cod_restrict \circ linear_map.dom_restrict called linear_map.restrict?)

Unfortunately, for the time being it seems to me that linear_map.restrict is only the restriction of an endomorphism (domain=codomain=M), whereas I am in a more general setting where the domain and codomain differ.


Last updated: May 06 2021 at 18:20 UTC