Smooth locus of an algebra

Most results in this file are proved for algebras of finite presentations. Some of them are true for arbitrary algebras but the proof is substantially harder.

Main results

• Algebra.smoothLocus : The set of primes that are smooth over the base.
• Algebra.basicOpen_subset_smoothLocus_iff : D(f) is contained in the smooth locus if and only if A_f is smooth over R.
• Algebra.smoothLocus_eq_univ_iff : The smooth locus is the whole spectrum if and only if A is smooth over R.
• Algebra.isOpen_smoothLocus : The smooth locus is open.

@[reducible, inline]

abbrev Algebra.IsSmoothAt (R : Type u) {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (p : Ideal A) [p.IsPrime] : Prop

An R-algebra A is smooth at a prime p of A if Aₚ is formally smooth over R.

This does not imply Aₚ is smooth over R under the mathlib definition even if A is finitely presented, but it can be shown that this is equivalent to the stacks project definition that A is smooth at p if and only if there exists f ∉ p such that A_f is smooth over R. See Algebra.basicOpen_subset_smoothLocus_iff_smooth and Algebra.isOpen_smoothLocus.

Stacks Tag 00TB

Equations

• Algebra.IsSmoothAt R p = Algebra.FormallySmooth R (Localization.AtPrime p)

def Algebra.smoothLocus (R A : Type u) [CommRing R] [CommRing A] [Algebra R A] : Set (PrimeSpectrum A)

Algebra.smoothLocus R A is the set of primes p of A such that Aₚ is formally smooth over R.

Equations

• Algebra.smoothLocus R A = {p : PrimeSpectrum A | Algebra.IsSmoothAt R p.asIdeal}

theorem Algebra.smoothLocus_eq_compl_support_inter {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [EssFiniteType R A] : smoothLocus R A = (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A (Ω[A⁄R])

theorem Algebra.basicOpen_subset_smoothLocus_iff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] {f : A} : ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ FormallySmooth R (Localization.Away f)

theorem Algebra.basicOpen_subset_smoothLocus_iff_smooth {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] {f : A} : ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ Smooth R (Localization.Away f)

theorem Algebra.smoothLocus_eq_univ_iff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] : smoothLocus R A = Set.univ ↔ FormallySmooth R A

theorem Algebra.smoothLocus_comap_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {Af : Type u} [CommRing Af] [Algebra A Af] [Algebra R Af] [IsScalarTower R A Af] (f : A) [IsLocalization.Away f Af] : ⇑(PrimeSpectrum.comap (algebraMap A Af)) ⁻¹' smoothLocus R A = smoothLocus R Af

theorem Algebra.isOpen_smoothLocus {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] : IsOpen (smoothLocus R A)