algebraMap_quotient_injective — Mathlib

English

Let R be a commutative ring, A an R-algebra, and I a two-sided ideal of A. The induced algebra map from R/I to A/I is injective.

Русский

Пусть R — коммутативное кольцо, A — R-алгебра, I — двусторонний идеал A. Индукированная алгебраическая карта из R/I в A/I инъективна.

LaTeX

$$$\\operatorname{Injective}\\left(\\mathrm{algebraMap}\\left(R \\,/\\, I.\\mathrm{comap}(\\mathrm{algebraMap}\\; R\\; A),\\; A / I\\right)\\right)$$$

Lean4

theorem algebraMap_quotient_injective {R} [CommRing R] {I : Ideal A} [I.IsTwoSided] [Algebra R A] :
    Function.Injective (algebraMap (R ⧸ I.comap (algebraMap R A)) (A ⧸ I)) :=
  by
  rintro ⟨a⟩ ⟨b⟩ hab
  replace hab := Quotient.eq.mp hab
  rw [← RingHom.map_sub] at hab
  exact Quotient.eq.mpr hab

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