# Zulip Chat Archive

## Stream: new members

### Topic: restrict_scalars

#### Frédéric Dupuis (Sep 09 2020 at 02:41):

I'm having a lot of trouble with the `restrict_scalars`

mechanism. Here's an MWE of what I'm trying to do:

```
import data.complex.is_R_or_C
variables {α 𝕜 : Type*}
[nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜] [is_R_or_C 𝕜]
[add_comm_group α] [semimodule 𝕜 α]
example (K : set α) (h : convex K) : true := sorry
```

The problem is that `convex K`

requires an instance of `semimodule ℝ α`

. Casting `K`

to a `set (semimodule.restrict_scalars ℝ 𝕜 α)`

doesn't work for a reason I don't understand, it still looks for a `semimodule ℝ α`

when I do that. Also, registering the appropriate instance also fails, since that makes trouble with `semimodule ℝ ℝ`

.

Any advice?

#### Kenny Lau (Sep 09 2020 at 06:42):

`restrict_scalars`

is used to generate a module instance

#### Kenny Lau (Sep 09 2020 at 06:43):

docs#is_scalar_tower is used to prove anything about them

#### Kenny Lau (Sep 09 2020 at 06:43):

we should put this in the docstring of docs#semimodule.restrict_scalars

#### Kenny Lau (Sep 09 2020 at 06:44):

also since `k`

is a field I guess you should say `vector_space`

instead of `semimodule`

#### Kenny Lau (Sep 09 2020 at 06:45):

```
import data.complex.is_R_or_C
variables {α 𝕜 : Type*}
[nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜] [is_R_or_C 𝕜]
[add_comm_group α] [vector_space 𝕜 α] [vector_space ℝ α] [is_scalar_tower ℝ 𝕜 α]
example (K : set α) (h : convex K) : true := sorry
```

#### Frédéric Dupuis (Sep 09 2020 at 18:42):

Seems to work -- thanks a lot!

#### Frédéric Dupuis (Sep 10 2020 at 00:36):

Now I have a follow-up question: is there a good way to deal with subspaces with these scalar towers? For example, suppose I'd like to show that a `subspace 𝕜 α`

is convex, is there a clean way to do that?

#### Kenny Lau (Sep 10 2020 at 06:09):

what's the issue?

#### Frédéric Dupuis (Sep 10 2020 at 13:53):

To prove that a subspace is convex, one would want to use `subspace.convex`

, which only works for `subspace ℝ α`

. So as far as I can tell, one would have to contruct a `subspace ℝ α`

out of the `subspace 𝕜 α`

, and add some lemmas showing that their carriers are the same, etc. I was hoping that there was some easier way that I had overlooked, but maybe I'm just the first to run into this issue...

Last updated: May 12 2021 at 04:19 UTC