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_1) {A : Type u_2} [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.

Equations

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

def Algebra.smoothLocus (R : Type u_1) (A : Type u_2) [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 : Type u_1} {A : Type u_2} [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 : Type u_1} {A : Type u_2} [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 : Type u_1} {A : Type u_2} [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 : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] : smoothLocus R A = Set.univ ↔ FormallySmooth R A

theorem Algebra.smoothLocus_eq_univ {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Smooth R A] : smoothLocus R A = Set.univ

theorem Algebra.smoothLocus_comap_of_isLocalization {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {Af : Type u_3} [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 : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] : IsOpen (smoothLocus R A)

theorem Algebra.IsSmoothAt.exists_notMem_smooth (R : Type u_1) {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] (p : Ideal A) [p.IsPrime] [IsSmoothAt R p] : ∃ f ∉ p, Smooth R (Localization.Away f)