kahler_map — Mathlib

English

Let φ be a linear isometry between 2D oriented spaces. Then kahler is preserved under pullback by φ: kahler map equality holds.

Русский

Пусть φ — линейная изометрия между ориентированными пространствами размерности 2. Тогда kahler сохраняется при вытягивании по φ.

LaTeX

$$ (Orientation.map (Fin 2) φ.toLinearEquiv o).kahler x y = o.kahler (φ^{-1} x) (φ^{-1} y) $$

Lean4

theorem kahler_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (finrank ℝ F = 2)]
    (φ : E ≃ₗᵢ[ℝ] F) (x y : F) :
    (Orientation.map (Fin 2) φ.toLinearEquiv o).kahler x y = o.kahler (φ.symm x) (φ.symm y) := by
  simp [kahler_apply_apply, areaForm_map]

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