English
Let R be a ring, A an R-algebra, and I a two-sided ideal of A. Then the quotient A/I carries a canonical algebra structure over the quotient ring R / (I.comap(algebraMap R A)). In other words, A/I becomes an algebra over R/(I pulled back along the structure map).
Русский
Пусть R — кольцо, A — алгебра над R, и I — двусторонний идеал A. Тогда частное кольца A/I естественным образом приобретает структуру алгебры над кольцом R / (I.comap(algebraMap R A)). Другими словами, A/I является R/(I, вытягиваемое через алгебраическую карту)–алгеброй.
LaTeX
$$$\\mathrm{Algebra}\\left(R \\big/ I.\\mathrm{comap}(\\mathrm{algebraMap}\\; R\\; A),\\; A / I\\right)$$$
Lean4
instance (priority := 100) quotientAlgebra {R} [CommRing R] {I : Ideal A} [I.IsTwoSided] [Algebra R A] :
Algebra (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) :=
Quotient.algebraQuotientOfLEComap le_rfl
