restrictScalars — Mathlib

English

If d is a derivation R B M, then its action on the algebra map results in a derivation on A, preserving Leibniz and units.

Русский

Если d — деривация R B M, то её действие на алгебраическую карту дает деривацию на A, сохраняющую лейбнисову форму и единицы.

LaTeX

$$$d( ab ) = a d(b) + d(a) b$ for relevant a,b; map_one_eq_zero' holds.$$

Lean4

/-- If `A` is both an `R`-algebra and an `S`-algebra; `M` is both an `R`-module and an `S`-module,
then an `S`-derivation `A → M` is also an `R`-derivation if it is also `R`-linear. -/
protected def restrictScalars (d : Derivation S A M) : Derivation R A M
    where
  map_one_eq_zero' := d.map_one_eq_zero
  leibniz' := d.leibniz
  toLinearMap := d.toLinearMap.restrictScalars R

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