toKaehler_cotangentSpaceBasis — Mathlib

English

The map from Kaehler differentials to cotangent space sends the basis element to the Kaehler differential D applied to the corresponding generator.

Русский

Отображение KaehlerDifferential на котангенциальное пространство отправляет базисный элемент в D соответствующего генератора.

LaTeX

$$$P \\toExtension.toKaehler\\bigl(P.cotangentSpaceBasis i\\bigr) = D R S (P.val i)$$$

Lean4

@[simp]
theorem toKaehler_cotangentSpaceBasis (i) : P.toExtension.toKaehler (P.cotangentSpaceBasis i) = D R S (P.val i) :=
  by
  rw [cotangentSpaceBasis_apply]
  exact (KaehlerDifferential.mapBaseChange_tmul ..).trans (by simp)

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