Stream: Is there code for X?
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):
linear_map.map seem to come up empty in the api search
Alex J. Best (Dec 03 2020 at 23:19):
Adam Topaz (Dec 03 2020 at 23:20):
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
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
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