δ — Mathlib · SciLib

English

The connecting homomorphism δ in the Jacobi–Zariski sequence is defined as a canonical linear map from H1Cotangent S T to T ⊗S Ω[S/R].

Русский

Соединяющее отображение δ в последовательности Jacobi–Zariski есть каноническое линейное отображение из H1Cotangent(S,T) в T ⊗S Ω[S/R].

LaTeX

$$$\\delta : H1Cotangent\\; S\\; T \\rightarrow_{} T \\otimes_S \\Omega[S/R]$$$

Lean4

/-- The connecting homomorphism in the Jacobi-Zariski sequence. -/
noncomputable def δ : H1Cotangent S T →ₗ[T] T ⊗[S] Ω[S⁄R] :=
  Generators.H1Cotangent.δ (Generators.self S T) (Generators.self R S)

Похожие утверждения