localization map for modules

Stream: maths

[Filippo A. E. Nuccio]

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]

I think Reid Barton is working on generalizing localization

[Johan Commelin]

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

[Reid Barton]

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]

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]

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]

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

[Johan Commelin]

There is a PR

[Johan Commelin]

But I'm working on too many things atm.

[Johan Commelin]

#4773

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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 $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]

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

[Filippo A. E. Nuccio]

True...

[Adam Topaz]

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]

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]

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]

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

[Reid Barton]

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]

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]

Adam Topaz said:

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

Yes

[Reid Barton]

Oh, I didn't realize this either

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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]

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

[Filippo A. E. Nuccio]

(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]

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]

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

[Reid Barton]

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

[Adam Topaz]

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]

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]

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]

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

[Reid Barton]

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

[Filippo A. E. Nuccio]

Great, I think it worked. Thanks!

[Reid Barton]

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

[Filippo A. E. Nuccio]

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:

[Filippo A. E. Nuccio]

(deleted)

[Filippo A. E. Nuccio]

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]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

Let me try

[Filippo A. E. Nuccio]

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]

(Have to run -- sorry!)

[Johan Commelin]

Aah, ok.

[Johan Commelin]

In that case you might need to do what you did

[Johan Commelin]

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

[Anne Baanen]

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

[Filippo A. E. Nuccio]

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]

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.

[Andrew Yang]

Is there any active plans on localizing modules? Maybe @Jujian Zhang ?
If not, I will try and make some basic API by mimicking the is_localization stuff.
Probably something like

variables {R : Type u} [comm_ring R] (S : submonoid R)
variables {M M' : Type u} [add_comm_group M] [add_comm_group M']
variables [module R M] [module R M'] (f : M →ₗ[R] M')

