Zulip Chat Archive

Stream: Is there code for X?

Topic: Image of submodule under linear map


view this post on Zulip 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)?

view this post on Zulip 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

view this post on Zulip Alex J. Best (Dec 03 2020 at 23:19):

docs#submodule.map ?

view this post on Zulip Adam Topaz (Dec 03 2020 at 23:20):

thanks

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Reid Barton (Dec 04 2020 at 00:28):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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