Algebraic Independence #
This file contains basic results on algebraic independence of a family of elements of an R
-algebra
References #
Tags #
transcendence basis, transcendence degree, transcendence
The transcendence degree of a commutative algebra A
over a commutative ring R
is
defined to be the maximal cardinality of an R
-algebraically independent set in A
.
Equations
- Algebra.trdeg R A = ⨆ (ι : { s : Set A // AlgebraicIndepOn R id s }), Cardinal.mk ↑↑ι
Instances For
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
.
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.
Alias of AlgebraicIndependent.of_subsingleton
.
A set of algebraically independent elements in an algebra A
over a ring K
is also
algebraically independent over a subring R
of K
.
Every finite subset of an algebraically independent set is algebraically independent.
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.
The isomorphism between MvPolynomial (Option ι) R
and the polynomial ring over
the algebra generated by an algebraically independent family.
Equations
Instances For
simp
-normal form of mvPolynomialOptionEquivPolynomialAdjoin_C