The complex-linear part of a real-linear operator

A continuous real-linear operator Ψ : E →L[ℝ] F between complex normed spaces has a complex-linear part

Ψ.complexLinearPart z = ½ (Ψ z - i Ψ (i z)),

which is a continuous complex-linear operator (ContinuousLinearMap.complexLinearPart). Its underlying real-linear map is the algebraic complex-linear part TauCeti.complexLinearPart for the complex structures given by multiplication by i (ContinuousLinearMap.coe_complexLinearPart). Likewise the complex-antilinear part Ψ.complexAntilinearPart z = ½ (Ψ z + i Ψ (i z)) is a continuous complex-antilinear operator (ContinuousLinearMap.complexAntilinearPart), and Ψ is the sum of its two parts. A complex-linear operator is its own complex-linear part and has zero complex-antilinear part, and taking either part commutes with composition by complex-linear operators on either side. Both parts depend continuously on Ψ (ContinuousLinearMap.continuous_complexLinearPart, ContinuousLinearMap.continuous_complexAntilinearPart), so a continuous family of real-linear operators has continuous families of complex-linear and complex-antilinear parts.

For a real-linear map Ψ between complex inner product spaces preserving the standard symplectic form Im ⟪·, ·⟫, the complex-linear part P and the complex-antilinear part A satisfy ‖P z‖² = ‖z‖² + ‖A z‖² (ContinuousLinearMap.norm_sq_complexLinearPart_apply). So the complex-linear part of a linear symplectic map is injective, and for an endomorphism of a finite-dimensional space it is a complex-linear automorphism (ContinuousLinearMap.complexLinearPartEquiv), in particular of nonzero determinant (ContinuousLinearMap.det_complexLinearPart_ne_zero). This is how the graph of a linear symplectic map is moved into place by complex-linear automorphisms in TauCeti.LinearAlgebra.TotallyReal.Maslov.Symplectic.

Main declarations

• ContinuousLinearMap.complexLinearPart: the complex-linear part of a real-linear operator.
• ContinuousLinearMap.complexAntilinearPart: the complex-antilinear part of a real-linear operator, with ContinuousLinearMap.complexLinearPart_add_complexAntilinearPart_apply.
• ContinuousLinearMap.complexLinearPart_add, ContinuousLinearMap.complexLinearPart_smul, …: real-linearity in the operator.
• ContinuousLinearMap.complexLinearPart_restrictScalars: a complex-linear operator is its own complex-linear part.
• ContinuousLinearMap.complexLinearPart_restrictScalars_comp, ContinuousLinearMap.complexLinearPart_comp_restrictScalars: compatibility with composition by complex-linear operators.
• ContinuousLinearMap.restrictScalars_complexLinearPart: the underlying real-linear operator ½ (Ψ - i ∘ Ψ ∘ i).
• ContinuousLinearMap.continuous_complexLinearPart: continuity in the operator.
• ContinuousLinearMap.complexAntilinearPart_add, ContinuousLinearMap.complexAntilinearPart_smul, ContinuousLinearMap.complexAntilinearPart_restrictScalars, ContinuousLinearMap.complexAntilinearPart_restrictScalars_comp, ContinuousLinearMap.complexAntilinearPart_comp_restrictScalars, ContinuousLinearMap.continuous_complexAntilinearPart: the same API for the complex-antilinear part.
• ContinuousLinearMap.norm_sq_complexLinearPart_apply: the norm identity for a linear map preserving Im ⟪·, ·⟫.
• ContinuousLinearMap.complexLinearPartEquiv: the complex-linear part of such a map, as a complex-linear automorphism in finite dimension.
• ContinuousLinearMap.det_complexLinearPart_ne_zero: its determinant is nonzero.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Section 2.2 (the complex-linear part of a real-linear map).
• D. McDuff and D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford University Press, 2017, Section 2.2 (linear symplectic maps of ℂⁿ and their complex-linear parts).

noncomputable def ContinuousLinearMap.complexLinearPart {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) : E →L[ℂ] F

The complex-linear part z ↦ ½ (Ψ z - i Ψ (i z)) of a continuous real-linear operator between complex normed spaces, as a continuous complex-linear operator.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) (v : E) : Ψ.complexLinearPart v = 2⁻¹ • (Ψ v - Complex.I • Ψ (Complex.I • v))

The defining formula of the complex-linear part.

theorem ContinuousLinearMap.coe_complexLinearPart {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) : ⇑Ψ.complexLinearPart = ⇑(TauCeti.complexLinearPart (DistribSMul.toLinearMap ℝ E Complex.I) (DistribSMul.toLinearMap ℝ F Complex.I) ↑Ψ)

