toEnd_baseChange — Mathlib

English

If A is an R-algebra, any Lie submodule N of M may be pushed forward to a LieSubmodule of A ⊗ M via baseChange, with the bracket structure extended accordingly.

Русский

Если A — R-алгебра, любое подмодуль Ли N под M можно перенести в LieSubmodule(A⊗M) через baseChange, с соответствующим продолжением скобки.

LaTeX

$$$\text{baseChange } A\ N : \text{LieSubmodule } A (A\otimes_R L) (A\otimes_R M)$$$

Lean4

@[simp]
theorem toEnd_baseChange (x : L) : toEnd A (A ⊗[R] L) (A ⊗[R] M) (1 ⊗ₜ x) = (toEnd R L M x).baseChange A := by ext; simp

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