Topic: restriction of scalars
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.
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
Kevin Buzzard (Nov 17 2019 at 16:35):
module B maybe doesn't exist in that form.
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