Algebraic elements and integral elements #

This file relates algebraic and integral elements of an algebra, by proving every integral element is algebraic and that every algebraic element over a field is integral.

Main results #

IsIntegral.isAlgebraic, Algebra.IsIntegral.isAlgebraic: integral implies algebraic.
isAlgebraic_iff_isIntegral, Algebra.isAlgebraic_iff_isIntegral: integral iff algebraic over a field.
IsAlgebraic.of_finite, Algebra.IsAlgebraic.of_finite: finite-dimensional (as module) implies algebraic.
IsAlgebraic.exists_integral_multiple: an algebraic element has a multiple which is integral
IsAlgebraic.iff_exists_smul_integral: If R is reduced and S is an R-algebra with injective algebraMap, then an element of S is algebraic over R iff some R-multiple is integral over R.
Algebra.IsAlgebraic.trans': If A/S/R is a tower of algebras and both A/S and S/R are algebraic, then A/R is also algebraic, provided that S has no zero divisors and algebraMap S A is injective (so S can be regarded as an R-subalgebra of A).
Subalgebra.algebraicClosure: If R is a domain and S is an arbitrary R-algebra, then the elements of S that are algebraic over R form a subalgebra.
Transcendental.extendScalars: an element of an R-algebra that is transcendental over R remains transcendental over any algebraic R-subalgebra that has no zero divisors.

source

theorem IsIntegral.isAlgebraic {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] {x : A} :

IsIntegral R x → IsAlgebraic R x

An integral element of an algebra is algebraic.

source

instance Algebra.IsIntegral.isAlgebraic {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] [Algebra.IsIntegral R A] :

Algebra.IsAlgebraic R A

source

theorem isAlgebraic_iff_isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] {x : A} :

IsAlgebraic K x ↔ IsIntegral K x

An element of an algebra over a field is algebraic if and only if it is integral.

source

theorem Algebra.isAlgebraic_iff_isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] :

Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A

source

theorem IsAlgebraic.isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] {x : A} :

IsAlgebraic K x → IsIntegral K x

Alias of the forward direction of isAlgebraic_iff_isIntegral.

An element of an algebra over a field is algebraic if and only if it is integral.

source

instance Algebra.IsAlgebraic.isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] [Algebra.IsAlgebraic K A] :

Algebra.IsIntegral K A

This used to be an alias of Algebra.isAlgebraic_iff_isIntegral but that would make Algebra.IsAlgebraic K A an explicit parameter instead of instance implicit.

source

theorem Algebra.IsAlgebraic.of_isIntegralClosure (R : Type u_1) (B : Type u_2) (C : Type u_3) [CommRing R] [Nontrivial R] [CommRing B] [CommRing C] [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C] [IsIntegralClosure B R C] :

Algebra.IsAlgebraic R B

source

theorem IsAlgebraic.of_finite (K : Type u_1) {A : Type u_5} [Field K] [Ring A] [Algebra K A] (e : A) [FiniteDimensional K A] :

IsAlgebraic K e

source

instance Algebra.IsAlgebraic.of_finite (K : Type u_1) (A : Type u_5) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] :

Algebra.IsAlgebraic K A

A field extension is algebraic if it is finite.

Stacks Tag 09GG (first part)

source

theorem Algebra.IsAlgebraic.trans {K : Type u_1} {L : Type u_2} {A : Type u_5} [Field K] [Field L] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] [L_alg : Algebra.IsAlgebraic K L] [A_alg : Algebra.IsAlgebraic L A] :

Algebra.IsAlgebraic K A

If L is an algebraic field extension of K and A is an algebraic algebra over L, then A is algebraic over K.

Stacks Tag 09GJ

source

@[simp]

theorem transcendental_aeval_iff {K : Type u_1} {A : Type u_5} [Field K] [Ring A] [Algebra K A] {r : A} {f : Polynomial K} :

Transcendental K ((Polynomial.aeval r) f) ↔ Transcendental K r ∧ Transcendental K f

If K is a field, r : A and f : K[X], then Polynomial.aeval r f is transcendental over K if and only if r and f are both transcendental over K. See also Transcendental.aeval_of_transcendental and Transcendental.of_aeval.

source

theorem AlgHom.bijective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (ϕ : L →ₐ[K] L) :

Function.Bijective ⇑ϕ

source

@[reducible, inline]

noncomputable abbrev algEquivEquivAlgHom (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] :

(L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Equations

algEquivEquivAlgHom K L = Algebra.IsAlgebraic.algEquivEquivAlgHom K L

Instances For

source

theorem IsAlgebraic.exists_integral_multiple {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} (hz : IsAlgebraic R z) (inj : Function.Injective ⇑(algebraMap R A)) :

∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

source

@[deprecated IsAlgebraic.exists_integral_multiple (since := "2024-11-30")]

theorem exists_integral_multiple {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} (hz : IsAlgebraic R z) (inj : Function.Injective ⇑(algebraMap R A)) :

∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

Alias of IsAlgebraic.exists_integral_multiple.

source

theorem Algebra.IsAlgebraic.exists_integral_multiples {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] [NoZeroDivisors R] [alg : Algebra.IsAlgebraic R A] (inj : Function.Injective ⇑(algebraMap R A)) (s : Finset A) :

∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

source

theorem IsAlgebraic.of_smul_isIntegral {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} {y : R} (hy : ¬IsNilpotent y) (h : IsIntegral R (y • z)) :

IsAlgebraic R z

source

theorem IsAlgebraic.of_smul {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} {y : R} (hy : y ∈ nonZeroDivisors R) (h : IsAlgebraic R (y • z)) :

IsAlgebraic R z

source

theorem IsAlgebraic.iff_exists_smul_integral {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} [IsReduced R] (inj : Function.Injective ⇑(algebraMap R A)) :

IsAlgebraic R z ↔ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

source

theorem IsAlgebraic.restrictScalars_of_isIntegral (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] (inj : Function.Injective ⇑(algebraMap S A)) [int : Algebra.IsIntegral R S] {a : A} (h : IsAlgebraic S a) :

IsAlgebraic R a

source

theorem IsAlgebraic.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] (inj : Function.Injective ⇑(algebraMap S A)) [Algebra.IsAlgebraic R S] {a : A} (h : IsAlgebraic S a) :

