Stream: Is there code for X?

Topic: Image of submodule under linear map

Adam Topaz (Dec 03 2020 at 23:03):

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

Adam Topaz (Dec 03 2020 at 23:04):

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

thanks

Kevin Buzzard (Dec 04 2020 at 00:13):

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 (Dec 04 2020 at 00:26):

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

Reid Barton (Dec 04 2020 at 00:28):

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

Kevin Buzzard (Dec 04 2020 at 00:31):

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 (Dec 04 2020 at 00:31):

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 (Dec 04 2020 at 00:32):

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

Patrick Massot (Dec 04 2020 at 08:19):

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.

Last updated: May 19 2021 at 02:10 UTC