exact_map_δ — Mathlib

English

The map δ from H1Cotangent to the base-extended cotangent spaces is exact with respect to the base-change map: δ and base-change interplay exactly as in the snake lemma configuration.

Русский

Отображение δ из H1Cotangent в базисно-перемещенные котангентные пространства является точным в отношении базового переноса: δ и базисное изменение взаимодействуют как в схеме змейки (snake lemma).

LaTeX

$$$\text{Exact}( \delta Q P, \; mapBaseChange R S T )$$$

Lean4

theorem exact_map_δ : Function.Exact (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) (δ Q P) :=
  by
  simp only [δ]
  apply SnakeLemma.exact_δ_right (ι₂ := (Q.comp P).toExtension.h1Cotangentι) (hι₂ := LinearMap.exact_subtype_ker_map _)
  · ext x; rfl
  · exact Subtype.val_injective

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