English
If p and q are polynomials with p∘q = X and q∘p = X, then there is an R-algebra automorphism of R[X] sending X to p (and inverse sending X to q).
Русский
Если p и q удовлетворяют p∘q = X и q∘p = X, то существует R-алгебравый автоморфизм R[X], отправляющий X в p (и, соответственно, инверсный отправляющий X в q).
LaTeX
$$$$\text{If } hpq: p\circ q = X \text{ and } hqp: q\circ p = X, \; R[X] \xrightarrow{\mathrm{aeval}(p)} R[X] \text{ is an automorphism.}$$$$
Lean4
/-- Two polynomials `p` and `q` such that `p(q(X))=X` and `q(p(X))=X`
induces an automorphism of the polynomial algebra. -/
@[simps!]
def algEquivOfCompEqX (p q : R[X]) (hpq : p.comp q = X) (hqp : q.comp p = X) : R[X] ≃ₐ[R] R[X] := by
refine AlgEquiv.ofAlgHom (aeval p) (aeval q) ?_ ?_ <;>
exact AlgHom.ext fun _ ↦ by simp [← comp_eq_aeval, comp_assoc, hpq, hqp]