class is_module_localization : Prop :=
(map_units [] : ∀ (x : S), is_unit (algebra_map R (module.End R M') x))
(surj [] : ∀ y : M', ∃ (x : M × S), x.2 • y = f x.1)
(eq_iff_exists [] : ∀ {x₁ x₂}, f x₁ = f x₂ ↔ ∃ c : S, c • x₁ = c • x₂)

I've also tried the tensor product API, but it seemed a bit hard to use.
It might be because there isn't a good predicate for tensor products, but I think we would still need special support for these anyway.

[Johan Commelin]

@Reid Barton You experimented with localising modules, right? Do you have something on a branch somewhere?

[Junyan Xu]

map_units could be replaced by surjectivity of scalar multiplication: ∀ (s : S) (x : M'), ∃ (y : M'), s • y = x (injectivity follows from the other two conditions; same for the ← direction of eq_iff_exists, and I'm not sure by what consideration that direction was included in the definition of is_localization). I think this is more similar to map_units in is_localization, since is_unit x is equivalent to ∃ z, x * z = 1 and also to ∀ y, ∃ z, x * z = y. I wonder if there would be any advantage to refactor is_localization through is_module_localization with f taken to be the docs#algebra.linear_map ...

[Jujian Zhang]

I was trying to find the same thing yesterday experimenting with defining quasicoherent sheaf of modules and ended up using "exactness" as definition because I couldn't localise module

[Jujian Zhang]

If no one is working on it, I could give it a try

[Andrew Yang]

I already have some API covering the most basic stuff. What I want eventually is that injectivity and surjectivity are local properties and that's about it. I'm not sure how much of this you would need though. If you are planning to use these soon I could squeeze out a PR tomorrow, and you can build more of the library based on your need.

[Adam Topaz]

Wouldn't it be better to try to come up with a is_base_change class and to characterize localization as a base change?

[Andrew Yang]

I agree that we should also come up with such a class, but I think there is still a need for such a specialized API. For example, some work needs to be done before we have an action of $R_p$ on $M_p$ to realize $M_p$ as the tensor product, or the fact that $R_p \times M \to R_p \otimes M$ is surjective should probably also get some decent API.

[Adam Topaz]

Well, we already have is_localization for algebras. So whatever you want to prove about localization of modules could be done with lemmas assuming is_localization and is_base_change. I don't see why we would need a custom class for localization of modules...

[Junyan Xu]

I think defining is_base_change isn't any easier than defining is_tensor_product, which seems to be an unsolved problem. Definition via the universal property seems to be the simplest and most natural and easy-to-use, though you have to be careful about the universes: you could use the max universe of the two modules' universes, or you could use the ring's universe as I showed here; both should be strong enough to imply the universal property for all universes. Using the presentation Relations->R[M]->M->0 and right exactness of tensoring you can also derive a characterization of the "kernel" of the bilinear map to the tensor product that only refers to elements of R,M,N, not even the ideals, somewhat similar to stacks#00HK (but also somewhat different and best stated using equality in finsupp), but it's asymmetric in M and N and won't be pleasant to use.

[Andrew Yang]

But I suppose most of the times when one wants to prove that some module is the localization of the other, it would be easier to show some (weaker but equivalent version of) the criteria in is_module_localization rather than to show the universal property.
Or is there a suitable generalization of such criteria onto arbitrary base change of modules?

[Andrew Yang]

I still think that base-changing along localizations have sufficiently better behavior to deserve some API on its own, but I'm also experimenting with predicates like is_tensor_productand see how far it could take me.

[Reid Barton]

Johan Commelin said:

Reid Barton You experimented with localising modules, right? Do you have something on a branch somewhere?

I had Ore localization of "modules" here but these are not with the additive structure yet, just sets acted on by monoids

[Reid Barton]

(but, it's the same construction)

[Adam Topaz]

What about something like this?

import ring_theory.tensor_product

variables {A B M N : Type*} [comm_ring A] [comm_ring B]
  [add_comm_group M] [add_comm_group N] [module A M] [module B N]
  [algebra A B]

open_locale tensor_product

def base_change (f : M →ₗ[A] restrict_scalars A B N) :
  B ⊗[A] M →ₗ[B] N :=
{ to_fun := tensor_product.lift
  { to_fun := λ b,
    { to_fun := λ m, b • (f m),
      map_add' := sorry,
      map_smul' := sorry },
    map_add' := sorry,
    map_smul' := sorry },
  map_add' := sorry,
  map_smul' := sorry }

class is_base_change (f : M →ₗ[A] restrict_scalars A B N) : Prop :=
(cond : function.bijective (base_change f))

I'm a little surprised that we don't have that version of base_change in mathlib. Maybe I missed it?

Sorry, that definition is wrong. let me fix it. It should be okay now.

[Junyan Xu]

Hmm, I see you can then define is_base_change f to mean that base_change f is an isomorphism, which is indeed simpler than general is_tensor_product for two modules (if one module is a ring A then it has 1 and we can embed M into A⊗M which makes things easier). However your approach starts from a B-module N while in @Andrew Yang's approach (for the localization case) there is only one ring R, modules M,N over R and a R-linear map between them; I don't know which is easier to work with. I looked for base_change a while ago and it's not in mathlib exactly in this form but you can combine docs#tensor_product.algebra_tensor_module.lift.equiv (case M = A) with docs#linear_map.ring_lmap_equiv_self to get it.

[Junyan Xu]

Actually for a general bilinear map we can also define is_tensor_product to mean that docs#tensor_product.lift is an isomorphism. However both this and @Adam Topaz's definition relies on comparison with a fixed construction, thus in a distinct flavor from is_localization. However I think there may not exist a simple predicate for is_tensor_product; even the universal property may not be of much use, and constructing isomorphisms with the "canonical" tensor product, possibly through exact sequences (presentation/resolution), or a bijection between bases in the free module case, might be the easiest way to show something is a tensor product. If that's the case, we may as well take the comparison-with-canonical definition for is_tensor_product.

[Adam Topaz]

Another concern I have with Andrew's definition above is that it would be very hard to use that definition in the case where we have an $A$-algebra which is a localization (in the sense of docs#is_localization ), but not "the" localization. If $A \to B$ is a localization, $M$ an $A$-module and $N$ a $B$-module, how would you formulate the condition of $N$ being a localization of $M$?

[Junyan Xu]

It seems not to be a concern to me. An identification of $N$ with the localization of $M$ is an $B$-linear equivalence $B\otimes_A M\cong N$, from which you get a $A$-linear map $f:M\to N$ by mapping $m$ to $1\otimes m$ then across the linear equiv. Then you may state that the $A$-linear map $f$ is_module_localization according to Andrew's definition.

Conversely given $A$-modules $M,N$ and an $A$-linear map between them that is_module_localization, with is_module_localization.map_units we can uniquely extend the $A$-action on $N$ to a $B$-action, thus get $B\otimes_A M\to N$ via your base_change, and with the other conditions we should be able to show this is an isomorphism.

[Junyan Xu]

Some more details (I think Andrew is working on this?):
is_module_localization.surj clearly implies the surjectivity of ${B\otimes_A M}\to N$. To establish injectivity, it suffices to construct a $B$-linear map $g: N\to B\otimes_A M$ and show the composition ${B\otimes_A M}\to B\otimes_A M$ is the identity. By is_module_localization.surj, for $n\in N$ there exists $m\in M, s\in S$ such that $s\cdot n=f(m)$, and we define $g(n)=s^{-1}\otimes m$. Note that every generator $as^{-1}\otimes m=s^{-1}\otimes am$ of $B\otimes_A M$ is of this form. Using is_module_localization.eq_iff_exists we show this is well-defined, then it's easy to see the composition is id and it's $A$-linear by choosing $am,s$ for $an$. But it's easy to show a $A$-linear map between $B$-modules is automatically $B$-linear, so we are done. This seems to be a substantially different way of showing a module is isomorphic to a tensor product (not via free modules + exact sequence) that I haven't imagined above!

[Junyan Xu]

The above constitutes a complete proof that the localization of module constructed by tensor product satisfies the is_module_localization predicate, and conversely every map satisfying the predicate is isomorphic to that explicit construction. There is another more direct construction as a quotient of $S\times M$, but maybe we don't need it.

[Junyan Xu]

Andrew Yang said:

I still think that base-changing along localizations have sufficiently better behavior to deserve some API on its own, but I'm also experimenting with predicates like is_tensor_productand see how far it could take me.

I think so too, and I think your definition is good, but may benefit from some adjustment in map_units as I suggested. My post above yours was about difficulties and thoughts about defining a general is_tensor_product predicate.

[Junyan Xu]

The current definition (map_units [] : ∀ (x : S), is_unit (algebra_map A (module.End A N) x)) has the advantage that it would directly allow A →+* module.End A N (scalar multiplication by A) be extended to B →+* module.End A N via docs#is_localization.lift, but is_localization.lift currently requires P=module.End A N be commutative, which is unnecessary and should be replaced by [ring P] (even though the image of A is certainly commutative so this problem can also be circumvented).

[Junyan Xu]

Actually the S in is_localization R S can also just be a ring; if you define is_localization R S assuming only [ring S], you can prove an instance [comm_ring S] using map_units and surj. Then you may replace [comm_ring S] by [ring S] for the rest of the file; even you don't replace, they should still apply to any [ring S] because of the inferred [comm_ring S] instance.

R still must be comm_ring, as required by algebra R S. Reid Barton's work can localization noncommutative rings, and maybe that will enter mathlib sometime soon, given the current refactors etc. to accommodate noncommutative algebra.

[Andrew Yang]

Is there a good way to show that $1 \otimes x = 0$ in $S^{-1}A \otimes_R M$ implies $sx = 0$ for some $s \in S$?
The only proof I can think of for now is to really construct that quotient and show that it satisfies the universal property of tensor products.

[Adam Topaz]

Take the morphism $R \to M$ sending 1 to x, and base change along the localization and use flatness?

[Adam Topaz]

The explicit approach is probably easier to formalize :neutral:

[Andrew Yang]

But I'm not sure how to show that localizations are flat without this result

[Adam Topaz]

Can you use the characterization of flatness in terms of ideals? I don't remember exactly how is_localization is defined, nor whether mathlib has the ideal characterization of flatness...

[Andrew Yang]

There is flatstuff which seems to be a WIP, so I guess it's not in mathlib.

[Kevin Buzzard]

If all you know is the universal property then I agree you have to make the model (although you don't have to prove the model satisfies the universal property). Patrick pointed the analogous statement for rings to me a year or two ago and it really surprised me. If you just know the universal property for $R[1/S]$ (an $R$-algebra such that maps from R sending S to units extend uniquely) then you can't isolate the kernel of $R\to R[1/S]$ until you observe that the annihilators of elements of $S$ are the kernel of the map to the usual model $R\times S/\sim$, although you don't have to prove that the model is universal, its existence is enough.

[Kevin Buzzard]

Here I'm a bit confused about whether A=R in the original question but assuming it is, you can prove S x M / ~ admits a map from $S^{-1}R\otimes_R M$ and hence $1\otimes x$ must be zero in this model so is annihilated by some element of S. Note that you don't have to prove the model is universal.

[Antoine Chambert-Loir]

Junyan Xu said:

The above constitutes a complete proof that the localization of module constructed by tensor product satisfies the is_module_localization predicate, and conversely every map satisfying the predicate is isomorphic to that explicit construction. There is another more direct construction as a quotient of $S\times M$, but maybe we don't need it.

The construction as a quotient of $S \times M$ is essential if you want to prove flatness properties of the ring extension $R \to S^{-1}R$, or study the kernel of the canonical map $M \to S^{-1}M$.

[Antoine Chambert-Loir]

In general, it is easy to prove that universal constructions exist, with set theoretical bounds for unique difficulty (for Lean, that would mean taking care about universes) because one can define the universal object as a kind of colimit. As in category theory, knowing that some adjoint functor exists does not give you hands on it and you often need a more concrete description. (Example : you have a “field of fractions” for non-commutative rings without zero divisors, the universal ring which has a map from your ring and in which every nonzero stuff is invertible, but you can't prove its nonzero. And sometimes it is.)

[Junyan Xu]

Indeed it's my oversight to claim that that was a complete proof; thanks for the clarification. I agree that the quotient of SxM construction is necessary as Kevin and you point out.

[Jujian Zhang]

I just build quotient of SxM construction at #14470.