D_tensorProductTo — Mathlib

English

The Kaehler differential tensorProductTo on the ideal D coincides with the cotangent map to the ideal, i.e., applying the tensorProductTo map yields the cotangent map.

Русский

Дифференциал Хана под действием тензорного произведения совпадает с касательной картой к идеалу.

LaTeX

$$$(\\mathrm{KaehlerDifferential}.D\\, R\\, S).tensorProductTo(x) = (\\mathrm{KaehlerDifferential}.ideal(R,S)).toCotangent(x)$$$

Lean4

theorem D_tensorProductTo (x : KaehlerDifferential.ideal R S) :
    (KaehlerDifferential.D R S).tensorProductTo x = (KaehlerDifferential.ideal R S).toCotangent x :=
  by
  rw [← Derivation.liftKaehlerDifferential_apply, Derivation.liftKaehlerDifferential_D]
  rfl

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