English
On a representative element of the kernel, δ coincides with δAux after identifying via the cotangent-equivariant identification: δ and δAux agree on the kernel generator up to the canonical identifications.
Русский
На представителе ядра отображения δ совпадает с δAux после идентификации через каноническое соответствие котантной пространства: δ и δAux совпадают на порождающем элемента ядра.
LaTeX
$$$\delta Q P \langle. mk x, hx\rangle = δAux R Q x.1$$$
Lean4
theorem exact_δ_map : Function.Exact (δ Q P) (mapBaseChange R S T) :=
by
simp only [δ]
apply
SnakeLemma.exact_δ_left (π₂ := (Q.comp P).toExtension.toKaehler) (hπ₂ :=
(Q.comp P).toExtension.exact_cotangentComplex_toKaehler)
· apply (P.cotangentSpaceBasis.baseChange T).ext
intro i
simp only [Basis.baseChange_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.baseChange_tmul,
toKaehler_cotangentSpaceBasis, mapBaseChange_tmul, map_D, one_smul, LinearMap.liftBaseChange_tmul]
rw [cotangentSpaceBasis_apply]
conv_rhs => enter [2]; tactic => exact Extension.CotangentSpace.map_tmul ..
simp only [map_one, mapBaseChange_tmul, map_D, one_smul]
simp [Extension.Hom.toAlgHom]
· exact LinearMap.lTensor_surjective T P.toExtension.toKaehler_surjective
