cancelBaseChange — Mathlib

English

Naturality of rTensor with respect to a linear map g: P → P': the equation g.rTensor(M⊗N) = assoc ∘ map(g.rTensor M) ∘ assoc^{-1}.

Русский

Естественность rTensor относительно линейного отображения g: P → P': g.rTensor(M⊗N) = assoc ∘ map(g.rTensor M) ∘ assoc^{-1}.

LaTeX

$$$g\,\mathrm{rTensor}_{R,A}(M\otimes_R N) = \text{assoc} \circ \bigl(g\,\mathrm{rTensor}_M\bigr) \circ \text{assoc}^{-1}$$$

Lean4

/-- `B`-linear equivalence between `M ⊗[A] (A ⊗[R] N)` and `M ⊗[R] N`.
In particular useful with `B = A`. -/
def cancelBaseChange : M ⊗[A] (A ⊗[R] N) ≃ₗ[B] M ⊗[R] N :=
  letI g : (M ⊗[A] A) ⊗[R] N ≃ₗ[B] M ⊗[R] N := congr (AlgebraTensorModule.rid A B M) (.refl R N)
  (assoc R A B M A N).symm ≪≫ₗ g

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