algebraMap_residueField_eq_zero — Mathlib

English

The kernel of the algebra map from R to I.ResidueField equals I.

Русский

Ядро алгебраического отображения R → I.ResidueField равно I.

LaTeX

$$$\ker(\mathrm{algebraMap}\; R \; I.\mathrm{ResidueField}) = I.$$$

Lean4

@[simp high] -- marked `high` to override the more general `FaithfulSMul.algebraMap_eq_zero_iff`

theorem algebraMap_residueField_eq_zero {x} : algebraMap R I.ResidueField x = 0 ↔ x ∈ I :=
  by
  rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I), IsLocalRing.ResidueField.algebraMap_eq,
    IsLocalRing.residue_eq_zero_iff]
  exact IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _

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