English
Let I be a two-sided ideal of a ring A, and let x belong to the domain R1. Then the image of x under the algebra map into A is compatible with passing to the quotient A/I; i.e., the quotient map commutes with the algebra map from R1. Equivalently, the natural map which sends x to algebraMap R1 A x, then to A/I, equals the map sending x directly to algebraMap R1 (A/I) x.
Русский
Пусть I — двусторонний идеал кольца A, и пусть x ∈ R1. Тогда образ x через алгебраическую карту в A согласуется с переходом к факторкольцу A/I; то есть естественная карта факторизации через I согласована с алгебраическим отображением из R1 в A/I: mk I (algebraMap R1 A x) = algebraMap R1 (A/I) x.
LaTeX
$$$\operatorname{Quotient.mk} I\ (\operatorname{algebraMap} R_1 A\ x) = \operatorname{algebraMap} R_1 (A \;\!\mathbin{\usebox{quotient}}\ I)\ x$$$
Lean4
@[simp]
theorem mk_algebraMap (I : Ideal A) [I.IsTwoSided] (x : R₁) :
Quotient.mk I (algebraMap R₁ A x) = algebraMap R₁ (A ⧸ I) x :=
rfl
