extension of scalars for a module, complexification

Stream: Is there code for X?

[Juho Kupiainen]

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

[Eric Wieser]

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

[Heather Macbeth]

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

[Heather Macbeth]

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]

@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]

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

[Eric Wieser]

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.

[Oliver Nash]

@Eric Wieser @Johan Commelin I'd like to use extension of scalars for some of my work. How about I adopt #4773?

[Eric Wieser]

Sounds good to me - last time I touched it was to remove some duplicate lemmas, but I guess I forgot to clean-up the places those duplicates were being used, hence the CI failures

[Oliver Nash]

Yeah it's nearly working for me locally now. I'll push up once I've got it building and then take a closer look at what it does.