Algebraic Independence

This file relates algebraic independence and transcendence (or algebraicity) of elements.

References

• Stacks: Transcendence

Tags

transcendence

@[simp]

theorem algebraicIndependent_unique_type_iff {ι : Type u_1} {R : Type u_3} {A : Type v} {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_3} {A : Type v} {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_3} {A : Type v} [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_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] : Algebra.trdeg R A = 0

theorem trdeg_pos (R : Type u_3) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] [Algebra.Transcendental R A] : 0 < Algebra.trdeg R A

theorem trdeg_eq_zero_iff {R : Type u_3} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] : Algebra.trdeg R A = 0 ↔ Algebra.IsAlgebraic R A

theorem trdeg_ne_zero_iff {R : Type u_3} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] : Algebra.trdeg R A ≠ 0 ↔ Algebra.Transcendental 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)) : AlgebraicIndependent R x

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)) : AlgebraicIndependent R x

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) : AlgebraicIndependent R Subtype.val

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 ι} : (AlgebraicIndependent ↥(Algebra.adjoin R (x '' s)) fun (i : ↑t) => x ↑i) ↔ Disjoint s t

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 : ι} : Transcendental (↥(Algebra.adjoin R (x '' s))) (x i) ↔ i ∉ s

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] : Cardinal.lift.{v, u} (Algebra.trdeg R S) + Cardinal.lift.{u, v} (Algebra.trdeg S A) ≤ Cardinal.lift.{u, v} (Algebra.trdeg R 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] : Algebra.trdeg R S + Algebra.trdeg S A ≤ Algebra.trdeg R 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.