on the definition of Submodule.map

Stream: mathlib4

[Filippo A. E. Nuccio]

Suppose we are given two comm rings (or whatever) R and S, together with a ring hom σ : R →+* S. Fix also an R-module M, an S-module N and an additive map f : M →+ N that is σ-semilinear.

Given any submodule p ⊆ M, docs#Submodule.map defines its image as a submodule of N, under the assumption that σ is surjective. This is in contrast with docs#Ideal.map, that defines the (ideal structure on the) image of an ideal simply by taking the span of the image. The reason is clear: if we want to define the carrier as simply being the image, we need surjectivity of the ring hom to ensure that the gadget is smul-closed. On the other hand, it is very easy to prove that if we rather define p.map f to be Submodule.span S (f '' p), this is always well defined and coincides with the current definition in the case that σ is surjective.

So I wonder why the definition was chosen to be as it is and if we should not revert things.

Let me add that reverting things would need to add the import Mathlib.LinearAlgebra.Span.Defsto Mathlib.Algebra.Module.Submodule.Map but this seems hardly problematic. Also, the copyright dates back to 2017, so there might simply be a historical reason.

[Aaron Liu]

I think we care a little about the carrier being defea to set image

[Filippo A. E. Nuccio]

Well, I'm not 100% convinced. I agree this could be nice, but the price we're paying is too high especially since we've developped a good deal of the linear algebra library using semilinear maps, and for something as basic as the image of a submodule we need to add surjectivity...

[Sébastien Gouëzel]

I agree it would be nice to change the definition. The only way to know if there are places where the defeq is important is to try the refactor!

[Filippo A. E. Nuccio]

OK, I'm happy then to start and try it.

[Johan Commelin]

I think the reason is historical: for ideals it is clear that you need the span, as you point out. But in the "ordinary case" where M and N are two R-modules, and \sigma = id, then you don't need the span. And that's the case that is basically always treated in the informal literature.

I think this is a cool realization. I for one always thought that "ideals are just submodules of the ring itself" was a slightly bad heuristic because of "yes, but map is different"!

But you are telling me that map shouldn't be different at all! I like that.

[Riccardo Brasca]

I 100% agree with @Johan Commelin ! I used a lot that part of the library, and if we are able to get rid of Ideal.map (in the sense that it becomes a special case of Submodule.map) it would be great!

[Filippo A. E. Nuccio]

OK, just to sum up: @Johan Commelin and @Riccardo Brasca you also agree if I start the refactor (and in particular refactor Ideal.map to be a special case)?

[Filippo A. E. Nuccio]

I'm working on the refactor: following what has recently been agreed upon concerning morphism hierarchy, I am planning to change the variable

(F : Type*) [SemilinearMapClass F σ₁₂ M M₂] (f : F)

to variable (f : M →ₛₗ[σ₁₂] M₂) in all definitions and in all lemmas that actually coerce, in their statement, f : F to something else than a bare function (e.g. to either a semilinear map, or to an additive one), like docs#Submodule.mem_map or MonoidHom.coe_toAdditive_map. On the other hand, I can keep/reintroduce the class variable in things like Submodule.apply_coe_mem_map. Is this OK?

[Yaël Dillies]

No, Submodule.apply_coe_mem_map has f appearing in Submodule.map. Therefore it must be f : M →ₛₗ[σ₁₂] M₂.

[Eric Wieser]

Filippo A. E. Nuccio said:

On the other hand, it is very easy to prove that if we rather define p.map f to be Submodule.span S (f '' p),

If we did this, then presumably we would not even require that f is a bundled function?

[Filippo A. E. Nuccio]

Eric Wieser said:

Filippo A. E. Nuccio said:

On the other hand, it is very easy to prove that if we rather define p.map f to be Submodule.span S (f '' p),

If we did this, then presumably we would not even require that f is a bundled function?

Oh right!