English
Let A be a ring and I, J be two-sided ideals of A (with suitable algebra structure over a commutative semiring). There is a canonical isomorphism between the two-step quotients (A/I) modulo the image of J in A/I and (A/J) modulo the image of I in A/J. Moreover, the symmetry that swaps I and J yields the inverse isomorphism, and this inverse coincides with the canonical isomorphism obtained by swapping the order of quotients.
Русский
Пусть A — кольцо, I и J — двухсторонние идеалы A (при наличии соответствующей алгебраической структуры над коммутативным полем). Существует канонический изоморфизм между двумяступенчатыми фактор-ringами (A/I) / J' и (A/J) / I', где J' и i' — образы J и I в соответствующих фактор-алгебрах. Более того, симметрия, которая меняет местами I и J, даёт обратный изоморфизм, и этот обратный изоморфизм совпадает с каноническим изоморфизмом, полученным перекрещиванием порядков факторирования.
LaTeX
$$$((A/I) / J') \cong ((A/J) / I')$, where $J' = \mathrm{Im}(J \to A/I)$ and $I' = \mathrm{Im}(I \to A/J)$.$$
Lean4
@[simp]
theorem quotQuotEquivQuotSupₐ_symm_toRingEquiv :
((quotQuotEquivQuotSupₐ R I J).symm : _ ≃+* _ ⧸ J.map (Quotient.mkₐ R I)) = (quotQuotEquivQuotSup I J).symm :=
rfl
