Algebraic elements and algebraic extensions #
An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial. An R-algebra is algebraic over R if and only if all its elements are algebraic over R. The main result in this file proves transitivity of algebraicity: a tower of algebraic field extensions is algebraic.
An element of an R-algebra is algebraic over R if it is a root of a nonzero polynomial with coefficients in R.
Equations
- IsAlgebraic R x = ∃ p, p ≠ 0 ∧ ↑(Polynomial.aeval x) p = 0
Instances For
An element of an R-algebra is transcendental over R if it is not algebraic over R.
Equations
- Transcendental R x = ¬IsAlgebraic R x
Instances For
theorem
is_transcendental_of_subsingleton
(R : Type u)
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Subsingleton R]
(x : A)
:
Transcendental R x
def
Subalgebra.IsAlgebraic
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
(S : Subalgebra R A)
:
A subalgebra is algebraic if all its elements are algebraic.
Equations
- Subalgebra.IsAlgebraic S = ∀ (x : A), x ∈ S → IsAlgebraic R x
Instances For
An algebra is algebraic if all its elements are algebraic.
Equations
- Algebra.IsAlgebraic R A = ∀ (x : A), IsAlgebraic R x
Instances For
theorem
Subalgebra.isAlgebraic_iff
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
(S : Subalgebra R A)
:
Subalgebra.IsAlgebraic S ↔ Algebra.IsAlgebraic R { x // x ∈ S }
A subalgebra is algebraic if and only if it is algebraic as an algebra.
theorem
isAlgebraic_iff_not_injective
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{x : A}
:
IsAlgebraic R x ↔ ¬Function.Injective ↑(Polynomial.aeval x)
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.
theorem
isAlgebraic_zero
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
:
IsAlgebraic R 0
theorem
isAlgebraic_algebraMap
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
(x : R)
:
IsAlgebraic R (↑(algebraMap R A) x)
An element of R is algebraic, when viewed as an element of the R-algebra A.
theorem
isAlgebraic_one
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
:
IsAlgebraic R 1
theorem
isAlgebraic_nat
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
(n : ℕ)
:
IsAlgebraic R ↑n
theorem
isAlgebraic_int
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
(n : ℤ)
:
IsAlgebraic R ↑n
theorem
isAlgebraic_rat
(R : Type u)
{A : Type v}
[DivisionRing A]
[Field R]
[Algebra R A]
(n : ℚ)
:
IsAlgebraic R ↑n
theorem
isAlgebraic_of_mem_rootSet
{R : Type u}
{A : Type v}
[Field R]
[Field A]
[Algebra R A]
{p : Polynomial R}
{x : A}
(hx : x ∈ Polynomial.rootSet p A)
:
IsAlgebraic R x
theorem
isAlgebraic_algebraMap_of_isAlgebraic
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
[Algebra R S]
[Algebra S A]
[IsScalarTower R S A]
{a : S}
:
IsAlgebraic R a → IsAlgebraic R (↑(algebraMap S A) a)
theorem
isAlgebraic_algHom_of_isAlgebraic
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra R B]
(f : A →ₐ[R] B)
{a : A}
(h : IsAlgebraic R a)
:
IsAlgebraic R (↑f a)
This is slightly more general than isAlgebraic_algebraMap_of_isAlgebraic in that it
allows noncommutative intermediate rings A.
theorem
AlgEquiv.isAlgebraic
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra R B]
(e : A ≃ₐ[R] B)
(h : Algebra.IsAlgebraic R A)
:
Transfer Algebra.IsAlgebraic across an AlgEquiv.
theorem
AlgEquiv.isAlgebraic_iff
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra R B]
(e : A ≃ₐ[R] B)
:
Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R B
theorem
isAlgebraic_algebraMap_iff
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
[Algebra R S]
[Algebra S A]
[IsScalarTower R S A]
{a : S}
(h : Function.Injective ↑(algebraMap S A))
:
IsAlgebraic R (↑(algebraMap S A) a) ↔ IsAlgebraic R a
theorem
isAlgebraic_of_pow
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
{n : ℕ}
(hn : 0 < n)
(ht : IsAlgebraic R (r ^ n))
:
IsAlgebraic R r
theorem
Transcendental.pow
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
(ht : Transcendental R r)
{n : ℕ}
(hn : 0 < n)
:
Transcendental R (r ^ n)
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.
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
theorem
isAlgebraic_of_larger_base_of_injective
{R : Type u_3}
{S : Type u_4}
{A : Type u_5}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
(hinj : Function.Injective ↑(algebraMap R S))
{x : A}
(A_alg : IsAlgebraic R x)
:
IsAlgebraic S x
If x is algebraic over R, then x is algebraic over S when S is an extension of R,
and the map from R to S is injective.
theorem
Algebra.isAlgebraic_of_larger_base_of_injective
{R : Type u_3}
{S : Type u_4}
{A : Type u_5}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
(hinj : Function.Injective ↑(algebraMap R S))
(A_alg : Algebra.IsAlgebraic R A)
:
If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R,
and the map from R to S is injective.
theorem
isAlgebraic_of_larger_base
{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]
{x : A}
(A_alg : IsAlgebraic K x)
:
IsAlgebraic L x
If x is algebraic over K, then x is algebraic over L when L is an extension of K
theorem
Algebra.isAlgebraic_of_larger_base
{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]
(A_alg : Algebra.IsAlgebraic K A)
:
If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K
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
theorem
Algebra.isAlgebraic_of_finite
(K : Type u_1)
(A : Type u_5)
[Field K]
[Ring A]
[Algebra K A]
[FiniteDimensional K A]
:
A field extension is algebraic if it is finite.
theorem
Algebra.isAlgebraic_trans
{K : Type u_1}
{L : Type u_2}
{A : Type u_5}
[Field K]
[Field L]
[CommRing 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)
:
If L is an algebraic field extension of K and A is an algebraic algebra over L, then A is algebraic over K.
theorem
Algebra.IsAlgebraic.algHom_bijective
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(ha : Algebra.IsAlgebraic K L)
(f : L →ₐ[K] L)
:
theorem
AlgHom.bijective
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(ϕ : L →ₐ[K] L)
:
@[simp]
theorem
Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply
(K : Type u_1)
(L : Type u_2)
[Field K]
[Field L]
[Algebra K L]
(ha : Algebra.IsAlgebraic K L)
(ϕ : L →ₐ[K] L)
:
↑(MulEquiv.symm (Algebra.IsAlgebraic.algEquivEquivAlgHom K L ha)) ϕ = AlgEquiv.ofBijective ϕ (_ : Function.Bijective ↑ϕ)
@[simp]
theorem
Algebra.IsAlgebraic.algEquivEquivAlgHom_apply
(K : Type u_1)
(L : Type u_2)
[Field K]
[Field L]
[Algebra K L]
(ha : Algebra.IsAlgebraic K L)
(ϕ : L ≃ₐ[K] L)
:
↑(Algebra.IsAlgebraic.algEquivEquivAlgHom K L ha) ϕ = ↑ϕ
noncomputable def
Algebra.IsAlgebraic.algEquivEquivAlgHom
(K : Type u_1)
(L : Type u_2)
[Field K]
[Field L]
[Algebra K L]
(ha : Algebra.IsAlgebraic K L)
:
Bijection between algebra equivalences and algebra homomorphisms
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible]
noncomputable def
algEquivEquivAlgHom
(K : Type u_1)
(L : Type u_2)
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
:
Bijection between algebra equivalences and algebra homomorphisms
Equations
- algEquivEquivAlgHom K L = Algebra.IsAlgebraic.algEquivEquivAlgHom K L (_ : Algebra.IsAlgebraic K L)
Instances For
theorem
exists_integral_multiple
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[IsDomain R]
[CommRing S]
[Algebra R S]
{z : S}
(hz : IsAlgebraic R z)
(inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0)
:
∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
theorem
IsIntegralClosure.exists_smul_eq_mul
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[IsDomain R]
[CommRing S]
{L : Type u_3}
[Field L]
[Algebra R S]
[Algebra S L]
[Algebra R L]
[IsScalarTower R S L]
[IsIntegralClosure S R L]
(h : Algebra.IsAlgebraic R L)
(inj : Function.Injective ↑(algebraMap R L))
(a : S)
{b : S}
(hb : b ≠ 0)
:
A fraction (a : S) / (b : S) can be reduced to (c : S) / (d : R),
if S is the integral closure of R in an algebraic extension L of R.
theorem
inv_eq_of_aeval_divX_ne_zero
{K : Type u_3}
{L : Type u_4}
[Field K]
[Field L]
[Algebra K L]
{x : L}
{p : Polynomial K}
(aeval_ne : ↑(Polynomial.aeval x) (Polynomial.divX p) ≠ 0)
:
x⁻¹ = ↑(Polynomial.aeval x) (Polynomial.divX p) / (↑(Polynomial.aeval x) p - ↑(algebraMap K L) (Polynomial.coeff p 0))
theorem
inv_eq_of_root_of_coeff_zero_ne_zero
{K : Type u_3}
{L : Type u_4}
[Field K]
[Field L]
[Algebra K L]
{x : L}
{p : Polynomial K}
(aeval_eq : ↑(Polynomial.aeval x) p = 0)
(coeff_zero_ne : Polynomial.coeff p 0 ≠ 0)
:
x⁻¹ = -(↑(Polynomial.aeval x) (Polynomial.divX p) / ↑(algebraMap K L) (Polynomial.coeff p 0))
theorem
Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero
{K : Type u_3}
{L : Type u_4}
[Field K]
[Field L]
[Algebra K L]
(A : Subalgebra K L)
{x : { x // x ∈ A }}
{p : Polynomial K}
(aeval_eq : ↑(Polynomial.aeval x) p = 0)
(coeff_zero_ne : Polynomial.coeff p 0 ≠ 0)
:
theorem
Subalgebra.inv_mem_of_algebraic
{K : Type u_3}
{L : Type u_4}
[Field K]
[Field L]
[Algebra K L]
(A : Subalgebra K L)
{x : { x // x ∈ A }}
(hx : IsAlgebraic K ↑x)
:
theorem
Subalgebra.isField_of_algebraic
{K : Type u_3}
{L : Type u_4}
[Field K]
[Field L]
[Algebra K L]
(A : Subalgebra K L)
(hKL : Algebra.IsAlgebraic K L)
:
In an algebraic extension L/K, an intermediate subalgebra is a field.
def
Polynomial.hasSMulPi
(R' : Type u)
(S' : Type v)
[Semiring R']
[SMul R' S']
:
SMul (Polynomial R') (R' → S')
This is not an instance as it forms a diamond with Pi.instSMul.
See the instance_diamonds test for details.
Equations
- Polynomial.hasSMulPi R' S' = { smul := fun p f x => Polynomial.eval x p • f x }
Instances For
noncomputable def
Polynomial.hasSMulPi'
(R' : Type u)
(S' : Type v)
(T' : Type w)
[CommSemiring R']
[Semiring S']
[Algebra R' S']
[SMul S' T']
:
SMul (Polynomial R') (S' → T')
This is not an instance as it forms a diamond with Pi.instSMul.
See the instance_diamonds test for details.
Equations
- Polynomial.hasSMulPi' R' S' T' = { smul := fun p f x => ↑(Polynomial.aeval x) p • f x }
Instances For
@[simp]
theorem
polynomial_smul_apply
(R' : Type u)
(S' : Type v)
[Semiring R']
[SMul R' S']
(p : Polynomial R')
(f : R' → S')
(x : R')
:
(Polynomial R' • (R' → S')) (R' → S') instHSMul p f x = Polynomial.eval x p • f x
@[simp]
theorem
polynomial_smul_apply'
(R' : Type u)
(S' : Type v)
(T' : Type w)
[CommSemiring R']
[Semiring S']
[Algebra R' S']
[SMul S' T']
(p : Polynomial R')
(f : S' → T')
(x : S')
:
(Polynomial R' • (S' → T')) (S' → T') instHSMul p f x = ↑(Polynomial.aeval x) p • f x
noncomputable def
Polynomial.algebraPi
(R' : Type u)
(S' : Type v)
(T' : Type w)
[CommSemiring R']
[CommSemiring S']
[CommSemiring T']
[Algebra R' S']
[Algebra S' T']
:
Algebra (Polynomial R') (S' → T')
This is not an instance for the same reasons as Polynomial.hasSMulPi'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Polynomial.algebraMap_pi_eq_aeval
(R' : Type u)
(S' : Type v)
(T' : Type w)
[CommSemiring R']
[CommSemiring S']
[CommSemiring T']
[Algebra R' S']
[Algebra S' T']
:
↑(algebraMap (Polynomial R') (S' → T')) = fun p z => ↑(algebraMap ((fun x => S') p) T') (↑(Polynomial.aeval z) p)
@[simp]
theorem
Polynomial.algebraMap_pi_self_eq_eval
(R' : Type u)
[CommSemiring R']
:
↑(algebraMap (Polynomial R') (R' → R')) = fun p z => Polynomial.eval z p