restrict_scalars

Stream: new members

[Frédéric Dupuis]

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]

restrict_scalars is used to generate a module instance

[Kenny Lau]

docs#is_scalar_tower is used to prove anything about them

[Kenny Lau]

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

[Kenny Lau]

also since k is a field I guess you should say vector_space instead of semimodule

[Kenny Lau]

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]

Seems to work -- thanks a lot!

[Frédéric Dupuis]

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]

what's the issue?

[Frédéric Dupuis]

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...