English
Let f be a morphism between generator systems and x an element of the source H1Cotangent; then the connecting homomorphism δ is compatible with applying the generator-map to x, i.e. δ of the image equals δ of x.
Русский
Пусть f — морфизм между системами генераторов, а x — элемент пространства H1Cotangent; тогда отображение δ совместимо с отображением генераторов: δ(образ(x)) = δ(x).
LaTeX
$$$\\delta_{Q,P} \\bigl( \\mathrm{Extension.H1Cotangent.map}(f)\\, x \\bigr) \\\\stackrel{?}{=} \\delta_{Q',P'}(x).$$$
Lean4
theorem δ_map (f : Hom Q' Q) (x) : δ Q P (Extension.H1Cotangent.map f.toExtensionHom x) = δ Q' P' x :=
by
letI : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
obtain ⟨x, hx⟩ := x
obtain ⟨⟨y, hy⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
change δ _ _ ⟨_, _⟩ = δ _ _ _
replace hx : (1 : T) ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0 := by
simpa only [LinearMap.mem_ker, Extension.cotangentComplex_mk, ker, RingHom.mem_ker] using hx
simp only [LinearMap.domRestrict_apply, Extension.Cotangent.map_mk, δ_eq_δAux]
refine (δAux_toAlgHom f _).trans ?_
rw [hx, map_zero, map_zero, add_zero]
