free_cotangent

Mathlib.RingTheory.Smooth.StandardSmoothCotangent

URI: https://scilib.ai/kg/mathlib#Algebra.SubmersivePresentation.free_cotangent

English

If P is a submersive presentation of S over R, then the kaehler differential Ω[S/R] is a free S-module.

Русский

Если P — субмёрсивное представление S над R, то дифференциал Каэля Ω[S/R] свободен как S-модуль.

LaTeX

$$Module.Free S Ω[S⁄R]$$

Lean4

@[stacks 00T7 "(3)"]
instance free_cotangent : Module.Free S P.toExtension.Cotangent :=
  Module.Free.of_basis P.basisCotangent

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru