rTensor_tensor — Mathlib

English

Base change distributes over tensor products: A ⊗_R (M ⊗_R N) ≃_A (A ⊗_R M) ⊗_A (A ⊗_R N).

Русский

Изменение базы распределяет над тензорным произведением: A ⊗_R (M ⊗_R N) ≃_A (A ⊗_R M) ⊗_A (A ⊗_R N).

LaTeX

$$$A\otimes_R (M\otimes_R N) \cong_A (A\otimes_R M) \otimes_A (A\otimes_R N)$$$

Lean4

theorem rTensor_tensor [Module R P'] [IsScalarTower R A P'] (g : P →ₗ[A] P') :
    g.rTensor (M ⊗[R] N) = assoc R A A P' M N ∘ₗ map (g.rTensor M) id ∘ₗ (assoc R A A P M N).symm.toLinearMap :=
  TensorProduct.ext <| LinearMap.ext fun _ ↦ ext fun _ _ ↦ rfl

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