Stream: Is there code for X?
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