algHomAdjoinIntegralEquiv — Mathlib

English

There is a bijection between F-algebra homomorphisms F⟮α⟯ →ₐ[F] K and the roots of the polynomial minpoly F α in K (via the adjoin construction).

Русский

Существует биекция между алгеброморфизмами F⟮α⟯ →ₐ[F] K и корнями многочлена minpoly F α в K (через конструкцию адъюнкта).

LaTeX

$$Equiv between (F⟮α⟯ →ₐ[F] K) and { x // x ∈ (minpoly F α).aroots K }$$

Lean4

/-- Algebra homomorphism `F⟮α⟯ →ₐ[F] K` are in bijection with the set of roots
of `minpoly α` in `K`. -/
noncomputable def algHomAdjoinIntegralEquiv (h : IsIntegral F α) :
    (F⟮α⟯ →ₐ[F] K) ≃ { x // x ∈ (minpoly F α).aroots K } :=
  (adjoin.powerBasis h).liftEquiv'.trans
    ((Equiv.refl _).subtypeEquiv fun x => by rw [adjoin.powerBasis_gen, minpoly_gen, Equiv.refl_apply])

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