rTensor_baseChange — Mathlib

English

For AlgHom φ: A →_R B and t ∈ A ⊗_R M, and f: M →_R N, we have (φ.toLinearMap.rTensor N)(f.baseChange A t) = (f.baseChange B)(φ.toLinearMap.rTensor M t).

Русский

ДляAlg-гомоморфизма φ: A →_R B и t ∈ A ⊗_R M, выполняется (φ.toLinearMap.rTensor N)(f.baseChange A t) = (f.baseChange B)(φ.toLinearMap.rTensor M t).

LaTeX

$$$$ (\\phi^{\\mathrm{toLinearMap}}_{\\,R} \\; t) \\bigl(\\mathrm{baseChange}_A f (t)\\bigr) = \\mathrm{baseChange}_B f \\bigl(\\phi^{\\mathrm{toLinearMap}}_{\\,R} (t)\\bigr). $$$$

Lean4

theorem rTensor_baseChange (φ : A →ₐ[R] B) (t : A ⊗[R] M) (f : M →ₗ[R] N) :
    (φ.toLinearMap.rTensor N) (f.baseChange A t) = (f.baseChange B) (φ.toLinearMap.rTensor M t) := by
  simp [LinearMap.baseChange_eq_ltensor, ← LinearMap.comp_apply]

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