English
The unit circle in the complex plane is a Lie group with analytic multiplication and inversion.
Русский
Единичная окружность на плоскости комплексных чисел образует аналитику Ли-группу, с аналитическими операциями умножения и взятия обратного.
LaTeX
$$The unit circle $\mathbb{S}^1 \subset \mathbb{C}$ is a Lie group; the multiplication and inversion maps are analytic.$$
Lean4
/-- The unit circle in `ℂ` is an analytic Lie group. -/
instance : LieGroup (𝓡 1) ω Circle
where
contMDiff_mul := by
apply ContMDiff.codRestrict_sphere
let c : Circle → ℂ := (↑)
have h₂ : ContMDiff (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) ω fun z : ℂ × ℂ => z.fst * z.snd :=
by
rw [contMDiff_iff]
exact ⟨continuous_mul, fun x y => contDiff_mul.contDiffOn⟩
suffices h₁ : ContMDiff _ _ _ (Prod.map c c) from h₂.comp h₁
apply ContMDiff.prodMap <;> exact contMDiff_coe_sphere
contMDiff_inv := by
apply ContMDiff.codRestrict_sphere
simp only [← Circle.coe_inv, Circle.coe_inv_eq_conj]
exact Complex.conjCLE.contDiff.contMDiff.comp contMDiff_coe_sphere
