Physlib

Physlib.Mathematics.ForMathlib.ComplexLinear

Upgrading a real-linear map to a complex-linear one

i. Overview

An `ℝ`-linear map between complex vector spaces that commutes with multiplication by `i` is `ℂ`-linear, since `c = c.re + c.im · i`. Mathlib has the case of a map out of `ℂ` (`real_linearMap_map_smul_complex`, `ContinuousLinearMap.complexOfReal`); this file treats an arbitrary domain.

ii. Key results

  • `LinearMap.map_smul_of_commutesI` : the law along one direction.
  • `LinearMap.commutesI_of_basis` : commuting with `i` on a `ℂ`-basis suffices.
  • `ContinuousLinearMap.complexOfCommutesI` : the resulting continuous `ℂ`-linear map.

iii. Table of contents

  • A. The scalar law
  • B. Commuting with `i` on a basis
  • C. The complex-linear map

iv. References

There are no known references for the material in this module.

A. The scalar law

B. Commuting with `i` on a basis

C. The complex-linear map

4 declarations

theorem

L(iv)=iL(v)  ⟹  L(cv)=cL(v)L(iv) = iL(v) \implies L(cv) = cL(v) for R\mathbb{R}-linear maps

Let VV and EE be complex vector spaces, and let L:V→EL: V \to E be an R\mathbb{R}-linear map. If for a specific vector v∈Vv \in V, the map LL commutes with the action of the imaginary unit ii (i.e., L(i⋅v)=i⋅L(v)L(i \cdot v) = i \cdot L(v)), then for any complex scalar c∈Cc \in \mathbb{C}, LL also commutes with the action of cc on that vector: L(c⋅v)=c⋅L(v)L(c \cdot v) = c \cdot L(v).

theorem

Commutation of an R\mathbb{R}-linear map with ii on a C\mathbb{C}-basis implies global commutation with ii

Let VV and EE be complex vector spaces and let L:V→EL : V \to E be an R\mathbb{R}-linear map. Suppose {bi}i∈ι\{b_i\}_{i \in \iota} is a finite C\mathbb{C}-basis of VV. If L(i⋅bi)=i⋅L(bi)L(i \cdot b_i) = i \cdot L(b_i) for all i∈ιi \in \iota, where ii is the imaginary unit, then L(i⋅v)=i⋅L(v)L(i \cdot v) = i \cdot L(v) for every v∈Vv \in V.

definition

Continuous C\mathbb{C}-linear map from an R\mathbb{R}-linear map commuting with ii

Given a continuous R\mathbb{R}-linear map L:V→EL: V \to E between complex vector spaces and a proof hh that LL commutes with the imaginary unit ii (i.e., L(i⋅v)=i⋅L(v)L(i \cdot v) = i \cdot L(v) for all v∈Vv \in V), this definition constructs the corresponding continuous C\mathbb{C}-linear map from VV to EE.

theorem

The induced continuous C\mathbb{C}-linear map LCL_{\mathbb{C}} satisfies LC(v)=L(v)L_{\mathbb{C}}(v) = L(v)

Let VV and EE be complex vector spaces, and let L:V→EL: V \to E be a continuous R\mathbb{R}-linear map. Suppose LL commutes with the imaginary unit ii, such that L(i⋅v)=i⋅L(v)L(i \cdot v) = i \cdot L(v) for all v∈Vv \in V. If LCL_{\mathbb{C}} is the continuous C\mathbb{C}-linear map constructed from LL using this commutation property, then for any vector v∈Vv \in V, it holds that LC(v)=L(v)L_{\mathbb{C}}(v) = L(v).