Conformal maps between complex vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

is_conformal_map_complex_linear: a nonzero complex linear map into an arbitrary complex normed space is conformal.
is_conformal_map_complex_linear_conj: the composition of a nonzero complex linear map with conj is complex linear.
is_conformal_map_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.

source

theorem is_conformal_map_conj :

is_conformal_map ↑complex.conj_lie

source

theorem is_conformal_map_complex_linear {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [normed_space ℂ E] {map : ℂ →L[ℂ ] E} (nonzero : map ≠ 0) :

is_conformal_map (continuous_linear_map.restrict_scalars ℝ map)

source

theorem is_conformal_map_complex_linear_conj {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [normed_space ℂ E] {map : ℂ →L[ℂ ] E} (nonzero : map ≠ 0) :

is_conformal_map ((continuous_linear_map.restrict_scalars ℝ map).comp ↑complex.conj_cle)

source

theorem is_conformal_map.is_complex_or_conj_linear {g : ℂ →L[ℝ ] ℂ} (h : is_conformal_map g) :

(∃ (map : ℂ →L[ℂ ] ℂ), continuous_linear_map.restrict_scalars ℝ map = g) ∨ ∃ (map : ℂ →L[ℂ ] ℂ), continuous_linear_map.restrict_scalars ℝ map = g.comp ↑complex.conj_cle

source

theorem is_conformal_map_iff_is_complex_or_conj_linear {g : ℂ →L[ℝ ] ℂ} :

is_conformal_map g ↔ ((∃ (map : ℂ →L[ℂ ] ℂ), continuous_linear_map.restrict_scalars ℝ map = g) ∨ ∃ (map : ℂ →L[ℂ ] ℂ), continuous_linear_map.restrict_scalars ℝ map = g.comp ↑complex.conj_cle) ∧ 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.