English
There is an isomorphism of S-modules between S ⊗Q Ω[Q/R] and S ⊗P Ω[P/R], where Q = P/(ker(algebraMap P S))^2. This provides a canonical transfer of Kaehler differentials along the quotient.
Русский
Существует изоморфизм модулей над S между S ⊗Q Ω[Q/R] и S ⊗P Ω[P/R], где Q = P/(ker(algebraMap P S))^2. Это даёт канонический перенос Kaehler-дifferentials через тождество quotient.
LaTeX
$$$S \\otimes_{P/(\\ker(\\mathrm{algebraMap} P S))^2} \\Omega[(P/(\\ker(\\mathrm{algebraMap} P S))^2)/R] \\cong_S S \\otimes_P \\Omega[P/R]$$$
Lean4
/-- Given a tower of algebras `S/P/R`, with `I = ker(P → S)` and `Q := P/I²`,
there is an isomorphism of `S`-modules `S ⊗[Q] Ω[Q/R] ≃ S ⊗[P] Ω[P/R]`.
-/
noncomputable def tensorKaehlerQuotKerSqEquiv :
S ⊗[P ⧸ (RingHom.ker (algebraMap P S) ^ 2)] Ω[(P ⧸ (RingHom.ker (algebraMap P S) ^ 2))⁄R] ≃ₗ[S] S ⊗[P] Ω[P⁄R] :=
letI f₁ := (derivationQuotKerSq R P S).liftKaehlerDifferential
letI f₂ := AlgebraTensorModule.lift ((LinearMap.ringLmapEquivSelf S S _).symm f₁)
letI f₃ := KaehlerDifferential.map R R P (P ⧸ (RingHom.ker (algebraMap P S) ^ 2))
letI f₄ := ((mk (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S _ 1).restrictScalars P).comp f₃
letI f₅ := AlgebraTensorModule.lift ((LinearMap.ringLmapEquivSelf S S _).symm f₄)
{ __ := f₂
invFun := f₅
left_inv := by
suffices f₅.comp f₂ = LinearMap.id from LinearMap.congr_fun this
ext a
obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective a
simp [f₁, f₂, f₃, f₄, f₅]
right_inv := by
suffices f₂.comp f₅ = LinearMap.id from LinearMap.congr_fun this
ext a
simp [f₁, f₂, f₃, f₄, f₅] }
