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

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.

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

instance Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAt {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p] [IsUnramifiedAt R q] : FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)

theorem Algebra.IsUnramifiedAt.residueField {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (P : Ideal R) [P.IsPrime] (Q : Ideal A) [Q.IsPrime] [Q.LiesOver P] [IsUnramifiedAt R Q] (Q' : Ideal (P.Fiber A)) [Q'.IsPrime] (hQ' : Q = Ideal.comap TensorProduct.includeRight.toRingHom Q') : IsUnramifiedAt P.ResidueField Q'

If A is an R-algebra unramified at Q, P is the prime of R lying under Q, then κ(P) ⊗ A is unramified at Q' (the prime corresponding to Q) over κ(P).

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

theorem Algebra.basicOpen_subset_unramifiedLocus_iff {R : Type u_1} {A : Type u_2} [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 : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] : unramifiedLocus R A = Set.univ ↔ FormallyUnramified R A

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

theorem Algebra.exists_formallyUnramified_of_isUnramifiedAt {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [EssFiniteType R A] (p : Ideal A) [p.IsPrime] [IsUnramifiedAt R p] : ∃ f ∉ p, FormallyUnramified R (Localization.Away f)

theorem Algebra.exists_unramified_of_isUnramifiedAt {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FiniteType R A] (p : Ideal A) [p.IsPrime] [IsUnramifiedAt R p] : ∃ f ∉ p, Unramified R (Localization.Away f)