isOpen_unramifiedLocus — Mathlib

English

If A is essentially of finite type over R, then the unramified locus in Spec(R) is an open subset.

Русский

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

LaTeX

$$$[\\text{EssFiniteType } R A]\\; \\Rightarrow\\; \\text{IsOpen}(\\mathrm{unramifiedLocus}(R,A)).$$$

Lean4

theorem isOpen_unramifiedLocus [EssFiniteType R A] : IsOpen (unramifiedLocus R A) :=
  by
  rw [unramifiedLocus_eq_compl_support, Module.support_eq_zeroLocus]
  exact (PrimeSpectrum.isClosed_zeroLocus _).isOpen_compl

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