Stream: Is there code for X?

Topic: extension of scalars for a module, complexification

Juho Kupiainen (Jan 14 2021 at 12:43):

If it's already somewhere, the keywords "extension of scalars" and "complexification" might be a good idea to add.

Eric Wieser (Jan 14 2021 at 12:46):

Is docs#triv_sq_zero_ext close to what you're looking for?

Heather Macbeth (Jan 14 2021 at 12:47):

I don't think so, right? Juho wants https://en.wikipedia.org/wiki/Complexification

Heather Macbeth (Jan 14 2021 at 12:49):

Mathlib does have the "opposite" (restrict scalars) direction, eg docs#complex.normed_space.restrict_scalars_real. But I'm not sure about the "extend scalars" construction.

Heather Macbeth (Jan 14 2021 at 12:55):

@Johan Commelin Perhaps this PR will do it, once merged? #4773

Let R be a (semi)ring and A an R-algebra.
In this file we:
Define the A-module structure on A ⊗ M, for an R-module M.


Eric Wieser (Jan 14 2021 at 12:57):

I think we almost have the structure today via the asymmetry of src#tensor_product.has_scalar'.

Eric Wieser (Jan 14 2021 at 13:03):

Just tested - if you remove the unused typeclass arguments on that definition, then it provides a has_scalar ℂ (ℂ ⊗[ℝ] V). I don't think the same can be said of the semimodule instance, so bits of that PR are probably still warranted.

Last updated: May 07 2021 at 21:10 UTC