# Algebraic Independence #

This file concerns adjoining an algebraic independent family to a field.

## Main definitions #

- `AlgebraicIndependent.aevalEquivField` - The canonical isomorphism from the rational function field ring to the intermediate field generated by an algebraic independent family.

- `AlgebraicIndependent.reprField` - The canonical map from the intermediate field generated by an algebraic independent family into the rational function field. It is the inverse of `AlgebraicIndependent.aevalEquivField`.

source
def AlgebraicIndependent.aevalEquivField {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [Field F] [Field E] [Algebra F E] (hx : AlgebraicIndependent F x) :
FractionRing (MvPolynomial ι F) ≃ₐ[F] ↥(IntermediateField.adjoin F (Set.range x))

Canonical isomorphism between rational function field and the intermediate field generated by algebraically independent elements.

Equations

- hx.aevalEquivField = (have this := AlgEquiv.ofInjectiveField (IsFractionRing.liftAlgHom ⋯); this).trans (IntermediateField.equivOfEq ⋯)

Instances For

source
@[simp]
theorem AlgebraicIndependent.aevalEquivField_apply_coe {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [Field F] [Field E] [Algebra F E] (hx : AlgebraicIndependent F x) (a : FractionRing (MvPolynomial ι F)) :
↑(hx.aevalEquivField a) = (IsFractionRing.lift ⋯) a
source
theorem AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [Field F] [Field E] [Algebra F E] (hx : AlgebraicIndependent F x) (a : MvPolynomial ι F) :
↑(hx.aevalEquivField ((algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) a)) = (MvPolynomial.aeval x) a
source
def AlgebraicIndependent.reprField {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [Field F] [Field E] [Algebra F E] (hx : AlgebraicIndependent F x) :
↥(IntermediateField.adjoin F (Set.range x)) →ₐ[F] FractionRing (MvPolynomial ι F)

The canonical map from the intermediate field generated by an algebraic independent family into the rational function field.

Equations

- hx.reprField = ↑hx.aevalEquivField.symm

Instances For

source
@[simp]
theorem AlgebraicIndependent.lift_reprField {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [Field F] [Field E] [Algebra F E] (hx : AlgebraicIndependent F x) (p : ↥(IntermediateField.adjoin F (Set.range x))) :
(IsFractionRing.lift ⋯) (hx.reprField p) = ↑p
source
theorem AlgebraicIndependent.liftAlgHom_comp_reprField {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [Field F] [Field E] [Algebra F E] (hx : AlgebraicIndependent F x) :
(IsFractionRing.liftAlgHom ⋯).comp hx.reprField = (IntermediateField.adjoin F (Set.range x)).val