isClosed_support — Mathlib

English

If M is a finitely generated module over R, then its support in Spec(R) is a closed subset of the spectrum.

Русский

Если M конечнопорционен над R, то поддержка M в Spec(R) является замкнутым подмножеством спектра.

LaTeX

$$$\\text{Module.Finite }\\Rightarrow \\mathrm{IsClosed}(\\mathrm{Module.support }\\ R M)$$$

Lean4

theorem isClosed_support [Module.Finite R M] : IsClosed (Module.support R M) :=
  by
  rw [support_eq_zeroLocus]
  apply PrimeSpectrum.isClosed_zeroLocus

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