English
For x in the kernel of Q, the formula δ_eq_δAux shows that δ on the class ⟨x, hx⟩ equals δAux on x, tying δ to a base-change compatible δAux.
Русский
Для элемента x из ядра Q верна формула δ_eq_δAux: δ на классе ⟨x, hx⟩ равен δAux на x, что связывает δ с совместимым δAux через базовое изменение.
LaTeX
$$$\delta Q P ⟨.mk x, hx\rangle = δAux R Q x.1$$$
Lean4
theorem δ_eq_δAux (x : Q.ker) (hx) : δ Q P ⟨.mk x, hx⟩ = δAux R Q x.1 :=
by
let y := Extension.Cotangent.mk (P := (Q.comp P).toExtension) (Q.kerCompPreimage P x)
have hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x :=
by
simp only [y, Extension.Cotangent.map_mk]
congr
exact ofComp_kerCompPreimage Q P x
let z := (CotangentSpace.compEquiv Q P ((Q.comp P).toExtension.cotangentComplex y)).2
rw [H1Cotangent.δ_eq (y := y) (z := z)]
· rw [← ofComp_kerCompPreimage Q P x, δAux_ofComp]
rfl
· exact hy
· rw [← CotangentSpace.compEquiv_symm_inr]
apply (CotangentSpace.compEquiv Q P).injective
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_inr, Function.comp_apply,
LinearEquiv.apply_symm_apply, z]
ext
swap; · rfl
change
0 =
(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
(CotangentSpace.compEquiv Q P).toLinearMap)
((Q.comp P).toExtension.cotangentComplex y)
rw [CotangentSpace.fst_compEquiv, Extension.CotangentSpace.map_cotangentComplex, hy, hx]
