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.

• DifferentiableAt.conformalAt states that a real-differentiable function with a nonvanishing differential from the complex plane into an arbitrary complex-normed space is conformal at a point if it's holomorphic at that point. This is a version of Cauchy-Riemann equations.

• conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj proves that a real-differential function with a nonvanishing differential between the complex plane is conformal at a point if and only if it's holomorphic or antiholomorphic at that point.

Warning

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

TODO

• The classical form of Cauchy-Riemann equations
• On a connected open set u, a function which is ConformalAt each point is either holomorphic throughout or antiholomorphic throughout.

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.

Conformality of real-differentiable complex maps

theorem DifferentiableAt.conformalAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z : ℂ} {f : ℂ → E} (h : DifferentiableAt ℂ f z) (hf' : deriv f z ≠ 0) : ConformalAt f z

A real differentiable function of the complex plane into some complex normed space E is conformal at a point z if it is holomorphic at that point with a nonvanishing differential. This is a version of the Cauchy-Riemann equations.

theorem conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj {f : ℂ → ℂ} {z : ℂ} : ConformalAt f z ↔ (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0

A complex function is conformal if and only if the function is holomorphic or antiholomorphic with a nonvanishing differential.