English
For towers R → A → B with algebra structure, composing a derivation of B into M with the algebra map A → B yields a derivation of A into M.
Русский
Для башни R → A → B с алгебраической структурой композиция деривации B → M с алгебраической картой A → B даёт деривацию A → M.
LaTeX
$$$\text{compAlgebraMap} : \mathrm{Derivation}(R,B,M) \to \mathrm{Derivation}(R,A,M)$$$
Lean4
/-- For a tower `R → A → B` and an `R`-derivation `B → M`, we may compose with `A → B` to obtain an
`R`-derivation `A → M`. -/
@[simps!]
def compAlgebraMap [Algebra A B] [IsScalarTower R A B] [IsScalarTower A B M] (d : Derivation R B M) : Derivation R A M
where
map_one_eq_zero' := by simp
leibniz' a b := by simp
toLinearMap := d.toLinearMap.comp (IsScalarTower.toAlgHom R A B).toLinearMap
