basicOpen_subset_smoothLocus_iff_smooth

English

The product of a finite family of R-algebras is formally smooth over R if and only if each factor is formally smooth over R.

Русский

Произведение конечной семьи R-алгебр гладко над R тогда и только тогда, когда каждая из них формально гладкая над R.

LaTeX

$$$\mathrm{FormallySmooth}(R, \prod_i A_i) \iff \forall i, \mathrm{FormallySmooth}(R, A_i)$$$

Lean4

theorem basicOpen_subset_smoothLocus_iff_smooth [FinitePresentation R A] {f : A} :
    ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ Algebra.Smooth R (Localization.Away f) :=
  by
  have : FinitePresentation A (Localization.Away f) := IsLocalization.Away.finitePresentation f
  rw [basicOpen_subset_smoothLocus_iff]
  exact ⟨fun H ↦ ⟨H, .trans _ A _⟩, fun H ↦ H.1⟩

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