English
For two-sided ideals I ≤ J in A, there exists an algebra homomorphism from A/I to A/J that realizes the canonical factorization of the quotient maps; i.e., the natural map factors through the larger quotient.
Русский
Для двусторонних идеалов I ≤ J в A существует алгебраическое отображение A/I → A/J, реализующее каноническое разложение фактором двухкратной факторизации; естественный отображатель действует через больший фактор.
LaTeX
$$${I,J:A\text{ ideals of }A\;}(I\le J)\; \Rightarrow\; A/I \toₐ[R_1] A/J$$$
Lean4
/-- `AlgHom` version of `Ideal.Quotient.factor`. -/
def factorₐ {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (hIJ : I ≤ J) : A ⧸ I →ₐ[R₁] A ⧸ J
where
__ := Ideal.Quotient.factor hIJ
commutes' _ := rfl
