equivOfTranscendenceBasis — Mathlib

English

Two algebraically closed fields with equipotent transcendence bases over a base ring are isomorphic.

Русский

Два замкнутых по алгебре поля с равномерными базисами над основанием изоморфны.

LaTeX

$$IsAlgClosed.ringEquiv_of_equiv_of_charZero hK hKL$$

Lean4

/-- setting `R` to be `ZMod (ringChar R)` this result shows that if two algebraically
closed fields have equipotent transcendence bases and the same characteristic then they are
isomorphic. -/
def equivOfTranscendenceBasis [IsAlgClosed K] [IsAlgClosed L] (e : ι ≃ κ) (hv : IsTranscendenceBasis R v)
    (hw : IsTranscendenceBasis R w) : K ≃+* L :=
  by
  letI := isAlgClosure_of_transcendence_basis v hv
  letI := isAlgClosure_of_transcendence_basis w hw
  have e : Algebra.adjoin R (Set.range v) ≃+* Algebra.adjoin R (Set.range w) :=
    by
    refine hv.1.aevalEquiv.symm.toRingEquiv.trans ?_
    refine (AlgEquiv.ofAlgHom (MvPolynomial.rename e) (MvPolynomial.rename e.symm) ?_ ?_).toRingEquiv.trans ?_
    · ext; simp
    · ext; simp
    exact hw.1.aevalEquiv.toRingEquiv
  exact IsAlgClosure.equivOfEquiv K L e

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