Zulip Chat Archive

Stream: Is there code for X?

Topic: extension of scalars for a module, complexification


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

view this post on Zulip Eric Wieser (Jan 14 2021 at 12:46):

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

view this post on Zulip Heather Macbeth (Jan 14 2021 at 12:47):

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

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

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

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

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