English
For any algebra extension P over S in the formal smooth setting, the map from P.H1Cotangent to S.H1Cotangent induced by the extension is bijective; i.e., H1Cotangent is invariant under formally smooth extensions.
Русский
Для любой формально гладкой секции P над S отображение между P.H1Cotangent и S.H1Cotangent, индуцированное расширением, биективно; то есть H1Cotangent инвариантна относительно формально гладких расширений.
LaTeX
$$Bijective (H1Cotangent.map P.toInfinitesimal)$$
Lean4
theorem map_toInfinitesimal_bijective (P : Extension.{u} R S) :
Function.Bijective (CotangentSpace.map P.toInfinitesimal) :=
by
suffices CotangentSpace.map P.toInfinitesimal = (tensorKaehlerQuotKerSqEquiv _ _ _).symm.toLinearMap by rw [this];
exact (tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective
letI : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ _))
have : IsScalarTower P.Ring P.infinitesimal.Ring S := .of_algebraMap_eq' rfl
apply LinearMap.restrictScalars_injective P.Ring
ext x a
dsimp
simp only [map_tmul, algebraMap_self, RingHom.id_apply, Hom.toAlgHom_apply]
exact (tensorKaehlerQuotKerSqEquiv_symm_tmul_D _ _).symm
