basisKaehler — Mathlib

English

If S is R-standard smooth of relative dimension n, the rank of Ω[S/R] equals n.

Русский

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

LaTeX

$$Module.rank S Ω[S⁄R] = n$$

Lean4

/-- Given a submersive presentation of `S` as `R`-algebra, the images of `dxᵢ`
for `i` in the complement of `σ` in `ι` form a basis of `Ω[S⁄R]`. -/
@[stacks 00T7 "(2)"]
noncomputable def basisKaehler : Basis ((Set.range P.map)ᶜ : Set _) S Ω[S⁄R] :=
  P.basisKaehlerOfIsCompl Subtype.val_injective <|
    by
    rw [Subtype.range_coe_subtype]
    exact IsCompl.symm isCompl_compl

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