aevalEquivField — Mathlib

English

The X_i is transcendental over the supported algebra when Not (i ∈ s).

Русский

X_i трансцендентален над поддерживаемой алгеброй, если i не принадлежит s.

LaTeX

$$$$ \text{Transcendental } (X_i) \text{ over } \operatorname{supported} R s \quad \text{ whenever } i \notin s. $$$$

Lean4

/-- Canonical isomorphism between rational function field and the
  intermediate field generated by algebraically independent elements. -/
def aevalEquivField : FractionRing (MvPolynomial ι F) ≃ₐ[F] ↥(IntermediateField.adjoin F (range x)) :=
  let i :=
    IsFractionRing.liftAlgHom (K := FractionRing (MvPolynomial ι F)) (algebraicIndependent_iff_injective_aeval.2 hx)
  (show _ ≃ₐ[F] i.fieldRange from AlgEquiv.ofInjectiveField i).trans <|
    IntermediateField.equivOfEq <|
      IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq (g := aeval x) (f := i) (by ext <;> simp [i])
        (Algebra.adjoin_range_eq_range_aeval F x).symm

Похожие утверждения