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 : Polynomial R), 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 ∈ 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)
:
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
Algebra.IsIntegral.isAlgebraic
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
(h : Algebra.IsIntegral R A)
:
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
{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
{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 in that it
allows noncommutative intermediate rings A.
theorem
isAlgebraic_algHom_iff
{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)
(hf : Function.Injective ⇑f)
{a : A}
:
IsAlgebraic R (f a) ↔ IsAlgebraic R a
theorem
Algebra.IsAlgebraic.of_injective
{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)
(hf : Function.Injective ⇑f)
(h : Algebra.IsAlgebraic R B)
:
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.invOf
{R : Type u}
{S : Type u_1}
[CommRing R]
[CommRing S]
[Algebra R S]
{x : S}
[Invertible x]
(h : IsAlgebraic R x)
:
IsAlgebraic R ⅟x
theorem
IsAlgebraic.invOf_iff
{R : Type u}
{S : Type u_1}
[CommRing R]
[CommRing S]
[Algebra R S]
{x : S}
[Invertible x]
:
IsAlgebraic R ⅟x ↔ IsAlgebraic R x
theorem
IsAlgebraic.inv_iff
{R : Type u}
[CommRing R]
{K : Type u_2}
[Field K]
[Algebra R K]
{x : K}
:
IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
theorem
IsAlgebraic.inv
{R : Type u}
[CommRing R]
{K : Type u_2}
[Field K]
[Algebra R K]
{x : K}
:
IsAlgebraic R x → IsAlgebraic R x⁻¹
Alias of the reverse direction of IsAlgebraic.inv_iff.
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.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.
theorem
Algebra.IsAlgebraic.isIntegral
{K : Type u}
{A : Type v}
[Field K]
[Ring A]
[Algebra K A]
:
Algebra.IsAlgebraic K A → Algebra.IsIntegral K A
Alias of the forward direction of Algebra.isAlgebraic_iff_isIntegral.
theorem
IsAlgebraic.tower_top_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.tower_top_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.tower_top
{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.tower_top
{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]
[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)
:
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}
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
(ha : Algebra.IsAlgebraic K L)
(f : L →ₐ[K] L)
:
theorem
Algebra.IsAlgebraic.algHom_bijective₂
{K : Type u_1}
{L : Type u_2}
{R : Type u_3}
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
[Field R]
[Algebra K R]
(ha : Algebra.IsAlgebraic K L)
(f : L →ₐ[K] R)
(g : R →ₐ[K] L)
:
theorem
Algebra.IsAlgebraic.bijective_of_isScalarTower
{K : Type u_1}
{L : Type u_2}
{R : Type u_3}
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
(ha : Algebra.IsAlgebraic K L)
[Field R]
[Algebra K R]
[Algebra L R]
[IsScalarTower K L R]
(f : R →ₐ[K] L)
:
theorem
Algebra.IsAlgebraic.bijective_of_isScalarTower'
{K : Type u_1}
{L : Type u_2}
{R : Type u_3}
[CommRing K]
[Field L]
[Algebra K L]
[Field R]
[Algebra K R]
[NoZeroSMulDivisors K R]
(ha : Algebra.IsAlgebraic K R)
[Algebra L R]
[IsScalarTower K L R]
(f : R →ₐ[K] L)
:
@[simp]
theorem
Algebra.IsAlgebraic.algEquivEquivAlgHom_apply
(K : Type u_1)
(L : Type u_2)
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
(ha : Algebra.IsAlgebraic K L)
(ϕ : L ≃ₐ[K] L)
:
(Algebra.IsAlgebraic.algEquivEquivAlgHom K L ha) ϕ = ↑ϕ
@[simp]
theorem
Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply
(K : Type u_1)
(L : Type u_2)
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
(ha : Algebra.IsAlgebraic K L)
(ϕ : L →ₐ[K] L)
:
(MulEquiv.symm (Algebra.IsAlgebraic.algEquivEquivAlgHom K L ha)) ϕ = AlgEquiv.ofBijective ϕ (_ : Function.Bijective ⇑ϕ)
noncomputable def
Algebra.IsAlgebraic.algEquivEquivAlgHom
(K : Type u_1)
(L : Type u_2)
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors 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
theorem
AlgHom.bijective
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(ϕ : L →ₐ[K] L)
:
@[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 : ↥(integralClosure R S)) (y : R) (_ : y ≠ 0), 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 : ↥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 : ↥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)
:
IsField ↥A
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 : Polynomial R') (f : R' → S') (x : R') => 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 : Polynomial R') (f : S' → T') (x : S') => (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')
:
@[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')
:
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 : Polynomial R') (z : S') =>
(algebraMap S' 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 : Polynomial R') (z : R') => Polynomial.eval z p