IsAlgebraic R a

source

theorem IsIntegral.trans_isAlgebraic (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] (inj : Function.Injective ⇑(algebraMap S A)) [alg : Algebra.IsAlgebraic R S] {a : A} (h : IsIntegral S a) :

IsAlgebraic R a

source

theorem IsAlgebraic.neg {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {a : S} (ha : IsAlgebraic R a) :

IsAlgebraic R (-a)

source

theorem IsAlgebraic.smul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {a : S} (ha : IsAlgebraic R a) (r : R) :

IsAlgebraic R (r • a)

source

theorem IsAlgebraic.nsmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {a : S} (ha : IsAlgebraic R a) (n : ℕ) :

IsAlgebraic R (n • a)

source

theorem IsAlgebraic.zsmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {a : S} (ha : IsAlgebraic R a) (n : ℤ) :

IsAlgebraic R (n • a)

source

theorem IsAlgebraic.mul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [nzd : NoZeroDivisors R] {a b : S} (ha : IsAlgebraic R a) (hb : IsAlgebraic R b) :

IsAlgebraic R (a * b)

source

theorem IsAlgebraic.add {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [nzd : NoZeroDivisors R] {a b : S} (ha : IsAlgebraic R a) (hb : IsAlgebraic R b) :

IsAlgebraic R (a + b)

source

theorem IsAlgebraic.sub {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [nzd : NoZeroDivisors R] {a b : S} (ha : IsAlgebraic R a) (hb : IsAlgebraic R b) :

IsAlgebraic R (a - b)

source

theorem IsAlgebraic.pow {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [nzd : NoZeroDivisors R] {a : S} (ha : IsAlgebraic R a) (n : ℕ) :

IsAlgebraic R (a ^ n)

source

theorem Algebra.IsAlgebraic.trans' (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] (inj : Function.Injective ⇑(algebraMap S A)) [Algebra.IsAlgebraic R S] [alg : Algebra.IsAlgebraic S A] :

Algebra.IsAlgebraic R A

Transitivity of algebraicity for algebras over domains.

source

theorem Algebra.IsIntegral.trans_isAlgebraic (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] (inj : Function.Injective ⇑(algebraMap S A)) [Algebra.IsIntegral R S] [alg : Algebra.IsAlgebraic S A] :

Algebra.IsAlgebraic R A

source

theorem Algebra.IsAlgebraic.trans_isIntegral (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] (inj : Function.Injective ⇑(algebraMap S A)) [Algebra.IsAlgebraic R S] [int : Algebra.IsIntegral S A] :

Algebra.IsAlgebraic R A

source

def Subalgebra.algebraicClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] :

Subalgebra R S

If R is a domain and S is an arbitrary R-algebra, then the elements of S that are algebraic over R form a subalgebra.

Equations

Subalgebra.algebraicClosure R S = { carrier := {s : S | IsAlgebraic R s}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Instances For

source

theorem integralClosure_le_algebraicClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] :

integralClosure R S ≤ Subalgebra.algebraicClosure R S

source

theorem Subalgebra.algebraicClosure_eq_integralClosure (S : Type u_2) [CommRing S] {K : Type u_4} [Field K] [Algebra K S] :

Subalgebra.algebraicClosure K S = integralClosure K S

source

instance instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] :

Algebra.IsAlgebraic R ↥(Subalgebra.algebraicClosure R S)

source

theorem Algebra.isAlgebraic_adjoin_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] {s : Set S} :

(Algebra.adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x

source

theorem Algebra.isAlgebraic_adjoin_of_nonempty {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {s : Set S} (hs : s.Nonempty) :

(Algebra.adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x

source

theorem Algebra.isAlgebraic_adjoin_singleton_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {s : S} :

(Algebra.adjoin R {s}).IsAlgebraic ↔ IsAlgebraic R s

source

theorem IsAlgebraic.of_mul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {y z : S} (hy : y ∈ nonZeroDivisors S) (alg_y : IsAlgebraic R y) (alg_yz : IsAlgebraic R (y * z)) :

IsAlgebraic R z

source

theorem Transcendental.extendScalars_of_isIntegral {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} (ha : Transcendental R a) [NoZeroDivisors S] [Algebra.IsIntegral R S] (inj : Function.Injective ⇑(algebraMap S A)) :

Transcendental S a

source

theorem Transcendental.extendScalars {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} (ha : Transcendental R a) [NoZeroDivisors S] [Algebra.IsAlgebraic R S] (inj : Function.Injective ⇑(algebraMap S A)) :

Transcendental S a

source

theorem Transcendental.integralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {a : S} (ha : Transcendental R a) [NoZeroDivisors S] :

Transcendental (↥(integralClosure R S)) a

source

theorem Transcendental.subalgebraAlgebraicClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {a : S} (ha : Transcendental R a) [IsDomain R] [NoZeroDivisors S] :

Transcendental (↥(Subalgebra.algebraicClosure R S)) a

Documentation

Mathlib.RingTheory.Algebraic.Integral

Algebraic elements and integral elements #

Main results #