Commit 2024-11-15 09:12 80126d53

View on Github →

feat(RingTheory/AlgebraicIndependent): add AlgebraicIndependent.aevalEquivField and other results (#18648) This PR mainly adds

AlgebraicIndependent.aevalEquivField: canonical isomorphism between rational function field and the intermediate field generated by algebraically independent elements.
AlgebraicIndependent.reprField: canonical map from the intermediate field generated by an algebraic independent family into the rational function field. Other results:
AlgebraicIndependent.aeval_of_algebraicIndependent: 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.
AlgebraicIndependent.of_aeval: conversely, if {f_i(x) | i : ι} is algebraically independent over R, then {f_i : MvPolynomial ι R | i : ι} is also algebraically independent over R.
AlgebraicIndependent.polynomial_aeval_of_transcendental: 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.
AlgebraicIndependent.isEmpty_of_isAlgebraic: if A/R is algebraic, then all algebraically independent families are empty.
IsTranscendenceBasis.isEmpty_iff_isAlgebraic: if x is a transcendence basis of A/R, then it is empty if and only if A/R is algebraic.
IsTranscendenceBasis.nonempty_iff_transcendental: if x is a transcendence basis of A/R, then it is not empty if and only if A/R is transcendental.
IsTranscendenceBasis.isAlgebraic_field: if x is a transcendence basis of E / F, then the field extension E / F(x) is algebraic. Also add [of_]ringHom_of_comp_eq for [Algebra.]Transcendental and AlgebraicIndependent. Also add some results for Subalgebra inspired by IntermediateField.isAlgebraic_iff. Some of them are not back-ported to IntermediateField yet; may be for another PR if they are useful.