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.

[Arien Malec]

OK, coming back to this, I've done the brute force approach that Axler is looking for, by making a structure Vc with addition and multiplication as designated, and showing that it's a complex vector space.

(btw, when I look at introductions to complexification, the order of the tensor product is opposite to the (ℂ ⊗[ℝ] V) but rather (V ⊗[ℝ] ℂ)?)

The more mathy flavor of this is still beyond me. I think what @Eric Wieser is asking me for as a definition is the full Equiv structure? And I think we do this by mapping (fst,snd) = (1 ⊗[ℝ] fst) + (i ⊗[ℝ] snd) or something like that? And v ⊗[ℝ] ⟨re, im⟩ to (re • v, im • v) or ???

I'm not even sure that's the right track, but if it is, I don't know the syntax to make it work?

[Arien Malec]

(current code at https://github.com/arienmalec/axler)

[Eric Wieser]

Arien Malec said:

(btw, when I look at introductions to complexification, the order of the tensor product is opposite to the (ℂ ⊗[ℝ] V) but rather (V ⊗[ℝ] ℂ)?)

in mathlib V ⊗[ℝ] ℂ is not a ℂ-module, but ℂ ⊗[ℝ] V is. We can't have both without instance diamonds, and we picked the one that uses left-actions

[Eric Wieser]

Hopefully you can work out how to define the forward mapping. The trick with the reverse mapping is to use docs#TensorProduct.lift

[Arien Malec]

I think I figured out the forward mapping, but I'm swimming in a sea of notation. Like the difference between ⊗ₜ[ℝ] and ⊗[ℝ] where the first is "The canonical function M → N → M ⊗ N."

[Arien Malec]

toFun p := match p with
  |  ⟨fst, snd⟩ =>  (⟨1, 0⟩ ⊗ₜ[ℝ] fst) + ⟨0,1⟩ ⊗ₜ[ℝ] snd

[Jireh Loreaux]

Arien, are you familiar with tensor products mathematically, aside from Lean?

The first one creates elementary tensors. The second one forms the tensor product of two modules, and this is spanned by elementary tensors.

[Eric Wieser]

The difference between A ⊗[ℝ] B and a ⊗ₜ[ℝ] b is like the difference between α × β and (a, b)

[Eric Wieser]

Note that for ⊗ₜ you can almost always drop the [R] too

[Jireh Loreaux]

(with the key distinction that unlike Prod, not every element can be written this way)

[Eric Wieser]

(and also unlike Prod, there is usually more than one way to write the same element)

[Arien Malec]

Jireh Loreaux said:

Arien, are you familiar with tensor products mathematically, aside from Lean?

The first one creates elementary tensors. The second one forms the tensor product of two modules, and this is spanned by elementary tensors.

Not at any level of detail, which is certainly part of the issue here. So elementary tensors are to tensor products as vectors are to vector spaces?

[Eric Wieser]

I think a mildly better analogy is "as basis vectors are to vectors spaces"; not every vector is a basis vector, just as not every tensor is elementary

[Eric Wieser]

It may also help to know that a tensor product of vector spaces has as a basis the elementary tensors of the bases of the spaces; if $e_i$ is a basis for $E$ and $f_i$ is a basis for $F$ then $e_i \otimes f_j$ (note: two indices!) is a basis for $E \otimes F$.

[Arien Malec]

Some syntax help, please --

Following the hint, I got to: invFun tp := TensorProduct.lift liftFun tp where the type signature for liftFun is ℂ →ₗ[ℝ] V →ₗ[ℝ] (V × V), and I think it wants to take a complex number and a vector, and produce a Prod in the form of the smul definition above. But from a syntax perspective, when I write:

def liftFun: ℂ →ₗ[ℝ] V →ₗ[ℝ] (V × V) where the type of toFun wants to be ℂ → V →ₗ[ℝ] V × V not ℂ → V → V × V -- how do I write liftFun to be what I'm looking for?

(or, of course, if I'm completely off track....)

[Arien Malec]

(not sure how to get the unicode for R-linear maps to show up correctly.)

[Eric Wieser]

You probably want LinearMap.mk\_2

[Eric Wieser]

I think it would be easier to help you if you made a #mwe

[Eric Wieser]

Arien Malec said:

(not sure how to get the unicode for R-linear maps to show up correctly.)

I think you're referring to an Android bug; it looks fine on desktop

[Arien Malec]

Firefox bug apparently.

I seem to be missing an import somewhere, but hopefully this is close enough:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Complex.Module
import Mathlib.LinearAlgebra.TensorProduct


variable {V} [AddCommGroup V] [Module ℝ V]

open scoped TensorProduct

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

noncomputable def toFun (p: V × V) : (ℂ ⊗[ℝ] V) := match p with
  |  ⟨fst, snd⟩ => ((⟨1, 0⟩: ℂ) ⊗ₜ[ℝ] fst) + (⟨0,1⟩: ℂ)  ⊗ₜ[ℝ] snd

def liftFun: ℂ →ₗ[ℝ] V →ₗ[ℝ] (V × V) where
  toFun := sorry
  map_add' := sorry
  map_smul' := sorry

def prodEquivComplexTensor: V × V ≃ ℂ ⊗[ℝ] V where
  toFun p := toFun p
  invFun tp := TensorProduct.lift liftFun tp
  left_inv := sorry
  right_inv := sorry

[Eric Wieser]

Note that the final result is not as strong as the one you want to prove, and in fact you will find the stronger result easier!

[Eric Wieser]

You should be showing (V × V) ≃ₗ[ℂ] (ℂ ⊗[ℝ] V)

[Eric Wieser]

And you will almost certainly want to do so with docs#LinearEquiv.ofLinear

[Kevin Buzzard]

Eric Wieser said:

You should be showing (V × V) ≃ₗ[ℂ] (ℂ ⊗[ℝ] V)

Surely there is no $\mathbb{C}$-module structure on $V\times V$ if $V$ is a real vector space? You mean $\R$-linear?

[Kevin Buzzard]

Arien your code is full of errors for me (on master and in the lean 4 playground). Are you missing some import/open/whatever?

[Arien Malec]

It's missing something but I'm not sure what. Perhaps a variable statement
earlier on in the file I extracted this from.

[Arien Malec]

I'll try to track down what's missing and repost.

[Eric Wieser]

import Mathlib.Data.Complex.Module

[Eric Wieser]

But note that import Mathlib is fine for most "I can't work this out" mwes

[Eric Wieser]

Reducing imports is only important for "i think there is a bug" mwes

[Arien Malec]

Fixed the MWE

[Arien Malec]

It would be fun, for certain values of fun, to work out the material in https://kconrad.math.uconn.edu/blurbs/linmultialg/complexification.pdf in Mathlib...

[Eric Wieser]

I spent quite a lot of work on complexifying clifford algebras a few months ago

[Eric Wieser]

Note that in mathlib, "complexification" is usually called baseChange

[Eric Wieser]

@loogle "baseChange"

[loogle]

:search: Submodule.baseChange, Submodule.baseChange_bot, and 171 more

[Arien Malec]

Mathlib makes hard things possible, and really easy things elegant and things in the middle are sometimes....

[Arien Malec]

I've gotten to:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Complex.Module
import Mathlib.LinearAlgebra.TensorProduct


variable {V} [AddCommGroup V] [Module ℝ V]

open scoped TensorProduct

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


noncomputable def toFun: V × V →ₗ[ℝ] ℂ ⊗[ℝ] V where
  toFun p := match p with
  |  ⟨fst, snd⟩ => ((1: ℂ) ⊗ₜ[ℝ] fst) + Complex.I ⊗ₜ[ℝ] snd
  map_add' p1 p2 := by dsimp; simp [TensorProduct.tmul_add]; abel_nf
  map_smul' r p := by dsimp; simp [TensorProduct.tmul_smul]

noncomputable def invFun: ℂ ⊗[ℝ] V →ₗ[ℝ] V × V where
  toFun tp := by sorry
  map_add' tp1 tp1 := by dsimp; sorry
  map_smul' r tp := by dsimp; sorry

but the definition of invFun eludes me. In particular, if I had a complex number and a vector, I could create a Prod but I'm not sure how to get these "out" of the product, if I'm thinking about that the right way.

Also, when I do theorem toFun_invFun_comp: LinearMap.comp toFun invFun = LinearMap.id := by sorry I get

typeclass instance problem is stuck, it is often due to metavariables
  AddCommMonoid (?m.21022 × ?m.21022)

Which I assume means I need an instance for V × V

[Kevin Buzzard]

noncomputable def invFun : ℂ ⊗[ℝ] V →ₗ[ℝ] V × V := TensorProduct.lift {
  toFun := fun z ↦ {
    toFun := fun v ↦ (z.re • v, z.im • v)
    map_add' := sorry
    map_smul' := sorry
  }
  map_add' := sorry
  map_smul' := sorry
}

[Eric Wieser]

Eric Wieser said:

You probably want LinearMap.mk\_2

This would work too

[Eric Wieser]

Arien Malec said:

Also, when I do theorem toFun_invFun_comp: LinearMap.comp toFun invFun = LinearMap.id := by sorry I get

typeclass instance problem is stuck, it is often due to metavariables
  AddCommMonoid (?m.21022 × ?m.21022)

Which I assume means I need an instance for V × V

Lean is confused because you never told it you were talking about V

[Arien Malec]

Eric Wieser said:

Eric Wieser said:

You probably want LinearMap.mk\_2

This would work too

I'm sure but @Kevin Buzzard put the Don't Panic sticker on his.... (I looked at the sig for mk_2 but didn't grok it :-))

[Eric Wieser]

It takes a two-argument function, and four proofs

[Eric Wieser]

You could use by apply LinearMap.mk2 to have Lean grok it for you :)

[Arien Malec]

Eric Wieser said:

Arien Malec said:

Also, when I do theorem toFun_invFun_comp: LinearMap.comp toFun invFun = LinearMap.id := by sorry I get

typeclass instance problem is stuck, it is often due to metavariables
  AddCommMonoid (?m.21022 × ?m.21022)

...

Lean is confused because you never told it you were talking about V

Ah, theorem toFun_invFun_comp: LinearMap.comp (@toFun V _ _) invFun = LinearMap.id := by sorry fixes it.

[Eric Wieser]

Using (V) instead of {V} above would be another solution

[Kevin Buzzard]

mk\2

noncomputable def invFun: ℂ ⊗[ℝ] V →ₗ[ℝ] V × V :=
  TensorProduct.lift <| LinearMap.mk₂
  ℝ (fun z v ↦ (z.re • v, z.im • v)) _ _ _ _

[Arien Malec]

It turns out that works better -- the proofs for the plain lift version have complicated structures in them -- I'm sure there's a way around this, but this, despite the hackery, works:

noncomputable def invFun: ℂ ⊗[ℝ] V →ₗ[ℝ] V × V :=
  TensorProduct.lift <| LinearMap.mk₂
  ℝ (fun z v ↦ (z.re • v, z.im • v))
    (by intros; ext <;> dsimp <;> rw [add_smul])
    (by intros; ext <;> dsimp <;> simp [mul_smul])
    (by intros; ext <;> dsimp <;> simp [smul_add])
    (by intros; ext <;> dsimp <;> rw [smul_comm])

[Arien Malec]

Here's where I've gotten:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Complex.Module
import Mathlib.LinearAlgebra.TensorProduct


variable {V} [AddCommGroup V] [Module ℝ V]

open scoped TensorProduct

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

noncomputable def toFun: V × V →ₗ[ℝ] ℂ ⊗[ℝ] V where
  toFun p := match p with
  |  ⟨fst, snd⟩ => ((1: ℂ) ⊗ₜ[ℝ] fst) + Complex.I ⊗ₜ[ℝ] snd
  map_add' p1 p2 := by dsimp; simp [TensorProduct.tmul_add]; abel_nf
  map_smul' r p := by dsimp; simp [TensorProduct.tmul_smul]

noncomputable def invFun: ℂ ⊗[ℝ] V →ₗ[ℝ] V × V :=
  TensorProduct.lift <| LinearMap.mk₂
  ℝ (fun z v ↦ (z.re • v, z.im • v))
    (by intros; ext <;> dsimp <;> rw [add_smul])
    (by intros; ext <;> dsimp <;> simp [mul_smul])
    (by intros; ext <;> dsimp <;> simp [smul_add])
    (by intros; ext <;> dsimp <;> rw [smul_comm])


theorem toFun_invFun_comp_eq_id: LinearMap.comp (@toFun V _ _) invFun = LinearMap.id := by
  simp only [toFun, invFun]; ext z v; dsimp; simp [TensorProduct.tmul_add, TensorProduct.smul_tmul]
  sorry

theorem invFun_toFun_comp_eq_id: LinearMap.comp invFun (@toFun V _ _) = LinearMap.id := by
  simp only [invFun, toFun]; sorry

def prodRLinearComplexTensor: (V × V) ≃ₗ[ℝ] (ℂ ⊗[ℝ] V) := LinearEquiv.ofLinear toFun invFun toFun_invFun_comp_eq_id invFun_toFun_comp_eq_id

A few issues here:

1. If I make the {V} explicit I get a world of hurt with errors like: typeclass instance problem is stuck, it is often due to metavariables RingHomCompTriple ?m.31917 (RingHom.id ℝ) (RingHom.id ℝ) and friends
2. In toFun_invFun_comp_eq_id I get to a really nice goal state, but I can't get rw [←TensorProduct.add_tmul (z.re • 1) (z.im • Complex.I) v] to accept that the pattern exists; I've tried using @ and getting super explicit, but been unable to get a non barf state.

V: Type u_1
inst✝¹: AddCommGroup V
inst✝: Module ℝ V
z: ℂ
v: V
⊢ z.re • 1 ⊗ₜ[ℝ] v + z.im • Complex.I ⊗ₜ[ℝ] v = z ⊗ₜ[ℝ] v

3. The proof state for invFun_toFun_comp_eq_id by contrast is a real mess that I don't have a clue how to fix...

4. Most concerning, in prodRLinearComplexTensor I get the error:

compiler IR check failed at 'prodRLinearComplexTensor._rarg', error: unknown declaration 'toFun'

[Arien Malec]

BTW, when I clear this thicket, is it going to be easy to use the proofs to do simple things like prove:

def Rn_complexified_equiv {n: ℕ}: (ℂ ⊗[ℝ] (Fin n → ℝ)) ≃ₗ[ℝ] (Fin n → ℂ) := sorry

?

[Eric Wieser]

1 is because you need to add a bunch of Vs everywhere

[Eric Wieser]

I would guess your problem in 2 is that the operators don't have the parenthesization you think they do, and you need to start with an associativity lemma

[Eric Wieser]

4 is asking you to add noncomputable

[Eric Wieser]

Regarding R^n; you will most likely have to do all the work again from scratch, but you should find it much easier once you know the tricks

[Arien Malec]

Eric Wieser said:

I would guess your problem in 2 is that the operators don't have the parenthesization you think they do, and you need to start with an associativity lemma

I see -- the issue is that z.re • 1 ⊗ₜ[ℝ] v is seen as z.re • (1 ⊗ₜ[ℝ] v)?

[Eric Wieser]

If you hover over the goal view, vscode will tell you

[Eric Wieser]

I'm afraid while I can remember many lemmas names, I am unreliable at remembering operator precedence

[Arien Malec]

It's rfl as it happens.

theorem toFun_invFun_comp_eq_id: LinearMap.comp (@toFun V _ _) invFun = LinearMap.id := by
  simp only [toFun, invFun]; ext z v; dsimp; simp [TensorProduct.tmul_add, TensorProduct.smul_tmul]
  have h1: (z.re • (1: ℂ) ⊗ₜ[ℝ] v) = (z.re • 1) ⊗ₜ[ℝ] v := rfl
  have h2: (z.im • (Complex.I ⊗ₜ[ℝ] v)) = ((z.im • Complex.I) ⊗ₜ[ℝ] v) := rfl
  rw [h1, h2, ←TensorProduct.add_tmul (z.re • 1) (z.im • Complex.I) v]
  simp only [Complex.real_smul, mul_one, Complex.re_add_im]

[Eric Wieser]

I recommend using by rw? to find the actual lemma name

[Arien Malec]

Wow! rw? is a thing! TensorProduct.smul_tmul'

[Eric Wieser]

Just to explain why I told you to build everything as linear maps: if you hadn't, and tried to prove the inverse as f (g x) = x instead of this comp version, your ext z w wouldn't have worked

[Eric Wieser]

You might find the proof even easier if you add attribute [ext] TensorProduct.ext' before your proof

[Arien Malec]

I'm down to invFun_toFun_comp_eq_id and I can't seem to make progress -- the first part of the goal state is:

TensorProduct.lift
        (LinearMap.mk₂ ℝ --- then lots of functions to structures

and I haven't found the way around -- somehow this all normalized out in toFun_inFun_comp_eq_id.

[Eric Wieser]

Can you share the full goal state, or an updated mwe?

[Arien Malec]

Uh, scratch that, somehow:

theorem invFun_toFun_comp_eq_id: LinearMap.comp invFun (@toFun V _ _) = LinearMap.id := by
  simp only [toFun]; apply LinearMap.ext; intro p; simp [invFun]

works where

theorem invFun_toFun_comp_eq_id: LinearMap.comp invFun (@toFun V _ _) = LinearMap.id := by
  simp only [toFun, invFun]; apply LinearMap.ext; intro p

was simp resistant

[Arien Malec]

Oh, that's not correct either -- I never tried the literally simplest tactic

[Arien Malec]

Now what do I do with my time? Oh, yeah, show the R^n C^n case.

[Eric Wieser]

Arien Malec said:

Now what do I do with my time? Oh, yeah, show the R^n C^n case.

This one should actually be easier, you should be able to compose isomorphisms already in mathlib

[Arien Malec]

Hmm. With your hints on baseChange, do I want something like docs#IsBaseChange.equiv ?

[Eric Wieser]

I think I'm wrong, the result I'm thinking of only exists for finitely supported functions, not general functions

[Arien Malec]

I'll go the hard way then.

[Arien Malec]

What would need to be in Mathlib for this to be trivial?

[Eric Wieser]

docs#TensorProduct.directSumLeft for Pi types

[Eric Wieser]

(probably over a Fintype index)

[Eric Wieser]

You'd combine that with the fact that ℂ ⊗[ℝ] ℝ and ℂ are isomorphic, which Mathlib knows

[Arien Malec]

Oh, hey, we know docs#Complex.equivRealProd and now we know that (V × V) ≃ₗ[ℝ] (ℂ ⊗[ℝ] V)

[Arien Malec]

Can these be combined in useful ways?

[Eric Wieser]

Yes, you could have used that to get the isomorphism instead of your approach, I think

[Eric Wieser]

@loogle TensorProduct, Prod

[loogle]

:search: TensorProduct.SMul.aux, TensorProduct.SMul.aux_of, and 68 more

[Eric Wieser]

docs#TensorProduct.prodLeft is what I was looking for

[Arien Malec]

I played with that for a bit but didn't find the path through....

[Eric Wieser]

You'll need docs#TensorProduct.congr too

[Eric Wieser]

And docs#TensorProduct.lid

[Eric Wieser]

And docs#LinearEquiv.prod