kahler_map_complex — Mathlib

English

The Kahler form under the complex-number representation is ω_K(x,y) = f(y) · overline{f(x)} for a linear isometry f: E → ℂ compatible with the orientation.

Русский

Кайлерова форма в комплексной записи: ω_K(x,y) = f(y) \overline{f(x)}.

LaTeX

$$$ \\omega_{\\text{kahler}}(x,y) = f(y) \\overline{f(x)} $$$

Lean4

/-- The Kahler form on an oriented real inner product space of dimension 2 can be evaluated in terms
of a complex-number representation of the space. -/
theorem kahler_map_complex (f : E ≃ₗᵢ[ℝ] ℂ) (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation)
    (x y : E) : o.kahler x y = f y * conj (f x) :=
  by
  rw [← Complex.kahler, ← hf, kahler_map]
  iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]

Похожие утверждения