Zulip Chat Archive

Stream: maths

Topic: restriction of scalars


view this post on Zulip Sebastien Gouezel (Nov 17 2019 at 16:33):

Is there anything about restriction of scalars in mathlib? I need to interpret a -vector space as an -vector space, but I don't want to reinvent the wheel. A quick grep did not show anything, but maybe I did not use the right keywords.

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 16:34):

I was looking for precisely this last week and couldn't find anything. Looking at it now I realise that it's some kind of comap isn't it, a map A -> B gives a map module B -> module A

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 16:35):

except that module B maybe doesn't exist in that form.

view this post on Zulip Sebastien Gouezel (Nov 17 2019 at 16:38):

Yes, you have a nice categorical interpretation, as emphasized in https://en.wikipedia.org/wiki/Change_of_rings. What I need is the down-to-earth version, of course, i.e., a concrete real vector space structure on a given type with a concrete complex vector space structure. I'll cook up something then.


Last updated: May 10 2021 at 08:14 UTC