The complex-linear part is, as a function, the algebraic complex-linear part TauCeti.complexLinearPart for the complex structures given by multiplication by i.

noncomputable def ContinuousLinearMap.complexAntilinearPart {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) : E →L⋆[ℂ] F

The complex-antilinear part z ↦ ½ (Ψ z + i Ψ (i z)) of a continuous real-linear operator between complex normed spaces, as a continuous complex-antilinear operator.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) (v : E) : Ψ.complexAntilinearPart v = 2⁻¹ • (Ψ v + Complex.I • Ψ (Complex.I • v))

The defining formula of the complex-antilinear part.

theorem ContinuousLinearMap.coe_complexAntilinearPart {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) : ⇑Ψ.complexAntilinearPart = ⇑(TauCeti.complexAntilinearPart (DistribSMul.toLinearMap ℝ E Complex.I) (DistribSMul.toLinearMap ℝ F Complex.I) ↑Ψ)

The complex-antilinear part is, as a function, the algebraic complex-antilinear part TauCeti.complexAntilinearPart for the complex structures given by multiplication by i.

theorem ContinuousLinearMap.complexLinearPart_add_complexAntilinearPart_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) (v : E) : Ψ.complexLinearPart v + Ψ.complexAntilinearPart v = Ψ v

A real-linear operator is the sum of its complex-linear and complex-antilinear parts.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_restrictScalars {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : E →L[ℂ] F) : (restrictScalars ℝ f).complexLinearPart = f

A complex-linear operator is its own complex-linear part.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_restrictScalars_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] (f : F →L[ℂ] G) (Ψ : E →L[ℝ] F) : (restrictScalars ℝ f ∘SL Ψ).complexLinearPart = f ∘SL Ψ.complexLinearPart

Postcomposing with a complex-linear operator commutes with taking complex-linear parts.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_comp_restrictScalars {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] (Ψ : F →L[ℝ] G) (f : E →L[ℂ] F) : (Ψ ∘SL restrictScalars ℝ f).complexLinearPart = Ψ.complexLinearPart ∘SL f

Precomposing with a complex-linear operator commutes with taking complex-linear parts.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] : complexLinearPart 0 = 0

The complex-linear part of 0 is 0.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ Φ : E →L[ℝ] F) : (Ψ + Φ).complexLinearPart = Ψ.complexLinearPart + Φ.complexLinearPart

The complex-linear part is additive.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_neg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) : (-Ψ).complexLinearPart = -Ψ.complexLinearPart

The complex-linear part commutes with negation.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ Φ : E →L[ℝ] F) : (Ψ - Φ).complexLinearPart = Ψ.complexLinearPart - Φ.complexLinearPart

The complex-linear part commutes with subtraction.

@[simp]

theorem ContinuousLinearMap.complexLinearPart_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (c : ℝ) (Ψ : E →L[ℝ] F) : (c • Ψ).complexLinearPart = c • Ψ.complexLinearPart

The complex-linear part commutes with real scalar multiplication.

theorem ContinuousLinearMap.restrictScalars_complexLinearPart {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) : restrictScalars ℝ Ψ.complexLinearPart = 2⁻¹ • (Ψ - ↑(Complex.smulIEquiv F) ∘SL Ψ ∘SL ↑(Complex.smulIEquiv E))

The real-linear operator underlying the complex-linear part is ½ (Ψ - i ∘ Ψ ∘ i).

theorem ContinuousLinearMap.continuous_complexLinearPart {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] : Continuous complexLinearPart

The complex-linear part depends continuously on the operator.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] : complexAntilinearPart 0 = 0

The complex-antilinear part of 0 is 0.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ Φ : E →L[ℝ] F) : (Ψ + Φ).complexAntilinearPart = Ψ.complexAntilinearPart + Φ.complexAntilinearPart

The complex-antilinear part is additive.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_neg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ : E →L[ℝ] F) : (-Ψ).complexAntilinearPart = -Ψ.complexAntilinearPart

The complex-antilinear part commutes with negation.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (Ψ Φ : E →L[ℝ] F) : (Ψ - Φ).complexAntilinearPart = Ψ.complexAntilinearPart - Φ.complexAntilinearPart

The complex-antilinear part commutes with subtraction.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (c : ℝ) (Ψ : E →L[ℝ] F) : (c • Ψ).complexAntilinearPart = c • Ψ.complexAntilinearPart

The complex-antilinear part commutes with real scalar multiplication.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_restrictScalars {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : E →L[ℂ] F) : (restrictScalars ℝ f).complexAntilinearPart = 0

