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.

@[reducible, inline]

abbrev Algebra.IsUnramifiedAt (R : Type u_1) {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (q : Ideal A) [q.IsPrime] : Prop

We say that an R-algebra A is unramified at a prime q of A if A_q is formally unramified over R.

If A is of finite type over R and q is lying over p, then this is equivalent to κ(q)/κ(p) being separable and pA_q = qA_q. See Algebra.isUnramifiedAt_iff_map_eq in RingTheory.Unramified.LocalRing

Equations

• Algebra.IsUnramifiedAt R q = Algebra.FormallyUnramified R (Localization.AtPrime q)

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

Algebra.unramifiedLocus R A is the set of primes p of A that are unramified.

Equations

• Algebra.unramifiedLocus R A = {p : PrimeSpectrum A | Algebra.IsUnramifiedAt R p.asIdeal}

theorem Algebra.IsUnramifiedAt.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [p.IsPrime] [P.IsPrime] [IsUnramifiedAt R p] [IsUnramifiedAt A P] : IsUnramifiedAt R P

theorem Algebra.IsUnramifiedAt.of_restrictScalars (R : Type u_1) {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (P : Ideal B) [P.IsPrime] [IsUnramifiedAt R P] : IsUnramifiedAt A P

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)