isOpen_smoothLocus — Mathlib

English

If R and A are finitely presented, the smooth locus of A over R is an open subset of the prime spectrum of A.

Русский

Если R и A имеют конечную презентацию, гладкий локус A над R является открытым подмножеством спектра примитивных идеалов A.

LaTeX

$$$\mathrm{IsOpen}(\mathrm{smoothLocus}(R,A))$$$

Lean4

theorem isOpen_smoothLocus [FinitePresentation R A] : IsOpen (smoothLocus R A) :=
  by
  rw [isOpen_iff_forall_mem_open]
  intro x hx
  obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hxf, hf⟩ :=
    isBasis_basic_opens.exists_subset_of_mem_open (smoothLocus_eq_compl_support_inter.le hx).2 Module.isOpen_freeLocus
  rw [Module.basicOpen_subset_freeLocus_iff] at hf
  let Af := Localization.Away f
  have : Algebra.FinitePresentation A (Localization.Away f) := IsLocalization.Away.finitePresentation f
  have : Algebra.FinitePresentation R (Localization.Away f) := .trans _ A _
  have : IsOpen (smoothLocus R Af) :=
    by
    have := IsLocalizedModule.iso (.powers f) (KaehlerDifferential.map R R A (Localization.Away f))
    have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
    have := Module.Projective.of_equiv this
    rw [smoothLocus_eq_compl_support_inter, Module.support_eq_zeroLocus]
    exact (isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus
  rw [← smoothLocus_comap_of_isLocalization f] at this
  replace this := (PrimeSpectrum.localization_away_isOpenEmbedding Af f).isOpenMap _ this
  rw [Set.image_preimage_eq_inter_range, localization_away_comap_range Af f] at this
  exact ⟨_, Set.inter_subset_left, this, hx, hxf⟩

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