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.
• Algebra.IsUnramifiedIn : A prime 𝔭 of R is unramified in A if every prime of A lying over 𝔭 is unramified.

@[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

instance Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAtOfIsScalarTower {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] [IsUnramifiedAt R q] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime 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).

def Algebra.IsUnramifiedIn {R : Type u_1} [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] (𝔭 : Ideal R) : Prop

A prime 𝔭 of R is unramified in A if every prime ideal 𝔓 of A lying over 𝔭 is unramified.

Equations

• Algebra.IsUnramifiedIn A 𝔭 = ∀ (𝔓 : Ideal A) (x : 𝔓.IsPrime), 𝔓.LiesOver 𝔭 → Algebra.IsUnramifiedAt R 𝔓

theorem Algebra.isUnramifiedIn_top {R : Type u_1} [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] : IsUnramifiedIn A ⊤

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.formallyUnramified_iff_forall {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] : FormallyUnramified R A ↔ ∀ (q : PrimeSpectrum A), IsUnramifiedAt R q.asIdeal

theorem Algebra.unramified_iff_forall {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FiniteType R A] : Unramified R A ↔ ∀ (q : PrimeSpectrum A), IsUnramifiedAt R q.asIdeal

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)