Integrally closed rings #
An integrally closed ring R
contains all the elements of Frac(R)
that are
integral over R
. A special case of integrally closed rings are the Dedekind domains.
Main definitions #
IsIntegrallyClosedIn R A
statesR
contains all integral elements ofA
IsIntegrallyClosed R
statesR
contains all integral elements ofFrac(R)
Main results #
isIntegrallyClosed_iff K
, whereK
is a fraction field ofR
, statesR
is integrally closed iff it is the integral closure ofR
inK
TODO Related notions #
The following definitions are closely related, especially in their applications in Mathlib.
A normal domain is a domain that is integrally closed in its field of fractions.
Stacks: normal domain
Normal domains are the major use case of IsIntegrallyClosed
at the time of writing, and we have
quite a few results that can be moved wholesale to a new NormalDomain
definition.
In fact, before PR #6126 IsIntegrallyClosed
was exactly defined to be a normal domain.
(So you might want to copy some of its API when you define normal domains.)
A normal ring means that localizations at all prime ideals are normal domains.
Stacks: normal ring
This implies IsIntegrallyClosed
,
Stacks: Tag 034M
but is equivalent to it only under some conditions (reduced + finitely many minimal primes),
Stacks: Tag 030C
in which case it's also equivalent to being a finite product of normal domains.
We'd need to add these conditions if we want exactly the products of Dedekind domains.
In fact noetherianity is sufficient to guarantee finitely many minimal primes, so IsDedekindRing
could be defined as IsReduced
, IsNoetherian
, Ring.DimensionLEOne
, and either
IsIntegrallyClosed
or NormalDomain
. If we use NormalDomain
then IsReduced
is automatic,
but we could also consider a version of NormalDomain
that only requires the localizations are
IsIntegrallyClosed
but may not be domains, and that may not equivalent to the ring itself being
IsIntegallyClosed
(even for noetherian rings?).
R
is integrally closed in A
if all integral elements of A
are also elements of R
.
Equations
- IsIntegrallyClosedIn R A = IsIntegralClosure R R A
Instances For
R
is integrally closed if all integral elements of Frac(R)
are also elements of R
.
This definition uses FractionRing R
to denote Frac(R)
. See isIntegrallyClosed_iff
if you want to choose another field of fractions for R
.
Equations
Instances For
Being integrally closed is preserved under injective algebra homomorphisms.
R
is integrally closed iff it is the integral closure of itself in its field of fractions.
R
is integrally closed iff it is the integral closure of itself in its field of fractions.
R
is integrally closed in A
iff all integral elements of A
are also elements of R
.
R
is integrally closed iff all integral elements of its fraction field K
are also elements of R
.
If R
is the integral closure of S
in A
, then it is integrally closed in A
.
Note that this is not a duplicate instance, since IsIntegrallyClosed R
is instead defined
as IsIntegrallyClosed R R (FractionRing R)
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
This is almost a duplicate of IsIntegrallyClosedIn.integralClosure_eq_bot
,
except the NoZeroSMulDivisors
hypothesis isn't inferred automatically from IsFractionRing
.
Any field is integral closed.
Equations
- ⋯ = ⋯