English
Let P be a PreSubmersivePresentation of R into S with finite σ, and let x lie in the kernel of P. Then for every i in σ, the i-th component of the cotangentComplexAux at Cotangent.mk x coincides with the evaluation, via aeval, of the derivation pderiv (P.map i) applied to x, on P.val.
Русский
Пусть P — пред-subмёрсивное представление R в S с конечным набором σ, и пусть x лежит в ядре P. Тогда для каждого i в σ i-й компонент касательного комплекса при Cotangent.mk x совпадает с оценкой, по aeval, производной pderiv (P.map i), примененной к x, на P.val.
LaTeX
$$$P.cotangentComplexAux (Cotangent.mk x) i = (\\mathrm{aeval} P.val) (\\mathrm{pderiv} (P.map i) x.val) \\quad\\text{for all } i \\in σ$$$
Lean4
theorem cotangentComplexAux_apply [Finite σ] (P : PreSubmersivePresentation R S ι σ) (x : P.ker) (i : σ) :
P.cotangentComplexAux (Cotangent.mk x) i = (aeval P.val) (pderiv (P.map i) x.val) :=
by
dsimp only [cotangentComplexAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, cotangentComplex_mk]
simp only [Generators.toExtension_Ring, Finsupp.lcomapDomain_apply, Finsupp.linearEquivFunOnFinite_apply,
Finsupp.comapDomain_apply, Generators.cotangentSpaceBasis_repr_tmul, one_mul]
