## Stream: maths

### Topic: localization map for modules

#### 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?

#### Johan Commelin (Oct 28 2020 at 12:39):

I think Reid Barton is working on generalizing localization

#### Johan Commelin (Oct 28 2020 at 12:39):

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

#### 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).

#### 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.

#### 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.

#### 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?

There is a PR

#### Johan Commelin (Oct 28 2020 at 13:56):

But I'm working on too many things atm.

#4773

#### Johan Commelin (Oct 28 2020 at 13:57):

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

#### Filippo A. E. Nuccio (Oct 28 2020 at 14:00):

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 $S^{-1}M$ is an $R$-module through the structural map turning $S^{-1}R$ into an $R$-algebra this is not needed (where I have changed notations slightly, $S$ is now the localizing monoid)

#### Reid Barton (Oct 28 2020 at 14:03):

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

True...

#### Adam Topaz (Oct 28 2020 at 14:04):

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

#### 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 $I$ is an ideal of $R$ which is f.g. (or noetherian, since I am assuming $R$ is), then the fractional ideal $f(I)$ is also noetherian as a $R$-module, where $f$ is a localization map?

#### Filippo A. E. Nuccio (Oct 28 2020 at 14:07):

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

#### Adam Topaz (Oct 28 2020 at 14:07):

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

#### 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...?

#### 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.

#### Filippo A. E. Nuccio (Oct 28 2020 at 14:08):

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

Yes

#### Reid Barton (Oct 28 2020 at 14:09):

Oh, I didn't realize this either

#### Johan Commelin (Oct 28 2020 at 14:09):

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

#### Johan Commelin (Oct 28 2020 at 14:10):

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

#### 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.

#### Filippo A. E. Nuccio (Oct 28 2020 at 14:12):

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

#### 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 $R$, this is probably what he meant)

#### 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.

#### 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.

#### Reid Barton (Oct 28 2020 at 14:13):

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

#### Adam Topaz (Oct 28 2020 at 14:13):

If $A \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.

#### 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 :)

#### 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...

#### Filippo A. E. Nuccio (Oct 28 2020 at 14:14):

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

#### 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

#### Filippo A. E. Nuccio (Oct 28 2020 at 14:20):

Great, I think it worked. Thanks!

#### Reid Barton (Oct 28 2020 at 14:21):

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

#### 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:

(deleted)

#### 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.

#### Johan Commelin (Oct 28 2020 at 18:53):

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

#### Johan Commelin (Oct 28 2020 at 18:53):

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

Let me try

#### 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).

#### Filippo A. E. Nuccio (Oct 28 2020 at 18:55):

(Have to run -- sorry!)

Aah, ok.

#### Johan Commelin (Oct 28 2020 at 18:56):

In that case you might need to do what you did

#### Johan Commelin (Oct 28 2020 at 18:57):

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

#### Anne Baanen (Oct 28 2020 at 18:58):

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

#### 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:

#### 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