English
There is a canonical equivalence between H1Cotangent modules for algebra extensions, compatible with extension structure and base rings, enabling consistent computation of H1Cotangent across different presentations of the same algebra.
Русский
Существуют канонические эквивалентности между модулями H1Cotangent для алгебраических расширений, совместимые со структурой расширения и базовыми колами, что обеспечивает согласованные вычисления H1Cotangent в различных презентациях одной и той же алгебры.
LaTeX
$$P.H1Cotangent ≃_S Q.H1Cotangent for extensions P→S, Q→S$$
Lean4
/-- Any formally smooth extension can be used to calculate `H¹(L_{S/R})`. -/
noncomputable def equivH1CotangentOfFormallySmooth (P : Extension R S) [FormallySmooth R P.Ring] :
P.H1Cotangent ≃ₗ[S] H1Cotangent R S :=
have : FormallySmooth R (Generators.self R S).toExtension.Ring :=
inferInstanceAs (FormallySmooth R (MvPolynomial _ _))
H1Cotangent.equivOfFormallySmooth _ _
