Algebraic Independence #
This file relates algebraic independence and transcendence (or algebraicity) of elements.
References #
Tags #
transcendence
theorem
algebraicIndependent_singleton_iff
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Subsingleton ι]
(i : ι)
:
theorem
AlgebraicIndependent.transcendental
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{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_3}
{A : Type v}
{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
trdeg_eq_zero
{R : Type u_3}
{A : Type v}
[CommRing R]
[CommRing A]
[Algebra R A]
[Algebra.IsAlgebraic R A]
:
theorem
AlgebraicIndependent.option_iff_transcendental
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{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.option_iff
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{a : A}
:
(AlgebraicIndependent R fun (o : Option ι) => o.elim a x) ↔ AlgebraicIndependent R x ∧ Transcendental (↥(Algebra.adjoin R (Set.range x))) a
theorem
AlgebraicIndepOn.insert_iff
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{s : Set ι}
{i : ι}
(h : i ∉ s)
:
AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(Algebra.adjoin R (x '' s))) (x i)
theorem
AlgebraicIndepOn.insert
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{s : Set ι}
{i : ι}
(hs : AlgebraicIndepOn R x s)
(hi : Transcendental (↥(Algebra.adjoin R (x '' s))) (x i))
:
AlgebraicIndepOn R x (insert i s)
theorem
algebraicIndependent_of_set_of_finite
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set ι)
(ind : AlgebraicIndependent R fun (i : ↑s) => x ↑i)
(H :
∀ (t : Set ι),
t.Finite →
(AlgebraicIndependent R fun (i : ↑t) => x ↑i) →
∀ i ∉ s, i ∉ t → Transcendental (↥(Algebra.adjoin R (x '' t))) (x i))
:
theorem
algebraicIndependent_of_finite_type'
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{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_3}
{A : Type v}
[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)
:
Variant of algebraicIndependent_of_finite using Transcendental.
theorem
AlgebraicIndependent.sumElim_iff
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{ι' : Type u_4}
{y : ι' → A}
:
AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(Algebra.adjoin R (Set.range x))) y
theorem
AlgebraicIndependent.iff_adjoin_image
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set ι)
:
AlgebraicIndependent R x ↔ (AlgebraicIndependent R fun (i : ↑s) => x ↑i) ∧ AlgebraicIndepOn (↥(Algebra.adjoin R (x '' s))) x sᶜ
theorem
AlgebraicIndependent.iff_adjoin_image_compl
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set ι)
:
AlgebraicIndependent R x ↔ (AlgebraicIndependent R fun (i : ↑sᶜ) => x ↑i) ∧ AlgebraicIndepOn (↥(Algebra.adjoin R (x '' sᶜ))) x s
theorem
AlgebraicIndependent.iff_transcendental_adjoin_image
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(i : ι)
:
AlgebraicIndependent R x ↔ (AlgebraicIndependent R fun (j : { j : ι // j ≠ i }) => x ↑j) ∧ Transcendental (↥(Algebra.adjoin R (x '' {i}ᶜ))) (x i)
theorem
AlgebraicIndependent.sumElim
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
{ι' : Type u_4}
{y : ι' → A}
(hy : AlgebraicIndependent (↥(Algebra.adjoin R (Set.range x))) y)
:
AlgebraicIndependent R (Sum.elim y x)
theorem
AlgebraicIndependent.sumElim_of_tower
{ι : Type u_1}
{R : Type u_3}
{S : Type u}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
(hx : AlgebraicIndependent R x)
{ι' : Type u_4}
{y : ι' → A}
(hxS : Set.range x ⊆ Set.range ⇑(algebraMap S A))
(hy : AlgebraicIndependent S y)
:
AlgebraicIndependent R (Sum.elim y x)
theorem
AlgebraicIndependent.sumElim_comp
{ι : Type u_1}
{R : Type u_3}
{S : Type u}
{A : Type v}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
{ι' : Type u_4}
{x : ι → S}
{y : ι' → A}
(hx : AlgebraicIndependent R x)
(hy : AlgebraicIndependent S y)
:
AlgebraicIndependent R (Sum.elim y (⇑(algebraMap S A) ∘ x))
theorem
AlgebraicIndependent.adjoin_of_disjoint
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{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_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[Nontrivial A]
{s t : Set ι}
:
theorem
AlgebraicIndependent.transcendental_adjoin
{ι : Type u_1}
{R : Type u_3}
{A : Type v}
{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_3}
{A : Type v}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[Nontrivial A]
{s : Set ι}
{i : ι}
:
theorem
lift_trdeg_add_le
{R : Type u_3}
{S : Type u}
{A : Type v}
[CommRing R]
[CommRing S]
[CommRing A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[Nontrivial R]
[FaithfulSMul R S]
[FaithfulSMul S A]
:
theorem
trdeg_add_le
{R : Type u_3}
{S : Type u}
[CommRing R]
[CommRing S]
[Algebra R S]
[Nontrivial R]
{A : Type u}
[CommRing A]
[Algebra R A]
[Algebra S A]
[FaithfulSMul R S]
[FaithfulSMul S A]
[IsScalarTower R S A]
:
theorem
MvPolynomial.algebraicIndependent_polynomial_aeval_X
{ι : Type u_1}
{R : Type u_3}
[CommRing R]
(f : ι → Polynomial R)
(hf : ∀ (i : ι), Transcendental R (f i))
:
AlgebraicIndependent R fun (i : ι) => (Polynomial.aeval (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_3}
{A : Type v}
{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.