Theorems · Theorem · linear algebra

TensorProduct.AlgebraTensorModule.rTensor_tensor

∀ (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} {P : Type uP} (P' : Type uP') [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N]
  [inst_9 : AddCommMonoid P] [inst_10 : Module A P] [inst_11 : AddCommMonoid P'] [inst_12 : Module A P']
  [inst_13 : Module R P] [inst_14 : IsScalarTower R A P] [inst_15 : Module R P'] [inst_16 : IsScalarTower R A P']
  (g : P →ₗ[A] P'),
  LinearMap.rTensor (TensorProduct R M N) g =
    ↑(TensorProduct.AlgebraTensorModule.assoc R A A P' M N) ∘ₗ
      TensorProduct.AlgebraTensorModule.map (LinearMap.rTensor M g) LinearMap.id ∘ₗ
        ↑(TensorProduct.AlgebraTensorModule.assoc R A A P M N).symm

Defined in

Mathlib.LinearAlgebra.TensorProduct.Tower

Cited by

0 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraAddCommMonoidModuleModuleIsScalarTowerAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModuleModuleIsScalarTowerModuleIsScalarTower