instSubsingletonH1CotangentOfFormallySmooth

English

If S is formally smooth over R, then the H1Cotangent module is a subsingleton; this is deduced from the main equivalence between injectivity of kerCotangentToTensor and projectivity of Ω[S/R].

Русский

Если S формально гладкая над R, то H1Cotangent является подмножество из одного элемента; это вытекает из эквивалентности инъективности kerCotangentToTensor и проективности Ω[S/R].

LaTeX

$$Subsingleton (Algebra.H1Cotangent R S)$$

Lean4

instance [Algebra.FormallySmooth R S] : Subsingleton (Algebra.H1Cotangent R S) :=
  (Algebra.FormallySmooth.iff_subsingleton_and_projective.mp ‹_›).1

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