cotangentSpaceBasis_apply — Mathlib

English

For f: P → P', the representation of P'.cotangentSpaceBasis.repr mapped through CotangentSpace.map equals the aeval of the pderiv on the image of i.

Русский

Для f: P → P' представление P'.cotangentSpaceBasis через map совпадает с eval(pderiv) на образ i.

LaTeX

$$$P'.cotangentSpaceBasis.repr (CotangentSpace.map f.toExtensionHom (P.cotangentSpaceBasis i)) _ = aeval P'.val (pderiv _ (f.val i))$$$

Lean4

theorem cotangentSpaceBasis_apply (i) : P.cotangentSpaceBasis i = ((1 : S) ⊗ₜ[P.Ring] D R P.Ring (.X i) :) := by
  simp [cotangentSpaceBasis, toExtension]

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