English
There exists a natural algebra isomorphism between the two-step quotients (A/I)/(J') and (A/J)/(I'); this natural isomorphism is denoted quotQuotEquivCommₐ and its evaluation commutes with swapping I and J.
Русский
Существует естественный алгебраический изоморфизм между двукратными фактор-кольцами (A/I)/(J') и (A/J)/(I'); этот изоморфизм обозначается как quotQuotEquivCommₐ и он сохраняет равенство при обмене I и J.
LaTeX
$$$((A \overline{/} I) \overline{/} J') \cong ((A \overline{/} J) \overline{/} I')$
(где $J', I'$ — образы $J, I$ в соответствующих фактор-алгебрах).$$
Lean4
/-- The natural algebra isomorphism `(A / I) / J' → (A / J) / I'`,
where `J'` (resp. `I'`) is the projection of `J` in `A / I` (resp. `I` in `A / J`). -/
def quotQuotEquivCommₐ : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] (A ⧸ J) ⧸ I.map (Quotient.mkₐ R J) :=
AlgEquiv.ofRingEquiv (f := quotQuotEquivComm I J) fun _ => rfl
