English
The kahler map on E is a complex-valued bilinear form whose real part is the inner product and whose imaginary part is the area form.
Русский
Кähler-карта на E — это комплексно-значимая билинейная форма, чья вещественная часть есть скалярное произведение, а мнимая часть — форма площади.
LaTeX
$$kahler : E \\to E \\to \\mathbb{C} \\\\ kahler(x,y) = ⟪x,y⟫ + ω(x,y) i$$
Lean4
/-- A complex-valued real-bilinear map on an oriented real inner product space of dimension 2. Its
real part is the inner product and its imaginary part is `Orientation.areaForm`.
On `ℂ` with the standard orientation, `kahler w z = conj w * z`; see `Complex.kahler`. -/
def kahler : E →ₗ[ℝ] E →ₗ[ℝ] ℂ :=
LinearMap.llcomp ℝ E ℝ ℂ Complex.ofRealCLM ∘ₗ innerₛₗ ℝ +
LinearMap.llcomp ℝ E ℝ ℂ ((LinearMap.lsmul ℝ ℂ).flip Complex.I) ∘ₗ ω
