repr_CotangentSpaceMap — Mathlib

English

As in 175691, another formulation of the representation of mapped basis elements under CotangentSpace.map.

Русский

Как и в 175691, другая формулировка представления элементов базиса после отображения в CotangentSpace.map.

LaTeX

$$$\\text{repr}_{P',i}(\\text{CotangentSpace.map } f^{toExt}(P.cotangentSpaceBasis i)) = \\text{aeval}(P'.val)(pderiv i)(f(i))$$$

Lean4

@[simp]
theorem repr_CotangentSpaceMap (f : Hom P P') (i j) :
    P'.cotangentSpaceBasis.repr (CotangentSpace.map f.toExtensionHom (P.cotangentSpaceBasis i)) j =
      aeval P'.val (pderiv j (f.val i)) :=
  by
  rw [cotangentSpaceBasis_apply]
  simp only [toExtension]
  rw [CotangentSpace.map_tmul, map_one]
  erw [cotangentSpaceBasis_repr_one_tmul, Hom.toAlgHom_X]

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