## Stream: maths

### 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):

except that 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