basicOpen_subset_smoothLocus_iff — Mathlib

English

For finite presentation over R, the inclusion of the basic open subset D(f) into the smooth locus is equivalent to A_f being formally smooth over the localization away from f.

Русский

Для конечной презентации над R включение базового открытого D(f) в гладкий локус эквивалентно тому, что A_f формально гладкая по отношению к локализации Away от f.

LaTeX

$$$(\mathrm{PrimeSpectrum}.\mathrm{basicOpen} f) \subseteq \mathrm{smoothLocus}(R,A) \;\iff\; \mathrm{FormallySmooth}(R, \mathrm{LocalizationAway}(A,f))$$$

Lean4

theorem basicOpen_subset_smoothLocus_iff [FinitePresentation R A] {f : A} :
    ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ Algebra.FormallySmooth R (Localization.Away f) :=
  by
  rw [smoothLocus_eq_compl_support_inter, Set.subset_inter_iff, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl, ← LocalizedModule.subsingleton_iff_support_subset,
    Algebra.FormallySmooth.iff_subsingleton_and_projective]
  congr! 1
  · have := IsLocalizedModule.iso (.powers f) (H1Cotangent.map R R A (Localization.Away f))
    rw [this.subsingleton_congr]
  · rw [← PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Module.basicOpen_subset_freeLocus_iff]
    have := IsLocalizedModule.iso (.powers f) (KaehlerDifferential.map R R A (Localization.Away f))
    have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
    exact ⟨fun _ ↦ .of_equiv this, fun _ ↦ .of_equiv this.symm⟩

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