English
There is a natural equivalence between H1Cotangent modules along an extension P → S, giving a canonical transport of H1Cotangent along extensions and enabling comparison across different base rings.
Русский
Существует естественное эквивалентное отображение между H1Cotangent вдоль расширения P → S, обеспечивающее канонический перенос H1Cotangent через расширения и сравнение между разными базами.
LaTeX
$$P.H1Cotangent ≃_S H1Cotangent R S$$
Lean4
/-- Formally smooth extensions have isomorphic `H¹(L_P)`. -/
noncomputable def equivOfFormallySmooth (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] :
P₁.H1Cotangent ≃ₗ[S] P₂.H1Cotangent :=
.ofBijective _ (H1Cotangent.map_toInfinitesimal_bijective P₁) ≪≫ₗ
H1Cotangent.equiv (Extension.homInfinitesimal _ _) (Extension.homInfinitesimal _ _) ≪≫ₗ
.symm (.ofBijective _ (H1Cotangent.map_toInfinitesimal_bijective P₂))
