Algebraic Independence #
This file contains basic results on algebraic independence of a family of elements of an R-algebra
References #
TODO #
Define the transcendence degree and show it is independent of the choice of a transcendence basis.
Tags #
transcendence basis, transcendence degree, transcendence
theorem
algebraicIndependent_iff_ker_eq_bot
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
:
AlgebraicIndependent R x ↔ RingHom.ker (MvPolynomial.aeval x).toRingHom = ⊥
@[simp]
theorem
algebraicIndependent_empty_type_iff
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[IsEmpty ι]
:
AlgebraicIndependent R x ↔ Function.Injective ⇑(algebraMap R A)
theorem
AlgebraicIndependent.algebraMap_injective
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
:
Function.Injective ⇑(algebraMap R A)
theorem
AlgebraicIndependent.linearIndependent
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
:
theorem
AlgebraicIndependent.injective
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[Nontrivial R]
:
theorem
AlgebraicIndependent.ne_zero
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
[Nontrivial R]
(i : ι)
:
x i ≠ 0
theorem
AlgebraicIndependent.map
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{A' : Type u_6}
{x : ι → A}
[CommRing R]
[CommRing A]
[CommRing A']
[Algebra R A]
[Algebra R A']
(hx : AlgebraicIndependent R x)
{f : A →ₐ[R] A'}
(hf_inj : Set.InjOn ⇑f ↑(Algebra.adjoin R (Set.range x)))
:
AlgebraicIndependent R (⇑f ∘ x)
theorem
AlgebraicIndependent.map'
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{A' : Type u_6}
{x : ι → A}
[CommRing R]
[CommRing A]
[CommRing A']
[Algebra R A]
[Algebra R A']
(hx : AlgebraicIndependent R x)
{f : A →ₐ[R] A'}
(hf_inj : Function.Injective ⇑f)
:
AlgebraicIndependent R (⇑f ∘ x)
theorem
AlgebraicIndependent.aeval_of_algebraicIndependent
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
{f : ι → MvPolynomial ι R}
(hf : AlgebraicIndependent R f)
:
AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i)
If x = {x_i : A | i : ι} and f = {f_i : MvPolynomial ι R | i : ι} are algebraically
independent over R, then {f_i(x) | i : ι} is also algebraically independent over R.
For the partial converse, see AlgebraicIndependent.of_aeval.
theorem
AlgebraicIndependent.of_aeval
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{f : ι → MvPolynomial ι R}
(H : AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i))
:
If {f_i(x) | i : ι} is algebraically independent over R, then
{f_i : MvPolynomial ι R | i : ι} is also algebraically independent over R.
In fact, the x = {x_i : A | i : ι} is also transcendental over R provided that R
is a field and ι is finite; the proof needs transcendence degree.
theorem
MvPolynomial.algebraicIndependent_X
(σ : Type u_7)
(R : Type u_8)
[CommRing R]
:
AlgebraicIndependent R MvPolynomial.X
theorem
AlgHom.algebraicIndependent_iff
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{A' : Type u_6}
{x : ι → A}
[CommRing R]
[CommRing A]
[CommRing A']
[Algebra R A]
[Algebra R A']
(f : A →ₐ[R] A')
(hf : Function.Injective ⇑f)
:
AlgebraicIndependent R (⇑f ∘ x) ↔ AlgebraicIndependent R x
theorem
algebraicIndependent_of_subsingleton
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Subsingleton R]
:
theorem
algebraicIndependent_adjoin
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hs : AlgebraicIndependent R x)
:
AlgebraicIndependent R fun (i : ι) => ⟨x i, ⋯⟩
theorem
AlgebraicIndependent.restrictScalars
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{K : Type u_7}
[CommRing K]
[Algebra R K]
[Algebra K A]
[IsScalarTower R K A]
(hinj : Function.Injective ⇑(algebraMap R K))
(ai : AlgebraicIndependent K x)
:
A set of algebraically independent elements in an algebra A over a ring K is also
algebraically independent over a subring R of K.
theorem
AlgebraicIndependent.of_ringHom_of_comp_eq
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{S : Type u_7}
{B : Type u_8}
{FRS : Type u_9}
{FAB : Type u_10}
[CommRing S]
[CommRing B]
[Algebra S B]
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
(H : AlgebraicIndependent S (⇑g ∘ x))
(hf : Function.Injective ⇑f)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
theorem
AlgebraicIndependent.ringHom_of_comp_eq
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{S : Type u_7}
{B : Type u_8}
{FRS : Type u_9}
{FAB : Type u_10}
[CommRing S]
[CommRing B]
[Algebra S B]
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
(H : AlgebraicIndependent R x)
(hf : Function.Surjective ⇑f)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
AlgebraicIndependent S (⇑g ∘ x)
theorem
algebraicIndependent_ringHom_iff_of_comp_eq
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{S : Type u_7}
{B : Type u_8}
{FRS : Type u_9}
{FAB : Type u_10}
[CommRing S]
[CommRing B]
[Algebra S B]
[EquivLike FRS R S]
[RingEquivClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
AlgebraicIndependent S (⇑g ∘ x) ↔ AlgebraicIndependent R x
theorem
algebraicIndependent_finset_map_embedding_subtype
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set A)
(li : AlgebraicIndependent R Subtype.val)
(t : Finset ↑s)
:
AlgebraicIndependent R Subtype.val
Every finite subset of an algebraically independent set is algebraically independent.
theorem
algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{n : ℕ}
(H : ∀ (s : Finset A), (AlgebraicIndependent R fun (i : { x : A // x ∈ s }) => ↑i) → s.card ≤ n)
(s : Set A)
:
AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n
If every finite set of algebraically independent element has cardinality at most n,
then the same is true for arbitrary sets of algebraically independent elements.
theorem
AlgebraicIndependent.restrict_of_comp_subtype
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{s : Set ι}
(hs : AlgebraicIndependent R (x ∘ Subtype.val))
:
AlgebraicIndependent R (s.restrict x)
theorem
algebraicIndependent_empty_iff
(R : Type u_3)
(A : Type u_5)
[CommRing R]
[CommRing A]
[Algebra R A]
:
AlgebraicIndependent R Subtype.val ↔ Function.Injective ⇑(algebraMap R A)
theorem
AlgebraicIndependent.to_subtype_range
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{ι : Type u_7}
{f : ι → A}
(hf : AlgebraicIndependent R f)
:
AlgebraicIndependent R Subtype.val
theorem
AlgebraicIndependent.to_subtype_range'
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{ι : Type u_7}
{f : ι → A}
(hf : AlgebraicIndependent R f)
{t : Set A}
(ht : Set.range f = t)
:
AlgebraicIndependent R Subtype.val
theorem
algebraicIndependent_comp_subtype
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{s : Set ι}
:
AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ MvPolynomial.supported R s, (MvPolynomial.aeval x) p = 0 → p = 0
theorem
algebraicIndependent_subtype
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{s : Set A}
:
AlgebraicIndependent R Subtype.val ↔ ∀ p ∈ MvPolynomial.supported R s, (MvPolynomial.aeval id) p = 0 → p = 0
theorem
algebraicIndependent_of_finite
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set A)
(H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val)
:
AlgebraicIndependent R Subtype.val
theorem
algebraicIndependent_of_finite_type
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(H : ∀ (t : Set ι), t.Finite → AlgebraicIndependent R fun (i : ↑t) => x ↑i)
:
theorem
AlgebraicIndependent.image_of_comp
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{ι : Type u_7}
{ι' : Type u_8}
(s : Set ι)
(f : ι → ι')
(g : ι' → A)
(hs : AlgebraicIndependent R fun (x : ↑s) => g (f ↑x))
:
AlgebraicIndependent R fun (x : ↑(f '' s)) => g ↑x
theorem
AlgebraicIndependent.image
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{ι : Type u_7}
{s : Set ι}
{f : ι → A}
(hs : AlgebraicIndependent R fun (x : ↑s) => f ↑x)
:
AlgebraicIndependent R fun (x : ↑(f '' s)) => ↑x
theorem
algebraicIndependent_iUnion_of_directed
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{η : Type u_7}
[Nonempty η]
{s : η → Set A}
(hs : Directed (fun (x1 x2 : Set A) => x1 ⊆ x2) s)
(h : ∀ (i : η), AlgebraicIndependent R Subtype.val)
:
AlgebraicIndependent R Subtype.val
theorem
algebraicIndependent_sUnion_of_directed
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{s : Set (Set A)}
(hsn : s.Nonempty)
(hs : DirectedOn (fun (x1 x2 : Set A) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val)
:
AlgebraicIndependent R Subtype.val
theorem
AlgebraicIndependent.repr_ker
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
:
RingHom.ker ↑hx.repr = ⊥
def
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
:
MvPolynomial (Option ι) R ≃+* Polynomial ↥(Algebra.adjoin R (Set.range x))
The isomorphism between MvPolynomial (Option ι) R and the polynomial ring over
the algebra generated by an algebraically independent family.
Equations
- hx.mvPolynomialOptionEquivPolynomialAdjoin = (MvPolynomial.optionEquivLeft R ι).toRingEquiv.trans (Polynomial.mapEquiv hx.aevalEquiv.toRingEquiv)
Instances For
@[simp]
theorem
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(y : MvPolynomial (Option ι) R)
:
hx.mvPolynomialOptionEquivPolynomialAdjoin y = Polynomial.map (↑hx.aevalEquiv)
((MvPolynomial.aeval fun (o : Option ι) => o.elim Polynomial.X fun (s : ι) => Polynomial.C (MvPolynomial.X s)) y)
@[simp]
theorem
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C'
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(r : R)
:
Polynomial.C (hx.aevalEquiv (MvPolynomial.C r)) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
simp-normal form of mvPolynomialOptionEquivPolynomialAdjoin_C
theorem
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(r : R)
:
hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.C r) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
theorem
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
:
hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X none) = Polynomial.X
theorem
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(i : ι)
:
hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X (some i)) = Polynomial.C (hx.aevalEquiv (MvPolynomial.X i))
theorem
AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
(a : A)
:
(↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(MvPolynomial.aeval fun (o : Option ι) => o.elim a x)
theorem
algebraicIndependent_empty_type
{ι : Type u_1}
{K : Type u_4}
{A : Type u_5}
{x : ι → A}
[CommRing A]
[Field K]
[Algebra K A]
[IsEmpty ι]
[Nontrivial A]
:
theorem
algebraicIndependent_empty
{K : Type u_4}
{A : Type u_5}
[CommRing A]
[Field K]
[Algebra K A]
[Nontrivial A]
:
AlgebraicIndependent K Subtype.val