English
There is a canonical S-derivation from B = S ⊗_R A to S ⊗_R Ω_{A/R}, constructed by pushing out the universal derivation D_{R/A} along the pushout. This derivation extends the differential structure from A to the tensor product.
Русский
Существует каноническая S-деривация от B = S ⊗_R A к S ⊗_R Ω_{A/R}, полученная конструированием через пуш-аута и универсальное дифференциальное отображение D_{R/A}; эта деривация расширяет дифференциал от A на тензорное произведение.
LaTeX
$$$\\mathrm{Derivation}_S(B,\\, S \\otimes_R \\Omega_{A/R})$$$
Lean4
/-- (Implementation).
The `S`-derivation `B = S ⊗[R] A` to `S ⊗[R] Ω[A⁄R]` sending `a ⊗ b` to `a ⊗ d b`. -/
noncomputable def derivationTensorProduct [h : Algebra.IsPushout R S A B] : Derivation S B (S ⊗[R] Ω[A⁄R])
where
__ := h.out.lift ((TensorProduct.mk R S Ω[A⁄R] 1).comp (D R A).toLinearMap)
map_one_eq_zero' := by
rw [← (algebraMap A B).map_one]
refine (h.out.lift_eq _ _).trans ?_
dsimp
rw [Derivation.map_one_eq_zero, TensorProduct.tmul_zero]
leibniz' a
b := by
induction a using h.out.inductionOn with
| zero => rw [map_zero, zero_smul, smul_zero, zero_add, zero_mul, map_zero]
| smul x y e => rw [smul_mul_assoc, map_smul, e, map_smul, smul_add, smul_comm x b, smul_assoc]
| add b₁ b₂ e₁ e₂ => simp only [add_mul, add_smul, map_add, e₁, e₂, smul_add, add_add_add_comm]
| tmul z =>
dsimp
induction b using h.out.inductionOn with
| zero => rw [map_zero, zero_smul, smul_zero, zero_add, mul_zero, map_zero]
| tmul =>
simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom', algebraMap_smul, ← map_mul]
rw [← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq, ←
IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq, ← IsScalarTower.toAlgHom_apply R, ←
AlgHom.toLinearMap_apply, h.out.lift_eq]
simp only [LinearMap.coe_comp, Derivation.coeFn_coe, Function.comp_apply, Derivation.leibniz, mk_apply,
mulActionBaseChange_smul_tmul, TensorProduct.tmul_add]
| smul _ _ e => rw [mul_comm, smul_mul_assoc, map_smul, mul_comm, e, map_smul, smul_add, smul_comm, smul_assoc]
| add _ _ e₁ e₂ => simp only [mul_add, add_smul, map_add, e₁, e₂, smul_add, add_add_add_comm]
