equiv — Mathlib

English

There is an R-algebra isomorphism between A[X] and A ⊗R R[X] given by the pair (toFunAlgHom, invFun) with the stated inverses.

Русский

Существуют R-алгебраическое изоморфизм между A[X] и A ⊗R R[X], заданный парой (toFunAlgHom, invFun) с указанными обратными.

LaTeX

$$polyEquivTensor : A[X] ≃ₐ[R] A ⊗[R] R[X] with toFunAlgHom and invFun$$

Lean4

/-- (Implementation detail)

The equivalence, ignoring the algebra structure, `(A ⊗[R] R[X]) ≃ A[X]`.
-/
def equiv : A ⊗[R] R[X] ≃ A[X] where
  toFun := toFunAlgHom R A
  invFun := invFun R A
  left_inv := left_inv R A
  right_inv := right_inv R A

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