Complexification of a real vector space

Stream: Is there code for X?

[Arien Malec]

I assume this (Exercise 1B Problem 7) from Axler's Linear Algebra is a one liner in Mathlib, but what one liner is it?

Suppose 𝑉 is a real vector space.
• The complexification of 𝑉, denoted by 𝑉𝐂 , equals 𝑉 × 𝑉. An element of
𝑉𝐂 is an ordered pair( 𝑢,𝑣),where𝑢,𝑣 ∈ 𝑉, but we write this as 𝑢+𝑖𝑣.
• Addition on 𝑉𝐂 is defined by
(𝑢1 +𝑖𝑣1)+(𝑢2 +𝑖𝑣2) = (𝑢1 +𝑢2)+𝑖(𝑣1 +𝑣2) for all 𝑢1,𝑣1,𝑢2,𝑣2 ∈𝑉.
• Complex scalar multiplication on 𝑉𝐂 is defined by (𝑎+𝑏𝑖)(𝑢+𝑖𝑣) = (𝑎𝑢−𝑏𝑣)+𝑖(𝑎𝑣+𝑏𝑢)
for all 𝑎, 𝑏 ∈ 𝐑 and all 𝑢, 𝑣 ∈ 𝑉.
Prove that with the definitions of addition and scalar multiplication as above,
𝑉𝐂 is a complex vector space.

[Eric Rodriguez]

This will be done with the tensor product in mathlib

[Arien Malec]

Something like:

variable [Module ℝ V]
#synth Module ℝ (TensorProduct ℝ V V)

?

[Eric Wieser]

No, more like:

import Mathlib

variable {V} [AddCommGroup V] [Module ℝ V]
open scoped TensorProduct

#synth Module ℂ (ℂ ⊗[ℝ] V)

[Eric Wieser]

You can then prove your first bullet point as

def prodEquivComplexTensor : V × V ≃ ℂ ⊗[ℝ] V := sorry

and the second one as

theorem smul_def (c : ℂ) (a : V × V) :
    c • prodEquivComplexTensor b = prodEquivComplexTensor (c.re • a.1 - c.im • a.2, c.re • a.1 + c.im • a.2) := by
  sorry

[Arien Malec]

I've been beating my head against the first theorem without seeing any cracks in the armor -- any Mathlib theorems that simply or open up the proof.

[Richard Copley]

TensorProduct.prodLeft or TensorProduct.prodRight should help.

[Arien Malec]

I'm having trouble getting the right types in place.... prodLeft wants to distribute a product over a tensor product.

[Richard Copley]

Can you show ℂ ≃ₗ[R] (ℝ × ℝ)? (It's hard to guess exactly how far you've got.)

[Arien Malec]

huh... Nice idea...

[Arien Malec]

You can assume that I've been searching for relating things in Mathlib and trying to see if I can find a chain of structural decomposition to force fit.

[Richard Copley]

Then there's TensorProduct.rid and TensorProduct.lid.