toKaehler — Mathlib

English

The projection from the cotangent extension to the module of differentials is surjective, i.e., every differential appears from the cotangent construction after base change.

Русский

Проекция из котантного пространства на модуль различий сюръективна, то есть каждый дифференциал возникает из котантного конструктора после базового изменения.

LaTeX

$$$\\mathrm{toKaehler} : P.CotangentSpace \\twoheadrightarrow Ω[S⁄R]$ is surjective$$

Lean4

/-- The projection map from the relative cotangent space to the module of differentials. -/
noncomputable abbrev toKaehler : P.CotangentSpace →ₗ[S] Ω[S⁄R] :=
  mapBaseChange _ _ _

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