English
For every appropriate map between generator systems, the induced map between their H1Cotangent spaces is exact with respect to δ, i.e., the image of the map equals the kernel of δ.
Русский
Для каждого допустимого отображения между системами генераторов индуцированное отображение между их H1Cotangent-пространствами образует точную последовательность: образ = ядро(δ).
LaTeX
$$$\\operatorname{Im}\\bigl( \\mathrm{Extension.H1Cotangent.map}(f) \\bigr) \;=\; \\ker( \\delta_{Q,P} ).$$$
Lean4
/-- A variant of `exact_map_δ` that takes in an arbitrary map between generators. -/
theorem exact_map_δ' (f : Hom W Q) : Function.Exact (Extension.H1Cotangent.map f.toExtensionHom) (δ Q P) :=
by
refine (H1Cotangent.equiv (Q.comp P) W).surjective.comp_exact_iff_exact.mp ?_
change
Function.Exact ((Extension.H1Cotangent.map f.toExtensionHom).restrictScalars T ∘ₗ (Extension.H1Cotangent.map _))
(δ Q P)
rw [← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq _ (Q.ofComp P).toExtensionHom]
exact exact_map_δ Q P
