Documentation

Mathlib.RingTheory.Unramified.Locus

Unramified locus of an algebra #

Main results #

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

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
Instances For

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

    Equations
    Instances For