derivationTensorProduct_algebraMap

English

For x in A, the derivation on the image of x under the algebra map A → B is the canonical element 1 ⊗₂ D_{R,A}(x) in S ⊗_R Ω_{A/R}.

Русский

Для x ∈ A производная на образе x через алгебраическую карту A → B равна каноническому элементу 1 ⊗ D_{R,A}(x) в S ⊗_R Ω_{A/R}.

LaTeX

$$$\\mathrm{derivationTensorProduct}(R,S,A,B)(\\mathrm{algebraMap}_{A,B}(x)) = 1 \\otimes_\\text{tmul} D_{R,A}(x)$$$

Lean4

theorem derivationTensorProduct_algebraMap [Algebra.IsPushout R S A B] (x) :
    derivationTensorProduct R S A B (algebraMap A B x) = 1 ⊗ₜ D _ _ x :=
  IsBaseChange.lift_eq _ _ _

Похожие утверждения