English
The auxiliary connecting map δAux: Q.Ring →ₗ R (T ⊗_S Ω[S/R]) is defined by summing over the generators with the D-derivation; it behaves additively and satisfies Leibniz rule with respect to multiplication of generators.
Русский
Вспомогательное отображение δAux: Q.Ring →ₗ_R (T ⊗_S Ω[S/R]) задаётся суммированием по генераторам с деривацией D и ведёт себя по аддитивности и по правилу Лейбница относительно умножения генераторов.
LaTeX
$$$$ \\deltaAux : Q.Ring \\to_R T \\otimes_S \Omega[S/R], \\quad \\deltaAux\\,(f g) = f \\cdot \\deltaAux(g) + g \\cdot \\deltaAux(f) $$$$
Lean4
/-- Given `0 → I → S[Y] → T → 0`, this is an auxiliary map from `S[Y]` to `T ⊗[S] Ω[S⁄R]` whose
restriction to `ker(I/I² → ⊕ S dyᵢ)` is the connecting homomorphism in the Jacobi-Zariski sequence.
-/
noncomputable def δAux : Q.Ring →ₗ[R] T ⊗[S] Ω[S⁄R] :=
Finsupp.lsum R (R := R) fun f ↦
(TensorProduct.mk S T _ (f.prod (Q.val · ^ ·))).restrictScalars R ∘ₗ (D R S).toLinearMap
