Multiplication by i on complex modules

Multiplication by i is a real continuous linear automorphism of any complex module with a compatible real scalar action (IsScalarTower ℝ ℂ X) and continuous multiplication by constant scalars, with inverse multiplication by -i. It is the conjugating operator by which complex linearity of a real-linear map is tested: a continuous real-linear map between complex modules that commutes with it is continuous complex-linear.

Main definitions and results

• Complex.smulIEquiv: multiplication by i as a real continuous linear equivalence, with smulIEquiv_apply and smulIEquiv_symm_apply.
• ContinuousLinearMap.complexOfMapISmul: a continuous real-linear map between complex modules that commutes with multiplication by i, as a continuous complex-linear map.

noncomputable def Complex.smulIEquiv (X : Type u_1) [AddCommGroup X] [TopologicalSpace X] [Module ℝ X] [Module ℂ X] [IsScalarTower ℝ ℂ X] [ContinuousConstSMul ℂ X] : X ≃L[ℝ] X

Multiplication by i as a real continuous linear equivalence of a complex module with a compatible real scalar action and continuous multiplication by constant scalars.

@[simp]

theorem Complex.smulIEquiv_apply {X : Type u_1} [AddCommGroup X] [TopologicalSpace X] [Module ℝ X] [Module ℂ X] [IsScalarTower ℝ ℂ X] [ContinuousConstSMul ℂ X] (x : X) : (smulIEquiv X) x = I • x

@[simp]

theorem Complex.smulIEquiv_symm_apply {X : Type u_1} [AddCommGroup X] [TopologicalSpace X] [Module ℝ X] [Module ℂ X] [IsScalarTower ℝ ℂ X] [ContinuousConstSMul ℂ X] (x : X) : (smulIEquiv X).symm x = -I • x

def ContinuousLinearMap.complexOfMapISmul {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] [AddCommGroup W] [Module ℝ W] [Module ℂ W] [IsScalarTower ℝ ℂ W] [TopologicalSpace V] [TopologicalSpace W] (u : V →L[ℝ] W) (h : ∀ (v : V), u (Complex.I • v) = Complex.I • u v) : V →L[ℂ] W

A continuous real-linear map between complex modules that commutes with multiplication by I, as a continuous complex-linear map.

@[simp]

theorem ContinuousLinearMap.coe_complexOfMapISmul {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] [AddCommGroup W] [Module ℝ W] [Module ℂ W] [IsScalarTower ℝ ℂ W] [TopologicalSpace V] [TopologicalSpace W] (u : V →L[ℝ] W) (h : ∀ (v : V), u (Complex.I • v) = Complex.I • u v) : ⇑(u.complexOfMapISmul h) = ⇑u

@[simp]

theorem ContinuousLinearMap.restrictScalars_complexOfMapISmul {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] [AddCommGroup W] [Module ℝ W] [Module ℂ W] [IsScalarTower ℝ ℂ W] [TopologicalSpace V] [TopologicalSpace W] (u : V →L[ℝ] W) (h : ∀ (v : V), u (Complex.I • v) = Complex.I • u v) : restrictScalars ℝ (u.complexOfMapISmul h) = u