Algebraic Independence #
This file defines algebraic independence of a family of elements of an R
algebra.
Main definitions #
AlgebraicIndependent
-AlgebraicIndependent R x
states the family of elementsx
is algebraically independent overR
, meaning that the canonical map out of the multivariable polynomial ring is injective.AlgebraicIndependent.aevalEquiv
- The canonical isomorphism from the polynomial ring to the subalgebra generated by an algebraic independent family.AlgebraicIndependent.repr
- The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring. It is the inverse ofAlgebraicIndependent.aevalEquiv
.IsTranscendenceBasis R x
- a familyx
is a transcendence basis overR
if it is a maximal algebraically independent subset.
Main results #
We show that algebraic independence is preserved under injective maps of the indices.
References #
AlgebraicIndependent R x
states the family of elements x
is algebraically independent over R
, meaning that the canonical
map out of the multivariable polynomial ring is injective.
Stacks Tag 030E ((1))
Equations
Instances For
AlgebraicIndepOn R v s
states that the elements in the family v
that are indexed by the
elements of s
are algebraically independent over R
.
Equations
- AlgebraicIndepOn R x s = AlgebraicIndependent R fun (i : ↑s) => x ↑i
Instances For
Alias of the forward direction of algebraicIndependent_subtype_range
.
Canonical isomorphism between polynomials and the subalgebra generated by algebraically independent elements.
Equations
- hx.aevalEquiv = (AlgEquiv.ofInjective (MvPolynomial.aeval x) ⋯).trans ((MvPolynomial.aeval x).range.equivOfEq (Algebra.adjoin R (Set.range x)) ⋯)
Instances For
The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring.
Equations
- hx.repr = ↑hx.aevalEquiv.symm
Instances For
A family is a transcendence basis if it is a maximal algebraically independent subset.
Stacks Tag 030E ((4))
Equations
- IsTranscendenceBasis R x = (AlgebraicIndependent R x ∧ ∀ (s : Set A), AlgebraicIndepOn R id s → Set.range x ⊆ s → Set.range x = s)
Instances For
Alias of the forward direction of isTranscendenceBasis_subtype_range
.