mkₐ — Mathlib

English

There is a canonical R1-algebra homomorphism mkₐ from A to A/I, which is the algebraic realization of the quotient map.

Русский

Существует каноническое R1-алгебраическое отображение mkₐ: A → A/I, являющееся алгебраическим реализатором факторирования по I.

LaTeX

$$$ \text{mkₐ}^{R_1}_I: A \to_{R_1} A/I \text{ is a canonical algebra homomorphism} $$$

Lean4

/-- The canonical morphism `A →ₐ[R₁] A ⧸ I` as morphism of `R₁`-algebras, for `I` an ideal of
`A`, where `A` is an `R₁`-algebra. -/
def mkₐ (I : Ideal A) [I.IsTwoSided] : A →ₐ[R₁] A ⧸ I :=
  ⟨⟨⟨⟨fun a => Submodule.Quotient.mk a, rfl⟩, fun _ _ => rfl⟩, rfl, fun _ _ => rfl⟩, fun _ => rfl⟩

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