English
Given two power bases pb and pb', and that pb.gen and pb'.gen are mutual roots of each other via their minimal polynomials, there is a canonical algebra equivalence pb ≃ pb'.
Русский
При наличии двух баз силы pb и pb' и условии взаимной корневой связи их генераторов, существует каноническое алгебраическое эквивалентное отображение pb ≃ pb'.
LaTeX
$$pb.equivOfRoot pb' h1 h2 : S ≃_A S'$$
Lean4
/-- `pb.liftEquiv'` states that elements of the root set of the minimal
polynomial of `pb.gen` correspond to maps sending `pb.gen` to that root. -/
@[simps! -fullyApplied]
noncomputable def liftEquiv' [IsDomain B] (pb : PowerBasis A S) :
(S →ₐ[A] B) ≃ { y : B // y ∈ (minpoly A pb.gen).aroots B } :=
pb.liftEquiv.trans
((Equiv.refl _).subtypeEquiv fun x =>
by
rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]
· simp
· exact map_monic_ne_zero (minpoly.monic pb.isIntegral_gen))
