stableUnderSpecialization_singleton

English

For a point x in the prime spectrum of a ring, the singleton {x} is stable under specialization if and only if x.asIdeal is a maximal ideal.

Русский

Для точки x в спектре простых идеалов кольца множество {x} стабильно относительно специализации тогда и только тогда, когда соответствующий идеал x является максимальным.

LaTeX

$$$$ \operatorname{StableUnderSpecialization}(\{x\}) \iff x.\operatorname{asIdeal}.\operatorname{IsMaximal}. $$$$

Lean4

theorem stableUnderSpecialization_singleton {x : PrimeSpectrum R} :
    StableUnderSpecialization { x } ↔ x.asIdeal.IsMaximal :=
  by
  simp_rw [← isMax_iff, StableUnderSpecialization, ← le_iff_specializes, Set.mem_singleton_iff, @forall_comm _ (_ = _),
    forall_eq]
  exact ⟨fun H a h ↦ (H a h).le, fun H a h ↦ le_antisymm (H h) h⟩

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