English
The connecting map δ does not depend on the chosen presentation of S as a Generators of R and T: δ is invariant under replacing P by P'.
Русский
Связующее отображение δ не зависит от выбранной презентации S как порождающей над R и T: δ сохраняется при замене P на P'.
LaTeX
$$$\delta Q P = δ Q P'.$$$
Lean4
/-- The connecting homomorphism in the Jacobi-Zariski sequence for given presentations.
Given representations `0 → I → R[X] → S → 0` and `0 → K → S[Y] → T → 0`,
we may consider the induced representation `0 → J → R[X, Y] → T → 0`,
and this map is obtained by applying snake lemma to the following diagram
```
T ⊗[S] Ω[S/R] → Ω[T/R] → Ω[T/S] → 0
↑ ↑ ↑
0 → T ⊗[S] (⨁ₓ S dx) → (⨁ₓ T dx) ⊕ (⨁ᵧ T dy) → ⨁ᵧ T dy → 0
↑ ↑ ↑
T ⊗[S] (I/I²) → J/J² → K/K² → 0
↑ ↑
H¹(L_{T/R}) → H¹(L_{T/S})
```
This is independent from the presentations chosen. See `H1Cotangent.δ_comp_equiv`.
-/
noncomputable def δ : Q.toExtension.H1Cotangent →ₗ[T] T ⊗[S] Ω[S⁄R] :=
SnakeLemma.δ' (P.toExtension.cotangentComplex.baseChange T) (Q.comp P).toExtension.cotangentComplex
Q.toExtension.cotangentComplex ((Extension.Cotangent.map (toComp Q P).toExtensionHom).liftBaseChange T)
(Extension.Cotangent.map (ofComp Q P).toExtensionHom) (Cotangent.exact Q P)
((Extension.CotangentSpace.map (toComp Q P).toExtensionHom).liftBaseChange T)
(Extension.CotangentSpace.map (ofComp Q P).toExtensionHom) (CotangentSpace.exact Q P)
(map_comp_cotangentComplex_baseChange Q P)
(by ext; exact Extension.CotangentSpace.map_cotangentComplex (ofComp Q P).toExtensionHom _)
Q.toExtension.h1Cotangentι (LinearMap.exact_subtype_ker_map _) (N₁ := T ⊗[S] P.toExtension.CotangentSpace)
(P.toExtension.toKaehler.baseChange T)
(lTensor_exact T P.toExtension.exact_cotangentComplex_toKaehler P.toExtension.toKaehler_surjective)
(Cotangent.surjective_map_ofComp Q P) (CotangentSpace.map_toComp_injective Q P)
