English
There is a domain-specifically enhanced equivalence between S →_A B and roots in B of the minimal polynomial of pb.gen, valid for IsDomain B.
Русский
Существуют адаптированное эквивалентное соответствие между отображениями S →_A B и корнями в B минимального полинома pb.gen при B, являющемся доменом.
LaTeX
$$liftEquiv' [IsDomain B] (pb : PowerBasis A S) : (S →_A B) ≃ { y : B // y ∈ (minpoly A pb.gen).aroots B }$$
Lean4
/-- `pb.liftEquiv` states that roots of the minimal polynomial of `pb.gen` correspond to
maps sending `pb.gen` to that root.
This is the bundled equiv version of `PowerBasis.lift`.
If the codomain of the `AlgHom`s is an integral domain, then the roots form a multiset,
see `liftEquiv'` for the corresponding statement.
-/
@[simps]
noncomputable def liftEquiv (pb : PowerBasis A S) : (S →ₐ[A] S') ≃ { y : S' // aeval y (minpoly A pb.gen) = 0 }
where
toFun f := ⟨f pb.gen, by rw [aeval_algHom_apply, minpoly.aeval, map_zero]⟩
invFun y := pb.lift y y.2
left_inv _ := pb.algHom_ext <| lift_gen _ _ _
right_inv y := Subtype.ext <| lift_gen _ _ y.prop
