exact_δ_mapBaseChange — Mathlib

English

A variant of exactness asserting that for a given f between generator spaces, the δ-map together with the extension map yields an exact sequence.

Русский

Вариант точности: для данного отображения между пространствами генераторов отображения δ и обычного отображения образуют точную последовательность.

LaTeX

$$$\\operatorname{Im}(\\mathrm{Extension.H1Cotangent.map}(f)) = \\ker(\\delta_{Q,P}).$$$

Lean4

/-- Given algebras `R → S → T`, `H¹(L_{T/S}) → T ⊗[S] Ω[S/R] → Ω[T/R]` is exact. -/
theorem exact_δ_mapBaseChange : Function.Exact (δ R S T) (mapBaseChange R S T) :=
  Generators.H1Cotangent.exact_δ_map (Generators.self S T) (Generators.self R S)

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