# Integral closure as a characteristic predicate #

We prove basic properties of IsIntegralClosure.

theorem IsIntegral.isUnit {R : Type u_1} {S : Type u_2} [Field R] [Ring S] [IsDomain S] [Algebra R S] {x : S} (int : IsIntegral R x) (h0 : x ≠ 0) :

IsUnit x

A nonzero element in a domain integral over a field is a unit.

source

theorem isField_of_isIntegral_of_isField' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] [Algebra.IsIntegral R S] (hR : IsField R) :

IsField S

A commutative domain that is an integral algebra over a field is a field.

source

theorem IsIntegral.inv_mem_adjoin {R : Type u_1} {S : Type u_2} [Field R] [DivisionRing S] [Algebra R S] {x : S} (int : IsIntegral R x) :

x⁻¹ ∈ Algebra.adjoin R {x}

source

theorem IsIntegral.inv_mem {R : Type u_1} {S : Type u_2} [Field R] [DivisionRing S] [Algebra R S] {x : S} {A : Subalgebra R S} (int : IsIntegral R x) (hx : x ∈ A) :

x⁻¹ ∈ A

The inverse of an integral element in a subalgebra of a division ring over a field also lies in that subalgebra.

source

theorem Algebra.IsIntegral.inv_mem {R : Type u_1} {S : Type u_2} [Field R] [DivisionRing S] [Algebra R S] {x : S} {A : Subalgebra R S} [Algebra.IsIntegral R ↥A] (hx : x ∈ A) :

x⁻¹ ∈ A

An integral subalgebra of a division ring over a field is closed under inverses.

source

theorem IsIntegral.inv {R : Type u_1} {S : Type u_2} [Field R] [DivisionRing S] [Algebra R S] {x : S} (int : IsIntegral R x) :

IsIntegral R x⁻¹

The inverse of an integral element in a division ring over a field is also integral.

source

theorem IsIntegral.mem_of_inv_mem {R : Type u_1} {S : Type u_2} [Field R] [DivisionRing S] [Algebra R S] {x : S} {A : Subalgebra R S} (int : IsIntegral R x) (inv_mem : x⁻¹ ∈ A) :

x ∈ A

source

