injective_algebraMap_quotient_residueField

English

Let I be a prime ideal of a commutative ring R. The natural algebra map from the quotient R/I into the residue field I.ResidueField is injective.

Русский

Пусть I — простая идеал в коммутативном кольце R. Естественное алгебраическое отображение из R/I в поле остатка I.ResidueField инъективно.

LaTeX

$$$\forall \{R\} [\mathrm{CommRing}\ R] \{I : \mathrm{Ideal}\ R\} [I.\mathrm{IsPrime}],\; \operatorname{Injective}\bigl(\operatorname{algebraMap}(R/\!I)\ I.\mathrm{ResidueField}\bigr)$$$

Lean4

theorem injective_algebraMap_quotient_residueField : Function.Injective (algebraMap (R ⧸ I) I.ResidueField) :=
  by
  rw [RingHom.injective_iff_ker_eq_bot]
  refine (Ideal.ker_quotient_lift _ _).trans ?_
  change map (Quotient.mk I) (RingHom.ker (algebraMap R I.ResidueField)) = ⊥
  rw [Ideal.ker_algebraMap_residueField, map_quotient_self]

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