# Integral closure as a characteristic predicate #
We prove basic properties of IsIntegralClosure
.
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
.
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
.
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.