Conformal maps between complex vector spaces

We prove the sufficient and necessary conditions for a real-linear map between complex vector spaces to be conformal.

Main results

• isConformalMap_complex_linear: a nonzero complex linear map into an arbitrary complex normed space is conformal.
• isConformalMap_complex_linear_conj: the composition of a nonzero complex linear map with conj is complex linear.
• isConformalMap_iff_is_complex_or_conj_linear: a real linear map between the complex plane is conformal iff it's complex linear or the composition of some complex linear map and conj.

Warning

Antiholomorphic functions such as the complex conjugate are considered as conformal functions in this file.

theorem isConformalMap_conj : IsConformalMap ↑{ toLinearEquiv := Complex.conjLIE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem isConformalMap_complex_linear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) : IsConformalMap (ContinuousLinearMap.restrictScalars ℝ map)

theorem isConformalMap_complex_linear_conj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) : IsConformalMap ((ContinuousLinearMap.restrictScalars ℝ map).comp ↑Complex.conjCLE)

theorem IsConformalMap.is_complex_or_conj_linear {g : ℂ →L[ℝ] ℂ} (h : IsConformalMap g) : (∃ (map : ℂ →L[ℂ] ℂ), ContinuousLinearMap.restrictScalars ℝ map = g) ∨ ∃ (map : ℂ →L[ℂ] ℂ), ContinuousLinearMap.restrictScalars ℝ map = g.comp ↑Complex.conjCLE

theorem isConformalMap_iff_is_complex_or_conj_linear {g : ℂ →L[ℝ] ℂ} : IsConformalMap g ↔ ((∃ (map : ℂ →L[ℂ] ℂ), ContinuousLinearMap.restrictScalars ℝ map = g) ∨ ∃ (map : ℂ →L[ℂ] ℂ), ContinuousLinearMap.restrictScalars ℝ map = g.comp ↑Complex.conjCLE) ∧ g ≠ 0

A real continuous linear map on the complex plane is conformal if and only if the map or its conjugate is complex linear, and the map is nonvanishing.