English
Given a submersive presentation P, the basis of Kaehler differentials can be described via the split exact sequence using the cotangent basis and the cotangent equivalence.
Русский
Для субмёрсивного представления P база касательных дифференциалов определяется через разломную точную последовательность, используя базис касательной и эквивалентность касательных.
LaTeX
$$basisKaehler : Basis ((Set.range P.map)ᶜ : Set _) S Ω[S⁄R]$$
Lean4
/-- If `P` is a submersive presentation of `S` as an `R`-algebra and `S` is nontrivial,
`Ω[S⁄R]` is free of rank the dimension of `P`, i.e. the number of generators minus the number
of relations. -/
theorem rank_kaehlerDifferential [Nontrivial S] [Finite ι] (P : SubmersivePresentation R S ι σ) :
Module.rank S Ω[S⁄R] = P.dimension := by
simp only [rank_eq_card_basis P.basisKaehler, Fintype.card_compl_set, Presentation.dimension,
Nat.card_eq_fintype_card, Set.card_range_of_injective P.map_inj]
