Zulip Chat Archive

Stream: new members

Topic: restrict_scalars


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 09 2020 at 06:42):

restrict_scalars is used to generate a module instance

view this post on Zulip Kenny Lau (Sep 09 2020 at 06:43):

docs#is_scalar_tower is used to prove anything about them

view this post on Zulip Kenny Lau (Sep 09 2020 at 06:43):

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

view this post on Zulip Kenny Lau (Sep 09 2020 at 06:44):

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

view this post on Zulip 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

view this post on Zulip Frédéric Dupuis (Sep 09 2020 at 18:42):

Seems to work -- thanks a lot!

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 10 2020 at 06:09):

what's the issue?

view this post on Zulip 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