Integral closure of a subring. #
If A is an R-algebra then a : A
is integral over R if it is a root of a monic polynomial
with coefficients in R. Enough theory is developed to prove that integral elements
form a sub-R-algebra of A.
Main definitions #
Let R
be a CommRing
and let A
be an R-algebra.
RingHom.IsIntegralElem (f : R →+* A) (x : A)
:x
is integral with respect to the mapf
,IsIntegral (x : A)
:x
is integral overR
, i.e., is a root of a monic polynomial with coefficients inR
.integralClosure R A
: the integral closure ofR
inA
, regarded as a sub-R
-algebra ofA
.
An element x
of A
is said to be integral over R
with respect to f
if it is a root of a monic polynomial p : R[X]
evaluated under f
Equations
- f.IsIntegralElem x = ∃ (p : Polynomial R), p.Monic ∧ Polynomial.eval₂ f x p = 0
Instances For
An element x
of an algebra A
over a commutative ring R
is said to be integral,
if it is a root of some monic polynomial p : R[X]
.
Equivalently, the element is integral over R
with respect to the induced algebraMap
Equations
- IsIntegral R x = (algebraMap R A).IsIntegralElem x
Instances For
An algebra is integral if every element of the extension is integral over the base ring
- isIntegral : ∀ (x : A), IsIntegral R x
Instances
If R → A → B
is an algebra tower,
then if the entire tower is an integral extension so is A → B
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If S
is a sub-R
-algebra of A
and S
is finitely-generated as an R
-module,
then all elements of S
are integral over R
.
Suppose A
is an R
-algebra, M
is an A
-module such that a • m ≠ 0
for all non-zero a
and m
. If x : A
fixes a nontrivial f.g. R
-submodule N
of M
, then x
is R
-integral.
Alias of RingHom.Finite.to_isIntegral
.
The Kurosh problem asks to show that
this is still true when A
is not necessarily commutative and R
is a field, but it has
been solved in the negative. See https://arxiv.org/pdf/1706.02383.pdf for criteria for a
finitely generated algebraic (= integral) algebra over a field to be finite dimensional.
This could be an instance
, but we tend to go from Module.Finite
to IsIntegral
/IsAlgebraic
,
and making it an instance will cause the search to be complicated a lot.
finite = integral + finite type
Alias of RingHom.IsIntegral.to_finite
.
The integral closure of R in an R-algebra A.
Equations
- integralClosure R A = { carrier := {r : A | IsIntegral R r}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
Instances For
Mapping an integral closure along an AlgEquiv
gives the integral closure.
An AlgHom
between two rings restrict to an AlgHom
between the integral closures inside
them.
Equations
- f.mapIntegralClosure = (AlgHom.restrictDomain (↥(integralClosure R A)) f).codRestrict (integralClosure R S) ⋯
Instances For
An AlgEquiv
between two rings restrict to an AlgEquiv
between the integral closures inside
them.
Equations
- f.mapIntegralClosure = AlgEquiv.ofAlgHom (↑f).mapIntegralClosure (↑f.symm).mapIntegralClosure ⋯ ⋯
Instances For
Equations
- ⋯ = ⋯
Generalization of IsIntegral.of_mem_closure
bootstrapped up from that lemma
The monic polynomial whose roots are p.leadingCoeff * x
for roots x
of p
.
Equations
- normalizeScaleRoots p = ∑ i ∈ p.support, (Polynomial.monomial i) (if i = p.natDegree then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i))
Instances For
Given a p : R[X]
and a x : S
such that p.eval₂ f x = 0
,
f p.leadingCoeff * x
is integral.
Given a p : R[X]
and a root x : S
,
then p.leadingCoeff • x : S
is integral over R
.
IsIntegralClosure A R B
is the characteristic predicate stating A
is
the integral closure of R
in B
,
i.e. that an element of B
is integral over R
iff it is an element of (the image of) A
.
- algebraMap_injective' : Function.Injective ⇑(algebraMap A B)
- isIntegral_iff : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : A), (algebraMap A B) y = x
Instances
Equations
- ⋯ = ⋯
If x : B
is integral over R
, then it is an element of the integral closure of R
in B
.
Equations
- IsIntegralClosure.mk' A x hx = Classical.choose ⋯
Instances For
If B / S / R
is a tower of ring extensions where S
is integral over R
,
then S
maps (uniquely) into an integral closure B / A / R
.
Equations
- IsIntegralClosure.lift R A B = { toFun := fun (x : S) => IsIntegralClosure.mk' A ((algebraMap S B) x) ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
Integral closures are all isomorphic to each other.
Equations
- IsIntegralClosure.equiv R A B A' = AlgEquiv.ofAlgHom (IsIntegralClosure.lift R A' B) (IsIntegralClosure.lift R A B) ⋯ ⋯
Instances For
If A is an R-algebra all of whose elements are integral over R, and x is an element of an A-algebra that is integral over A, then x is integral over R.
If A is an R-algebra all of whose elements are integral over R, and B is an A-algebra all of whose elements are integral over A, then all elements of B are integral over R.
If R → A → B
is an algebra tower, C
is the integral closure of R
in B
and A
is integral over R
, then C
is the integral closure of A
in B
.
If R → A → B
is an algebra tower with A → B
injective,
then if the entire tower is an integral extension so is R → A
Equations
- ⋯ = ⋯
If the integral extension R → S
is injective, and S
is a field, then R
is also a field.