quotQuotEquivQuotSupₐ — Mathlib

English

The equivalence quotQuotEquivQuotSupₐ is the canonical isomorphism between ((A/I) ⧸ J.map (Quotient.mkₐ R I)) and (A ⧸ I ⊔ J).

Русский

Эквивалент quotQuotEquivQuotSupₐ является каноническим изоморфизмом между двойным фактором и фактором по сумме I ⊔ J.

LaTeX

$$$((A \text{ ⧸ } I) \ ⧸ J.map (Quotient.mkₐ R I)) \cong A \ ⧸ (I \sqcup J)$$$

Lean4

/-- `quotQuotToQuotSup` and `liftSupQuotQuotMk` are inverse isomorphisms. In the case where
`I ≤ J`, this is the Third Isomorphism Theorem (see `DoubleQuot.quotQuotEquivQuotOfLE`). -/
def quotQuotEquivQuotSupₐ : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] A ⧸ I ⊔ J :=
  AlgEquiv.ofRingEquiv (f := quotQuotEquivQuotSup I J) fun _ => rfl

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