free_kaehlerDifferential — Mathlib

English

If IsStandardSmoothOfRelativeDimension 0 holds, then Ω[S/R] is a Subsingleton (zero) module.

Русский

Если относительная размерность ноль, касательность Ω[S/R] тривиальна как модуль.

LaTeX

$$Subsingleton Ω[S⁄R] (under given hypotheses)$$

Lean4

/-- If `P` is a submersive presentation of `S` as an `R`-algebra, `Ω[S⁄R]` is free. -/
@[stacks 00T7 "(2)"]
theorem free_kaehlerDifferential (P : SubmersivePresentation R S ι σ) : Module.Free S Ω[S⁄R] :=
  Module.Free.of_basis P.basisKaehler

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