Algebraic Independence #
This file relates algebraic independence and transcendence (or algebraicity) of elements.
References #
Tags #
transcendence
@[simp]
theorem
algebraicIndependent_unique_type_iff
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Unique ι]
:
AlgebraicIndependent R x ↔ Transcendental R (x default)
A one-element family x is algebraically independent if and only if
its element is transcendental.
theorem
algebraicIndependent_singleton_iff
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Subsingleton ι]
(i : ι)
:
AlgebraicIndependent R x ↔ Transcendental R (x i)
theorem
algebraicIndependent_iff_transcendental
{R : Type u_2}
{A : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
{x : A}
:
AlgebraicIndependent R ![x] ↔ Transcendental R x
The one-element family ![x] is algebraically independent if and only if
x is transcendental.
theorem
AlgebraicIndependent.transcendental
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(i : ι)
:
Transcendental R (x i)
If a family x is algebraically independent, then any of its element is transcendental.
theorem
AlgebraicIndependent.isEmpty_of_isAlgebraic
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[Algebra.IsAlgebraic R A]
:
IsEmpty ι
If A/R is algebraic, then all algebraically independent families are empty.
theorem
AlgebraicIndependent.option_iff
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(a : A)
:
(AlgebraicIndependent R fun (o : Option ι) => o.elim a x) ↔ Transcendental (↥(Algebra.adjoin R (Set.range x))) a
theorem
algebraicIndependent_of_finite_type'
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hinj : Function.Injective ⇑(algebraMap R A))
(H :
∀ (t : Set ι),
t.Finite →
(AlgebraicIndependent R fun (i : ↑t) => x ↑i) → ∀ i ∉ t, Transcendental (↥(Algebra.adjoin R (x '' t))) (x i))
:
Variant of algebraicIndependent_of_finite_type using Transcendental.
theorem
algebraicIndependent_of_finite'
{R : Type u_2}
{A : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set A)
(hinj : Function.Injective ⇑(algebraMap R A))
(H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val → ∀ a ∈ s, a ∉ t → Transcendental (↥(Algebra.adjoin R t)) a)
:
AlgebraicIndependent R Subtype.val
Variant of algebraicIndependent_of_finite using Transcendental.
theorem
AlgebraicIndependent.adjoin_of_disjoint
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
{s t : Set ι}
(h : Disjoint s t)
:
AlgebraicIndependent ↥(Algebra.adjoin R (x '' s)) fun (i : ↑t) => x ↑i
theorem
AlgebraicIndependent.adjoin_iff_disjoint
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[Nontrivial A]
{s t : Set ι}
:
(AlgebraicIndependent ↥(Algebra.adjoin R (x '' s)) fun (i : ↑t) => x ↑i) ↔ Disjoint s t
theorem
AlgebraicIndependent.transcendental_adjoin
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
{s : Set ι}
{i : ι}
(hi : i ∉ s)
:
Transcendental (↥(Algebra.adjoin R (x '' s))) (x i)
theorem
AlgebraicIndependent.transcendental_adjoin_iff
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[Nontrivial A]
{s : Set ι}
{i : ι}
:
Transcendental (↥(Algebra.adjoin R (x '' s))) (x i) ↔ i ∉ s
theorem
MvPolynomial.algebraicIndependent_polynomial_aeval_X
{ι : Type u_1}
{R : Type u_2}
[CommRing R]
(f : ι → Polynomial R)
(hf : ∀ (i : ι), Transcendental R (f i))
:
AlgebraicIndependent R fun (i : ι) => (Polynomial.aeval (MvPolynomial.X i)) (f i)
If for each i : ι, f_i : R[X] is transcendental over R, then {f_i(X_i) | i : ι}
in MvPolynomial ι R is algebraically independent over R.
theorem
AlgebraicIndependent.polynomial_aeval_of_transcendental
{ι : Type u_1}
{R : Type u_2}
{A : Type u_3}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
{f : ι → Polynomial R}
(hf : ∀ (i : ι), Transcendental R (f i))
:
AlgebraicIndependent R fun (i : ι) => (Polynomial.aeval (x i)) (f i)
If {x_i : A | i : ι} is algebraically independent over R, and for each i,
f_i : R[X] is transcendental over R, then {f_i(x_i) | i : ι} is also
algebraically independent over R.