restriction of scalars

Stream: maths

[Sebastien Gouezel]

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]

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]

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

[Sebastien Gouezel]

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.