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 ofAlgebraicIndependent.aevalEquivField.
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 = (let_fun this := AlgEquiv.ofInjectiveField (IsFractionRing.liftAlgHom ⋯); this).trans (IntermediateField.equivOfEq ⋯)
Instances For
@[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
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
@[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