Image of submodule under linear map

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have some code for the image of a submodule under a linear map (as a submodule of the target)?

[Adam Topaz]

Both linear_map.image and linear_map.map seem to come up empty in the api search

[Alex J. Best]

docs#submodule.map ?

[Adam Topaz]

thanks

[Kevin Buzzard]

I was confused by this for ages :-) For me, the linear_map was doing the mapping. Chris once tried to explain to me that this .map was the same as functor.map and I always figured the linear_map was the functor, but somehow the submodule is the functor. I'm still confused by this point.

[Adam Topaz]

IMO it makes more sense to write f.map N as opposed to N.map f. Alas...

[Reid Barton]

The real crime is that there is no ${}_*$ Unicode character

[Kevin Buzzard]

If you have subgroups and normal subgroups, and you want to comap, you can use subgroup.comap and normal_subgroup.comap (at least if normal subgroups were bundled, which I think is now the plan, except nobody did it yet). You can't do this trick if it's group_hom.comap.

[Adam Topaz]

I see so I'm supposed to think of submodule as a functor from the category of modules to the category of types?

[Kevin Buzzard]

I think that this was Chris' point of view when he was explaining it to me, yes.

[Patrick Massot]

I think the actual reason is more prosaic. In the early cases of this situation, unbundled maps were involved so we got the habit of putting the map function in the namespace of the subobject. You could also have situations where a given type of bundled maps can push or pull several different types of subobjects.