rank_kaehlerDifferential — Mathlib

English

If S is nontrivial and R-standard smooth of relative dimension, Ω[S/R] is a free S-module of rank equal to the relative dimension.

Русский

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

LaTeX

$$rank_kaehlerDifferential (n) : Module.rank S Ω[S⁄R] = n$$

Lean4

/-- If `S` is non-trivial and `R`-standard smooth of relative dimension, `Ω[S⁄R]` is a free
`S`-module of rank `n`. -/
theorem rank_kaehlerDifferential [Nontrivial S] (n : ℕ) [IsStandardSmoothOfRelativeDimension n R S] :
    Module.rank S Ω[S⁄R] = n :=
  by
  obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
  rw [P.rank_kaehlerDifferential, hP]

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