residueField_specComap — Mathlib

English

The range of the map algebraMap R I.asIdeal.ResidueField .specComap consists of exactly the singleton { I } in PrimeSpectrum.

Русский

Диапазон отображения algebraMap R I.asIdeal.ResidueField .specComap состоит ровно из единственного элемента { I } в PrimeSpectrum.

LaTeX

$$$\\operatorname{range} (\\operatorname{algebraMap} R I.asIdeal.ResidueField).\\operatorname{specComap} = \\{ I \\}$$$

Lean4

theorem residueField_specComap (I : PrimeSpectrum R) :
    Set.range (algebraMap R I.asIdeal.ResidueField).specComap = { I } :=
  by
  rw [Set.range_unique, Set.singleton_eq_singleton_iff]
  exact PrimeSpectrum.ext (Ideal.ext fun x ↦ Ideal.algebraMap_residueField_eq_zero)

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