stableUnderSpecialization_support

English

The support of a module is stable under specialization: if a point lies in the support, any specialization of it also lies in the support.

Русский

Поддержка модуля стабильна по специализации: если точка принадлежит поддержке, то любая ее специализация также принадлежит поддержке.

LaTeX

$$$\\text{StableUnderSpecialization}(\\mathrm{Module.support}\\ R M)$$$

Lean4

theorem stableUnderSpecialization_support : StableUnderSpecialization (Module.support R M) :=
  by
  intro x y e H
  rw [mem_support_iff_exists_annihilator] at H ⊢
  obtain ⟨m, hm⟩ := H
  exact ⟨m, hm.trans ((PrimeSpectrum.le_iff_specializes _ _).mpr e)⟩

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