theorem Algebra.IsIntegral.finite {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Algebra.IsIntegral R A] [h' : Algebra.FiniteType R A] :

Module.Finite R A

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.

source

theorem Algebra.finite_iff_isIntegral_and_finiteType {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :

Module.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A

finite = integral + finite type

source

theorem RingHom.IsIntegral.to_finite {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (h : f.IsIntegral) (h' : f.FiniteType) :

f.Finite

source

theorem RingHom.Finite.of_isIntegral_of_finiteType {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (h : f.IsIntegral) (h' : f.FiniteType) :

f.Finite

Alias of RingHom.IsIntegral.to_finite.

source

theorem RingHom.finite_iff_isIntegral_and_finiteType {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} :

f.Finite ↔ f.IsIntegral ∧ f.FiniteType

finite = integral + finite type

source

theorem mem_integralClosure_iff_mem_fg (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] {r : A} :

r ∈ integralClosure R A ↔ ∃ (M : Subalgebra R A), (Subalgebra.toSubmodule M).FG ∧ r ∈ M

source

theorem adjoin_le_integralClosure {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} (hx : IsIntegral R x) :

Algebra.adjoin R {x} ≤ integralClosure R A

source

theorem le_integralClosure_iff_isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Subalgebra R A} :

S ≤ integralClosure R A ↔ Algebra.IsIntegral R ↥S

source

theorem Algebra.IsIntegral.adjoin {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Set A} (hS : ∀ x ∈ S, IsIntegral R x) :

Algebra.IsIntegral R ↥(Algebra.adjoin R S)

source

theorem integralClosure_eq_top_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :

integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A

source

theorem Algebra.isIntegral_sup {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S T : Subalgebra R A} :

Algebra.IsIntegral R ↥(S ⊔ T) ↔ Algebra.IsIntegral R ↥S ∧ Algebra.IsIntegral R ↥T

source

theorem Algebra.isIntegral_iSup {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {ι : Sort u_5} (S : ι → Subalgebra R A) :

Algebra.IsIntegral R ↥(iSup S) ↔ ∀ (i : ι), Algebra.IsIntegral R ↥(S i)

source

theorem integralClosure_map_algEquiv {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) :

Subalgebra.map (↑f) (integralClosure R A) = integralClosure R S

Mapping an integral closure along an AlgEquiv gives the integral closure.

source

def AlgHom.mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A →ₐ[R] S) :

↥(integralClosure R A) →ₐ[R] ↥(integralClosure R S)

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

source

@[simp]

theorem AlgHom.coe_mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A →ₐ[R] S) (x : ↥(integralClosure R A)) :

↑(f.mapIntegralClosure x) = f ↑x

source

def AlgEquiv.mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) :

↥(integralClosure R A) ≃ₐ[R] ↥(integralClosure R S)

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

source

@[simp]

theorem AlgEquiv.coe_mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) (x : ↥(integralClosure R A)) :

↑(f.mapIntegralClosure x) = f ↑x

source

theorem integralClosure.isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (x : ↥(integralClosure R A)) :

IsIntegral R x

source

instance integralClosure.AlgebraIsIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :

Algebra.IsIntegral R ↥(integralClosure R A)

Equations

⋯ = ⋯

source

theorem IsIntegral.of_mul_unit {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x y : B} {r : R} (hr : (algebraMap R B) r * y = 1) (hx : IsIntegral R (x * y)) :

IsIntegral R x

source

theorem RingHom.IsIntegralElem.of_mul_unit {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (x y : S) (r : R) (hr : f r * y = 1) (hx : f.IsIntegralElem (x * y)) :

f.IsIntegralElem x

source

theorem IsIntegral.of_mem_closure' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (G : Set A) (hG : ∀ x ∈ G, IsIntegral R x) (x : A) :

x ∈ Subring.closure G → IsIntegral R x

Generalization of IsIntegral.of_mem_closure bootstrapped up from that lemma

source

theorem IsIntegral.of_mem_closure'' {R : Type u_1} [CommRing R] {S : Type u_5} [CommRing S] {f : R →+* S} (G : Set S) (hG : ∀ x ∈ G, f.IsIntegralElem x) (x : S) :

x ∈ Subring.closure G → f.IsIntegralElem x

source

theorem IsIntegral.pow {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} (h : IsIntegral R x) (n : ℕ) :

IsIntegral R (x ^ n)

source

theorem IsIntegral.nsmul {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} (h : IsIntegral R x) (n : ℕ) :

IsIntegral R (n • x)

source

theorem IsIntegral.zsmul {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} (h : IsIntegral R x) (n : ℤ) :

IsIntegral R (n • x)

source

theorem IsIntegral.multiset_prod {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) :

IsIntegral R s.prod

source

theorem IsIntegral.multiset_sum {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) :

IsIntegral R s.sum

source

theorem IsIntegral.prod {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {α : Type u_5} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) :

IsIntegral R (∏ x ∈ s, f x)

source

theorem IsIntegral.sum {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {α : Type u_5} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) :

IsIntegral R (∑ x ∈ s, f x)

source

theorem IsIntegral.det {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {n : Type u_5} [Fintype n] [DecidableEq n] {M : Matrix n n A} (h : ∀ (i j : n), IsIntegral R (M i j)) :

IsIntegral R M.det

source

@[simp]

theorem IsIntegral.pow_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {n : ℕ} (hn : 0 < n) :

IsIntegral R (x ^ n) ↔ IsIntegral R x

source

theorem IsIntegral.tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Ring B] [Algebra R A] [Algebra R B] (x : A) {y : B} (h : IsIntegral R y) :

IsIntegral A (x ⊗ₜ[R] y)

source

@[deprecated Polynomial.integralNormalization]

def normalizeScaleRoots {R : Type u} [Semiring R] (p : Polynomial R) :

Polynomial R

The monic polynomial whose roots are p.leadingCoeff * x for roots x of p.

Equations

@normalizeScaleRoots = @Polynomial.integralNormalization

Instances For

source

@[deprecated Polynomial.integralNormalization_coeff_mul_leadingCoeff_pow]

theorem normalizeScaleRoots_coeff_mul_leadingCoeff_pow {R : Type u} [Semiring R] {p : Polynomial R} (i : ℕ) (hp : 1 ≤ p.natDegree) :

p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Alias of Polynomial.integralNormalization_coeff_mul_leadingCoeff_pow.

source

@[deprecated Polynomial.leadingCoeff_smul_integralNormalization]

theorem leadingCoeff_smul_normalizeScaleRoots {S : Type v} [CommSemiring S] (p : Polynomial S) :

p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff

Alias of Polynomial.leadingCoeff_smul_integralNormalization.

source

@[deprecated Polynomial.support_integralNormalization_subset]

theorem normalizeScaleRoots_support {R : Type u} [Semiring R] {p : Polynomial R} :

p.integralNormalization.support ⊆ p.support

Alias of Polynomial.support_integralNormalization_subset.

source

@[deprecated Polynomial.integralNormalization_degree]

theorem normalizeScaleRoots_degree {R : Type u} [Semiring R] {p : Polynomial R} :

p.integralNormalization.degree = p.degree

Alias of Polynomial.integralNormalization_degree.

source

@[deprecated Polynomial.integralNormalization_eval₂_leadingCoeff_mul]

theorem normalizeScaleRoots_eval₂_leadingCoeff_mul {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) :

Polynomial.eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p

Alias of Polynomial.integralNormalization_eval₂_leadingCoeff_mul.

source

@[deprecated Polynomial.monic_integralNormalization]

theorem normalizeScaleRoots_monic {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) :

p.integralNormalization.Monic

Alias of Polynomial.monic_integralNormalization.

source

theorem RingHom.isIntegralElem_leadingCoeff_mul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (p : Polynomial R) (x : S) (h : Polynomial.eval₂ f x p = 0) :

f.IsIntegralElem (f p.leadingCoeff * x)

Given a p : R[X] and a x : S such that p.eval₂ f x = 0, f p.leadingCoeff * x is integral.

source

theorem isIntegral_leadingCoeff_smul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (p : Polynomial R) (x : S) [Algebra R S] (h : (Polynomial.aeval x) p = 0) :

IsIntegral R (p.leadingCoeff • x)

Given a p : R[X] and a root x : S, then p.leadingCoeff • x : S is integral over R.

source

theorem Polynomial.Monic.quotient_isIntegralElem {S : Type u_4} [CommRing S] {g : Polynomial S} (mon : g.Monic) {I : Ideal (Polynomial S)} (h : g ∈ I) :

((Ideal.Quotient.mk I).comp (algebraMap S (Polynomial S))).IsIntegralElem ((Ideal.Quotient.mk I) Polynomial.X)

source

theorem Polynomial.Monic.quotient_isIntegral {S : Type u_4} [CommRing S] {g : Polynomial S} (mon : g.Monic) {I : Ideal (Polynomial S)} (h : g ∈ I) :

((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S (Polynomial S))).IsIntegral

source

instance integralClosure.isIntegralClosure (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] :

IsIntegralClosure (↥(integralClosure R A)) R A

Equations

⋯ = ⋯

source

theorem IsIntegralClosure.algebraMap_injective (A : Type u_1) (R : Type u_2) (B : Type u_3) [CommRing R] [CommSemiring A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] :

Function.Injective ⇑(algebraMap A B)

source

theorem IsIntegralClosure.isIntegral (R : Type u_1) {A : Type u_2} (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] (x : A) :

IsIntegral R x

source

theorem IsIntegralClosure.isIntegral_algebra (R : Type u_1) {A : Type u_2} (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] :

Algebra.IsIntegral R A

source

theorem IsIntegralClosure.noZeroSMulDivisors (R : Type u_1) {A : Type u_2} (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] [NoZeroSMulDivisors R B] :

NoZeroSMulDivisors R A

source

noncomputable def IsIntegralClosure.mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x) :

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

source

@[simp]

theorem IsIntegralClosure.algebraMap_mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x) :

(algebraMap A B) (IsIntegralClosure.mk' A x hx) = x

source

@[simp]

theorem IsIntegralClosure.mk'_one {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (h : IsIntegral R 1 := ⋯) :

IsIntegralClosure.mk' A 1 h = 1

source

@[simp]

theorem IsIntegralClosure.mk'_zero {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (h : IsIntegral R 0 := ⋯) :

IsIntegralClosure.mk' A 0 h = 0

source

theorem IsIntegralClosure.mk'_add {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :

IsIntegralClosure.mk' A (x + y) ⋯ = IsIntegralClosure.mk' A x hx + IsIntegralClosure.mk' A y hy

source

theorem IsIntegralClosure.mk'_mul {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :

IsIntegralClosure.mk' A (x * y) ⋯ = IsIntegralClosure.mk' A x hx * IsIntegralClosure.mk' A y hy

source

@[simp]

theorem IsIntegralClosure.mk'_algebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] (x : R) (h : IsIntegral R ((algebraMap R B) x) := ⋯) :

IsIntegralClosure.mk' A ((algebraMap R B) x) h = (algebraMap R A) x

source

theorem IsIntegralClosure.isField {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] [IsDomain A] (hR : IsField R) :

IsField A

The integral closure of a field in a commutative domain is always a field.

source

noncomputable def IsIntegralClosure.lift (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] {S : Type u_4} [CommRing S] [Algebra R S] [Algebra S B] [IsScalarTower R S B] [Algebra R A] [IsScalarTower R A B] [isIntegral : Algebra.IsIntegral R S] :

S →ₐ[R] A

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

source

@[simp]

theorem IsIntegralClosure.algebraMap_lift (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] {S : Type u_4} [CommRing S] [Algebra R S] [Algebra S B] [IsScalarTower R S B] [Algebra R A] [IsScalarTower R A B] [isIntegral : Algebra.IsIntegral R S] (x : S) :

(algebraMap A B) ((IsIntegralClosure.lift R A B) x) = (algebraMap S B) x

source

noncomputable def IsIntegralClosure.equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (A' : Type u_4) [CommRing A'] [Algebra A' B] [IsIntegralClosure A' R B] [Algebra R A] [Algebra R A'] [IsScalarTower R A B] [IsScalarTower R A' B] :

A ≃ₐ[R] A'

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

source

@[simp]

theorem IsIntegralClosure.algebraMap_equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (A' : Type u_4) [CommRing A'] [Algebra A' B] [IsIntegralClosure A' R B] [Algebra R A] [Algebra R A'] [IsScalarTower R A B] [IsScalarTower R A' B] (x : A) :

(algebraMap A' B) ((IsIntegralClosure.equiv R A B A') x) = (algebraMap A B) x

source

theorem isIntegral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] [Algebra.IsIntegral R A] (x : B) (hx : IsIntegral A x) :

