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 ifA_f
is unramified overR
.Algebra.unramifiedLocus_eq_univ_iff
: The unramified locus is the whole spectrum if and only ifA
is unramified overR
.Algebra.isOpen_unramifiedLocus
: IfA
is (essentially) of finite type overR
, 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]
:
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
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
that are unramified.
Equations
- Algebra.unramifiedLocus R A = {p : PrimeSpectrum A | Algebra.IsUnramifiedAt R p.asIdeal}
Instances For
theorem
Algebra.unramifiedLocus_eq_compl_support
{R A : Type u}
[CommRing R]
[CommRing A]
[Algebra R A]
:
theorem
Algebra.basicOpen_subset_unramifiedLocus_iff
{R A : Type u}
[CommRing R]
[CommRing A]
[Algebra R A]
{f : A}
:
theorem
Algebra.unramifiedLocus_eq_univ_iff
{R A : Type u}
[CommRing R]
[CommRing A]
[Algebra R A]
:
theorem
Algebra.isOpen_unramifiedLocus
{R A : Type u}
[CommRing R]
[CommRing A]
[Algebra R A]
[EssFiniteType R A]
:
IsOpen (unramifiedLocus R A)