Unramified locus of an algebra

Main results

• Algebra.unramifiedLocus : The set of primes that is unramified over the base.
• Algebra.basicOpen_subset_unramifiedLocus_iff : D(f) is contained in the unramified locus if and only if A_f is unramified over R.
• Algebra.unramifiedLocus_eq_univ_iff : The unramified locus is the whole spectrum if and only if A is unramified over R.
• Algebra.isOpen_unramifiedLocus : If A is (essentially) of finite type over R, then the unramified locus is open.

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

Algebra.unramifiedLocus R A is the set of primes p of A such that Aₚ is formally unramified over R.

Equations

• Algebra.unramifiedLocus R A = {p : PrimeSpectrum A | Algebra.FormallyUnramified R (Localization.AtPrime p.asIdeal)}

theorem Algebra.unramifiedLocus_eq_compl_support {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : unramifiedLocus R A = (Module.support A (Ω[A⁄R]))ᶜ

theorem Algebra.basicOpen_subset_unramifiedLocus_iff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {f : A} : ↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔ FormallyUnramified R (Localization.Away f)

theorem Algebra.unramifiedLocus_eq_univ_iff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : unramifiedLocus R A = Set.univ ↔ FormallyUnramified R A

theorem Algebra.isOpen_unramifiedLocus {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [EssFiniteType R A] : IsOpen (unramifiedLocus R A)