A complex-linear operator has zero complex-antilinear part.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_restrictScalars_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] (f : F →L[ℂ] G) (Ψ : E →L[ℝ] F) : (restrictScalars ℝ f ∘SL Ψ).complexAntilinearPart = f ∘SL Ψ.complexAntilinearPart

Postcomposing with a complex-linear operator commutes with taking complex-antilinear parts.

@[simp]

theorem ContinuousLinearMap.complexAntilinearPart_comp_restrictScalars {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] (Ψ : F →L[ℝ] G) (f : E →L[ℂ] F) : (Ψ ∘SL restrictScalars ℝ f).complexAntilinearPart = Ψ.complexAntilinearPart ∘SL f

Precomposing with a complex-linear operator commutes with taking complex-antilinear parts.

theorem ContinuousLinearMap.continuous_complexAntilinearPart {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] : Continuous complexAntilinearPart

The complex-antilinear part depends continuously on the operator.

The complex-linear part of a linear symplectic map

theorem ContinuousLinearMap.norm_sq_complexLinearPart_apply {V : Type u_4} {W : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [NormedAddCommGroup W] [InnerProductSpace ℂ W] {Ψ : V →L[ℝ] W} (hΨ : ∀ (x y : V), (inner ℂ (Ψ x) (Ψ y)).im = (inner ℂ x y).im) (z : V) : ‖Ψ.complexLinearPart z‖ ^ 2 = ‖z‖ ^ 2 + ‖Ψ.complexAntilinearPart z‖ ^ 2

For a real-linear map Ψ preserving the symplectic form Im ⟪·, ·⟫, the complex-linear part P and the complex-antilinear part A satisfy ‖P z‖² = ‖z‖² + ‖A z‖².

theorem ContinuousLinearMap.complexLinearPart_injective {V : Type u_4} {W : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [NormedAddCommGroup W] [InnerProductSpace ℂ W] {Ψ : V →L[ℝ] W} (hΨ : ∀ (x y : V), (inner ℂ (Ψ x) (Ψ y)).im = (inner ℂ x y).im) : Function.Injective ⇑Ψ.complexLinearPart

The complex-linear part of a real-linear map preserving Im ⟪·, ·⟫ is injective.

noncomputable def ContinuousLinearMap.complexLinearPartEquiv {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (Ψ : V →L[ℝ] V) (hΨ : ∀ (x y : V), (inner ℂ (Ψ x) (Ψ y)).im = (inner ℂ x y).im) : V ≃L[ℂ] V

The complex-linear part of a real-linear map preserving Im ⟪·, ·⟫, as a complex-linear automorphism.

@[simp]

theorem ContinuousLinearMap.coe_complexLinearPartEquiv {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (Ψ : V →L[ℝ] V) (hΨ : ∀ (x y : V), (inner ℂ (Ψ x) (Ψ y)).im = (inner ℂ x y).im) : ↑(Ψ.complexLinearPartEquiv hΨ) = Ψ.complexLinearPart

The automorphism ContinuousLinearMap.complexLinearPartEquiv is the complex-linear part.

@[simp]

theorem ContinuousLinearMap.coe_toLinearEquiv_complexLinearPartEquiv {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (Ψ : V →L[ℝ] V) (hΨ : ∀ (x y : V), (inner ℂ (Ψ x) (Ψ y)).im = (inner ℂ x y).im) : ↑↑(Ψ.complexLinearPartEquiv hΨ) = ↑Ψ.complexLinearPart

The linear automorphism underlying ContinuousLinearMap.complexLinearPartEquiv is the complex-linear part.

theorem ContinuousLinearMap.det_complexLinearPart_ne_zero {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] {Ψ : V →L[ℝ] V} (hΨ : ∀ (x y : V), (inner ℂ (Ψ x) (Ψ y)).im = (inner ℂ x y).im) : LinearMap.det ↑Ψ.complexLinearPart ≠ 0

The complex-linear part of a real-linear endomorphism preserving Im ⟪·, ·⟫ has nonzero determinant.

@[simp]

theorem ContinuousLinearMap.complexLinearPartEquiv_apply {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (Ψ : V →L[ℝ] V) (hΨ : ∀ (x y : V), (inner ℂ (Ψ x) (Ψ y)).im = (inner ℂ x y).im) (z : V) : (Ψ.complexLinearPartEquiv hΨ) z = Ψ.complexLinearPart z

The automorphism ContinuousLinearMap.complexLinearPartEquiv acts as the complex-linear part.