liftBaseChangeEquiv — Mathlib

English

For an algebra A over R and an R-module map l: M → N, the lifted map l.liftBaseChange behaves on simple tensors as l.liftBaseChange(x ⊗ y) = x ⋅ l(y).

Русский

Для модуля M над R и отображения l: M → N, поднятое отображение l.liftBaseChange действует на простые тензоры как l.liftBaseChange( x ⊗ y ) = x · l(y).

LaTeX

$$$l.liftBaseChange A (x \\otimes y) = x \\cdot l(y)$$$

Lean4

/-- If `M` is an `R`-module and `N` is an `A`-module, then `A`-linear maps `A ⊗[R] M →ₗ[A] N`
correspond to `R` linear maps `M →ₗ[R] N` by composing with `M → A ⊗ M`, `x ↦ 1 ⊗ x`.
-/
def liftBaseChangeEquiv : (M →ₗ[R] N) ≃ₗ[A] (A ⊗[R] M →ₗ[A] N) :=
  (LinearMap.ringLmapEquivSelf _ _ _).symm.trans (AlgebraTensorModule.lift.equiv _ _ _ _ _ _)

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