IsIntegral R x

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.

source

theorem Algebra.IsIntegral.trans {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] [Algebra.IsIntegral R A] [Algebra.IsIntegral A B] :

Algebra.IsIntegral R B

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.

source

theorem RingHom.IsIntegral.trans {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (hf : f.IsIntegral) (hg : g.IsIntegral) :

(g.comp f).IsIntegral

source

theorem IsIntegralClosure.tower_top {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_6} {C : Type u_7} [CommRing C] [CommRing B] [Algebra R B] [Algebra A B] [Algebra C B] [IsScalarTower R A B] [IsIntegralClosure C R B] [Algebra.IsIntegral R A] :

IsIntegralClosure C A B

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.

source

theorem RingHom.isIntegral_of_surjective {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) :

f.IsIntegral

source

theorem Algebra.isIntegral_of_surjective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (h : Function.Surjective ⇑(algebraMap R A)) :

Algebra.IsIntegral R A

source

theorem IsIntegral.tower_bot {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] (H : Function.Injective ⇑(algebraMap A B)) {x : A} (h : IsIntegral R ((algebraMap A B) x)) :

IsIntegral R x

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

source

theorem RingHom.IsIntegral.tower_bot {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (hg : Function.Injective ⇑g) (hfg : (g.comp f).IsIntegral) :

f.IsIntegral

source

theorem Algebra.IsIntegral.tower_bot {R : Type u_1} {S : Type u_4} (T : Type u_5) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [NoZeroSMulDivisors S T] [Nontrivial T] [IsScalarTower R S T] [h : Algebra.IsIntegral R T] :

Algebra.IsIntegral R S

Let T / S / R be a tower of algebras, T is non-trivial and is a torsion free S-module, then if T is an integral R-algebra, then S is an integral R-algebra.

source

theorem IsIntegral.tower_bot_of_field {R : Type u_6} {A : Type u_7} {B : Type u_8} [CommRing R] [Field A] [CommRing B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} (h : IsIntegral R ((algebraMap A B) x)) :

IsIntegral R x

source

theorem RingHom.isIntegralElem.of_comp {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) {x : T} (h : (g.comp f).IsIntegralElem x) :

g.IsIntegralElem x

source

theorem RingHom.IsIntegral.tower_top {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (h : (g.comp f).IsIntegral) :

g.IsIntegral

source

theorem Algebra.IsIntegral.tower_top (R : Type u_1) {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [h : Algebra.IsIntegral R T] :

Algebra.IsIntegral S T

Let T / S / R be a tower of algebras, T is an integral R-algebra, then it is integral as an S-algebra.

source

theorem RingHom.IsIntegral.quotient {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal S} (hf : f.IsIntegral) :

(Ideal.quotientMap I f ⋯).IsIntegral

source

instance instIsIntegralQuotientIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {I : Ideal A} [Algebra.IsIntegral R A] :

Algebra.IsIntegral R (A ⧸ I)

Equations

⋯ = ⋯

source

instance Algebra.IsIntegral.quotient {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {I : Ideal A} [Algebra.IsIntegral R A] :

Algebra.IsIntegral (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I)

Equations

⋯ = ⋯

source

theorem isIntegral_quotientMap_iff {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal S} :

(Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

source

theorem isField_of_isIntegral_of_isField {R : Type u_6} {S : Type u_7} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (hRS : Function.Injective ⇑(algebraMap R S)) (hS : IsField S) :

IsField R

If the integral extension R → S is injective, and S is a field, then R is also a field.

source

theorem Algebra.IsIntegral.isField_iff_isField {R : Type u_6} {S : Type u_7} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] [Algebra.IsIntegral R S] (hRS : Function.Injective ⇑(algebraMap R S)) :

IsField R ↔ IsField S

source

theorem integralClosure_idem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :

integralClosure (↥(integralClosure R A)) A = ⊥

source

instance instIsDomainSubtypeMemSubalgebraIntegralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] :

IsDomain ↥(integralClosure R S)

Equations

⋯ = ⋯

source

theorem roots_mem_integralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {f : Polynomial R} (hf : f.Monic) {a : S} (ha : a ∈ f.aroots S) :

a ∈ integralClosure R S

HepLean Documentation

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

# Integral closure as a characteristic predicate #