English
The δ map defined using the full construction equals the δAux map on the kernel representatives, i.e., δ maps kernel elements to δAux of their representative.
Русский
Отображение δ, определённое через композицию, равно δAux на представителях ядра; то есть δ применяется к элементам ядра через δAux.
LaTeX
$$$$ \delta\,Q\,P(\langle x, hx \rangle) = \deltaAux\,R\,Q(x) $$$$
Lean4
theorem δAux_toAlgHom (f : Hom Q Q') (x) :
δAux R Q' (f.toAlgHom x) =
δAux R Q x +
Finsupp.linearCombination _ (δAux R Q' ∘ f.val)
(Q.cotangentSpaceBasis.repr ((1 : T) ⊗ₜ[Q.Ring] D S Q.Ring x :)) :=
by
letI : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
have : IsScalarTower Q.Ring Q.Ring T := IsScalarTower.left _
induction x using MvPolynomial.induction_on with
| C s => simp [MvPolynomial.algebraMap_eq, δAux_C]
| add x₁ x₂ hx₁ hx₂ =>
simp only [map_add, hx₁, hx₂, tmul_add]
rw [add_add_add_comm]
| mul_X p n
IH =>
simp only [map_mul, Hom.toAlgHom_X, δAux_mul, algebraMap_apply, Hom.algebraMap_toAlgHom,
← @IsScalarTower.algebraMap_smul Q'.Ring T, algebraMap_self, δAux_X, RingHom.id_apply, coe_eval₂Hom, IH,
Hom.aeval_val, smul_add, map_aeval, tmul_add, tmul_smul, ← @IsScalarTower.algebraMap_smul Q.Ring T, smul_zero,
aeval_X, zero_add, Derivation.leibniz, LinearEquiv.map_add, LinearEquiv.map_smul, Basis.repr_self,
LinearMap.map_add, one_smul, LinearMap.map_smul, Finsupp.linearCombination_single, RingHomCompTriple.comp_eq,
Function.comp_apply, ← cotangentSpaceBasis_apply]
rw [add_left_comm]
rfl
