English
If h1 and h2 hold (compatibilities of aeval with root and with pb.gen), then there exists an algebra isomorphism equivalence between AdjoinRoot g and S, given by lifting the root and pb.gen.
Русский
При выполнении условий совместимости отображений, существует изоморфизм R-алгебр между AdjoinRoot g и S, заданный через верхний уровень линеаризации корня и pb.gen.
LaTeX
$$$\\exists\\; \\text{equiv}'(g,pb,h_1,h_2)\\;:\\; AdjoinRoot\ng \\cong_R S$, определённый через liftHom g pb.gen h_2 и pb.lift (root g) h_1.$$
Lean4
/-- If `S` is an extension of `R` with power basis `pb` and `g` is a monic polynomial over `R`
such that `pb.gen` has a minimal polynomial `g`, then `S` is isomorphic to `AdjoinRoot g`.
Compare `PowerBasis.equivOfRoot`, which would require
`h₂ : aeval pb.gen (minpoly R (root g)) = 0`; that minimal polynomial is not
guaranteed to be identical to `g`. -/
@[simps -fullyApplied]
def equiv' (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) : AdjoinRoot g ≃ₐ[R] S :=
{ AdjoinRoot.liftHom g pb.gen h₂ with
toFun := AdjoinRoot.liftHom g pb.gen h₂
invFun := pb.lift (root g) h₁
left_inv x := AdjoinRoot.induction_on _ x fun x => by rw [liftHom_mk, pb.lift_aeval, aeval_eq]
right_inv := fun x => by
nontriviality S
obtain ⟨f, _hf, rfl⟩ := pb.exists_eq_aeval x
rw [pb.lift_aeval, aeval_eq, liftHom_mk] }
-- This lemma should have the simp tag but this causes a lint issue.
