lift_algebraMap — Mathlib

English

The lift preserves scalar multiplication by elements of the base ring, i.e., it commutes with the algebra maps from R into B.

Русский

Поднятие сохраняет действие скаляров из базового кольца R, то есть он коммутирует с алгебраическими отображениями из R в B.

LaTeX

$$$\mathrm{lift}(R,A)\; maps\; (\mathrm{algebraMap}\; R\; (\mathrm{FreeProduct}\; R\; A)\; r) = (\mathrm{algebraMap}\; R\; B\; r)$$$

Lean4

@[simp↓]
theorem lift_algebraMap (r : R) : lift R A maps (algebraMap R _ r) = algebraMap R _ r := by
  rw [lift_apply, AlgHom.commutes]

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