English
A real continuous linear map g is conformal if and only if it is the restriction of a complex‑linear map or the restriction of a map composed with conjugation, and g ≠ 0.
Русский
Реальная непрерывная линейная карта g конформна тогда и только тогда, когда она является ограничением комплексно‑линейной карты или ограничением карты, композиции с сопряжением, и g ≠ 0.
LaTeX
$$$ IsConformalMap g \iff \\bigl((\exists map, map.restrictScalars \mathbb{R} = g) \lor (\exists map, map.restrictScalars \mathbb{R} = g \circ conjCLE)\bigr) \land g \neq 0$$$
Lean4
/-- 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. -/
theorem isConformalMap_iff_is_complex_or_conj_linear :
IsConformalMap g ↔
((∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g) ∨ ∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g ∘L ↑conjCLE) ∧
g ≠ 0 :=
by
constructor
· exact fun h => ⟨h.is_complex_or_conj_linear, h.ne_zero⟩
· rintro ⟨⟨map, rfl⟩ | ⟨map, hmap⟩, h₂⟩
· refine isConformalMap_complex_linear ?_
contrapose! h₂ with w
simp only [w, restrictScalars_zero]
· have minor₁ : g = map.restrictScalars ℝ ∘L ↑conjCLE :=
by
ext1
simp only [hmap, coe_comp', ContinuousLinearEquiv.coe_coe, Function.comp_apply, conjCLE_apply,
starRingEnd_self_apply]
rw [minor₁] at h₂ ⊢
refine isConformalMap_complex_linear_conj ?_
contrapose! h₂ with w
simp only [w, restrictScalars_zero, zero_comp]
