quotQuotEquivComm — Mathlib

English

The obvious isomorphism (R/I)/J' ≅ (R/J)/I' is implemented as a commutative isomorphism.

Русский

Очевидный изоморфизм (R/I)/J' ≅ (R/J)/I' реализован как коммутативный изоморфизм.

LaTeX

$$$(R \\!/ I) \\!/ (J.map(\\mathrm{Quotient.mk} I)) \\cong (R \\!/ J) \\!/ (I.map(\\mathrm{Quotient.mk} J))$$$

Lean4

/-- The obvious isomorphism `(R/I)/J' → (R/J)/I'` -/
def quotQuotEquivComm : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* (R ⧸ J) ⧸ I.map (Ideal.Quotient.mk J) :=
  ((quotQuotEquivQuotSup I J).trans (quotEquivOfEq (sup_comm ..))).trans (quotQuotEquivQuotSup J I).symm

Похожие утверждения