quotQuotToQuotSupₐ — Mathlib

English

The underlying RingHom of quotQuotMkₐ R I J equals quotQuotMk I J; i.e., the two realizations of the MK map agree.

Русский

Базовое кольцевое отображение quotQuotMkₐ совпадает с quotQuotMk I J; обе реализации MK-отображения совпадают.

LaTeX

$$$(quotQuotMkₐ R I J) : _ \to+* _ = quotQuotMk I J$$$

Lean4

/-- The algebra homomorphism `(A / I) / J' -> A / (I ⊔ J)` induced by `quotQuotToQuotSup`,
  where `J'` is the projection of `J` in `A / I`. -/
def quotQuotToQuotSupₐ : (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I) →ₐ[R] A ⧸ I ⊔ J :=
  AlgHom.mk (quotQuotToQuotSup I J) fun _ => rfl

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