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.

noncomputable 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 ⋯)

@[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

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

noncomputable 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

@[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

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