English
Every real continuous linear map on the plane that is conformal is either the restriction of a complex‑linear map or the restriction of a map composed with conjugation.
Русский
Каждое конформное веще‑линейное отображение плоскости либо является ограничением комплексно‑линейной карты, либо ограничением карты, композиции с сопряжением.
LaTeX
$$IsConformalMap g \Rightarrow ((\exists map, map.restrictScalars(\mathbb{R}) = g) \lor (\exists map, map.restrictScalars(\mathbb{R}) = g \circ conjCLE))$$
Lean4
theorem is_complex_or_conj_linear (h : IsConformalMap g) :
(∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g) ∨ ∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g ∘L ↑conjCLE :=
by
rcases h with ⟨c, -, li, rfl⟩
obtain ⟨li, rfl⟩ : ∃ li' : ℂ ≃ₗᵢ[ℝ] ℂ, li'.toLinearIsometry = li := ⟨li.toLinearIsometryEquiv rfl, by ext1; rfl⟩
rcases linear_isometry_complex li with
⟨a, rfl | rfl⟩
-- let rot := c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ,
· refine Or.inl ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩
ext1
simp
· refine Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩
ext1
simp
