English
The relative dimension of a standard smooth R-algebra S is the dimension of an arbitrarily chosen submersive presentation of S.
Русский
Относительная размерность стандартной гладкой R-алгебры S равна размерности произвольного подмодульного представления S.
LaTeX
$$$\mathrm{relativeDimension}(R,S) = \dim P$ for a submersive presentation P of S over R$$
Lean4
/-- The relative dimension of a standard smooth `R`-algebra `S` is
the dimension of an arbitrarily chosen submersive `R`-presentation of `S`.
Note: If `S` is non-trivial, this number is independent of the choice of the presentation as it is
equal to the `S`-rank of `Ω[S/R]`
(see `IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential`).
-/
noncomputable def relativeDimension [IsStandardSmooth R S] : ℕ :=
letI := ‹IsStandardSmooth R S›.out.choose_spec.choose_spec.choose
‹IsStandardSmooth R S›.out.choose_spec.choose_spec.choose_spec.2.some.dimension
