Lean4
theorem δAux_ofComp (x : (Q.comp P).Ring) :
δAux R Q ((Q.ofComp P).toAlgHom x) =
P.toExtension.toKaehler.baseChange T
(CotangentSpace.compEquiv Q P (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x : _)).2 :=
by
letI : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
have : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T := IsScalarTower.left _
induction x using MvPolynomial.induction_on with
| C s =>
simp only [algHom_C, δAux_C, derivation_C, Derivation.map_algebraMap, tmul_zero, map_zero,
MvPolynomial.algebraMap_apply, Prod.snd_zero]
| add x₁ x₂ hx₁ hx₂ => simp only [map_add, hx₁, hx₂, tmul_add, Prod.snd_add]
| mul_X p n
IH =>
simp only [map_mul, Hom.toAlgHom_X, ofComp_val, δAux_mul, ← @IsScalarTower.algebraMap_smul Q.Ring T,
algebraMap_apply, Hom.algebraMap_toAlgHom, algebraMap_self, map_aeval, RingHomCompTriple.comp_eq, comp_val,
RingHom.id_apply, IH, Derivation.leibniz, tmul_add, tmul_smul, ← cotangentSpaceBasis_apply, coe_eval₂Hom,
← @IsScalarTower.algebraMap_smul (Q.comp P).Ring T, aeval_X, LinearEquiv.map_add, LinearMapClass.map_smul,
Prod.snd_add, Prod.smul_snd, LinearMap.map_add]
obtain (n | n) := n
·
simp only [Sum.elim_inl, δAux_X, smul_zero, aeval_X, CotangentSpace.compEquiv, LinearEquiv.trans_apply,
Basis.repr_symm_apply, zero_add, Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply,
LinearMap.coe_inl, LinearMap.coe_inr, Function.comp_apply, one_smul, map_zero]
· simp only [Sum.elim_inr, Function.comp_apply, algHom_C, δAux_C, CotangentSpace.compEquiv, LinearEquiv.trans_apply,
Basis.repr_symm_apply, algebraMap_smul, Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply,
LinearMap.coe_inr, Basis.baseChange_apply, one_smul, LinearMap.baseChange_tmul, toKaehler_cotangentSpaceBasis,
add_left_inj, LinearMap.coe_inl]
rfl
