swap — Mathlib

English

There is an R-algebra automorphism swap of R[X][Y] that interchanges the variables X and Y, i.e., swap(X) = Y and swap(Y) = CX, where CX is the constant polynomial with value X.

Русский

Существует R-алгебра-автоморфизм swap на R[X][Y], обменивающий переменные X и Y: swap(X) = Y и swap(Y) = CX, где CX — константная полиномная функция.

LaTeX

$$$swap: R[X][Y]\\cong_R R[X][Y],\\quad swap(X)=Y,\\quad swap(Y)=C X.$$$

Lean4

/-- The R-algebra automorphism given by `X ↦ Y` and `Y ↦ X`. -/
def swap : R[X][Y] ≃ₐ[R] R[X][Y] := by
  apply AlgEquiv.ofAlgHom (aevalAeval (Y : R[X][Y]) (C X)) (aevalAeval (Y : R[X][Y]) (C X)) <;> (ext n m <;> simp)

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