quotQuotEquivQuotOfLEₐ — Mathlib

English

For a ring A and ideals I ≤ J with I,J two-sided, the natural algebra isomorphism between the two-step quotient ((A/I) / J') and A/J exists; equivalently, (A/I) / (J.map) ≅ A/J.

Русский

Для кольца A и идеалов I ≤ J, где I,J — двухсторонние, существует естественный алгебраический изоморфизм между двумя ступенями факторинга ((A/I) / J') и A/J; эквивалентно (A/I) / (J.map) ≅ A/J.

LaTeX

$$$((A \overline{/} I) \overline{/} (J \text{ image in } A/I)) \cong (A \overline{/} J)$$$

Lean4

/-- The **third isomorphism theorem** for algebras. See `quotQuotEquivQuotSupₐ` for version
    that does not assume an inclusion of ideals. -/
def quotQuotEquivQuotOfLEₐ (h : I ≤ J) : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] A ⧸ J :=
  AlgEquiv.ofRingEquiv (f := quotQuotEquivQuotOfLE h) fun _ => rfl

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