Mathlib.LinearAlgebra.TensorProduct.Associator

TensorProduct.lid_tmul theorem

(m : M) (r : R) : (TensorProduct.lid R M : R ⊗ M → M) (r ⊗ₜ m) = r • m

Full source

@[simp]
theorem lid_tmul (m : M) (r : R) : (TensorProduct.lid R M : R ⊗ M → M) (r ⊗ₜ m) = r • m :=
  rfl

Left Unitor Action on Pure Tensors: $\text{lid}_{R,M}(r \otimes m) = r \cdot m$

Informal description

For any module $M$ over a commutative ring $R$, the left unitor map $\text{lid}_{R,M} \colon R \otimes M \to M$ satisfies $\text{lid}_{R,M}(r \otimes m) = r \cdot m$ for all $r \in R$ and $m \in M$.

TensorProduct.lid_symm_apply theorem

(m : M) : (TensorProduct.lid R M).symm m = 1 ⊗ₜ m

Full source

@[simp]
theorem lid_symm_apply (m : M) : (TensorProduct.lid R M).symm m = 1 ⊗ₜ m :=
  rfl

Inverse of Left Unitor Maps Elements to Tensor with Unit

Informal description

For any module $M$ over a commutative ring $R$, the inverse of the left unitor isomorphism $\text{lid}_{R,M} : R \otimes_R M \to M$ satisfies $\text{lid}_{R,M}^{-1}(m) = 1 \otimes m$ for all $m \in M$.

TensorProduct.includeRight_lid theorem

 {S : Type*} [Semiring S] [Algebra R S] (m : R ⊗[R] M) :
  (1 : S) ⊗ₜ[R] (TensorProduct.lid R M) m = (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap) m

Full source

lemma includeRight_lid {S : Type*} [Semiring S] [Algebra R S] (m : R ⊗[R] M) :
    (1 : S) ⊗ₜ[R] (TensorProduct.lid R M) m =
      (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap) m := by
  suffices ∀ m, (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap).comp
    (TensorProduct.lid R M).symm.toLinearMap m = 1 ⊗ₜ[R] m by
    simp [← this]
  intros; simp

Right Tensor Inclusion with Left Unitor Identity

Informal description

Let $R$ be a commutative ring, $M$ be an $R$-module, and $S$ be a semiring with an $R$-algebra structure. For any element $m$ in the tensor product $R \otimes_R M$, the following equality holds: $$(1_S) \otimes_R (\text{lid}_{R} M)(m) = (\text{rTensor}_M (\text{algHom}_{R} R S))(m)$$ where: - $\text{lid}_{R} M$ is the left unitor isomorphism $R \otimes_R M \cong M$, - $1_S$ is the multiplicative identity in $S$, - $\text{rTensor}_M$ denotes the right tensor product with $M$, - $\text{algHom}_{R} R S$ is the canonical $R$-algebra homomorphism from $R$ to $S$.

TensorProduct.rid_tmul theorem

(m : M) (r : R) : (TensorProduct.rid R M) (m ⊗ₜ r) = r • m

Full source

@[simp]
theorem rid_tmul (m : M) (r : R) : (TensorProduct.rid R M) (m ⊗ₜ r) = r • m :=
  rfl

Right Unitor Maps Tensor with Scalar to Scalar Multiplication

Informal description

For any module $M$ over a commutative ring $R$, the right unitor isomorphism $\text{rid}_{R,M} : M \otimes_R R \to M$ satisfies $\text{rid}_{R,M}(m \otimes r) = r \cdot m$ for all $m \in M$ and $r \in R$.

TensorProduct.rid_symm_apply theorem

(m : M) : (TensorProduct.rid R M).symm m = m ⊗ₜ 1

Full source

@[simp]
theorem rid_symm_apply (m : M) : (TensorProduct.rid R M).symm m = m ⊗ₜ 1 :=
  rfl

Inverse Right Unitor Maps Element to Tensor with Identity

Informal description

For any $R$-module $M$ and any element $m \in M$, the inverse of the right unitor isomorphism $\text{rid}_R M : M \otimes_R R \cong M$ satisfies $(\text{rid}_R M)^{-1}(m) = m \otimes 1$, where $1$ is the multiplicative identity in $R$.

TensorProduct.lid_eq_rid theorem

: TensorProduct.lid R R = TensorProduct.rid R R

Full source

theorem lid_eq_rid : TensorProduct.lid R R = TensorProduct.rid R R :=
  LinearEquiv.toLinearMap_injective <| ext' mul_comm

Left and Right Unitor Isomorphisms Coincide for $R \otimes_R R$

Informal description

For a commutative ring $R$, the left unitor isomorphism $\text{lid}_{R,R} \colon R \otimes_R R \to R$ is equal to the right unitor isomorphism $\text{rid}_{R,R} \colon R \otimes_R R \to R$.

TensorProduct.lidOfCompatibleSMul_tmul theorem

(a m) : lidOfCompatibleSMul R A M (a ⊗ₜ[R] m) = a • m

Full source

theorem lidOfCompatibleSMul_tmul (a m) : lidOfCompatibleSMul R A M (a ⊗ₜ[R] m) = a • m := rfl

Left unit isomorphism acts on pure tensors as $a \otimes m \mapsto a \cdot m$

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $A$-module. For any $a \in A$ and $m \in M$, the left unit isomorphism $\text{lidOfCompatibleSMul}_{R,A,M}$ satisfies \[ \text{lidOfCompatibleSMul}_{R,A,M}(a \otimes_R m) = a \cdot m, \] where $\cdot$ denotes the scalar multiplication of $A$ on $M$.

TensorProduct.assoc_tmul theorem

(m : M) (n : N) (p : P) : (TensorProduct.assoc R M N P) (m ⊗ₜ n ⊗ₜ p) = m ⊗ₜ (n ⊗ₜ p)

Full source

@[simp]
theorem assoc_tmul (m : M) (n : N) (p : P) :
    (TensorProduct.assoc R M N P) (m ⊗ₜ nm ⊗ₜ n ⊗ₜ p) = m ⊗ₜ (n ⊗ₜ p) :=
  rfl

Associator Acts on Pure Tensors as $((m \otimes n) \otimes p) \mapsto m \otimes (n \otimes p)$

Informal description

Let $R$ be a commutative ring, and let $M$, $N$, and $P$ be $R$-modules. The associator isomorphism $\text{assoc}_{R,M,N,P} \colon (M \otimes_R N) \otimes_R P \to M \otimes_R (N \otimes_R P)$ satisfies \[ \text{assoc}_{R,M,N,P}((m \otimes n) \otimes p) = m \otimes (n \otimes p) \] for all $m \in M$, $n \in N$, and $p \in P$.

TensorProduct.assoc_symm_tmul theorem

(m : M) (n : N) (p : P) : (TensorProduct.assoc R M N P).symm (m ⊗ₜ (n ⊗ₜ p)) = m ⊗ₜ n ⊗ₜ p

Full source

@[simp]
theorem assoc_symm_tmul (m : M) (n : N) (p : P) :
    (TensorProduct.assoc R M N P).symm (m ⊗ₜ (n ⊗ₜ p)) = m ⊗ₜ nm ⊗ₜ n ⊗ₜ p :=
  rfl

Inverse Associator Acts on Pure Tensors as $(m \otimes n) \otimes p \mapsto m \otimes (n \otimes p)$

Informal description

Let $R$ be a commutative ring, and let $M$, $N$, and $P$ be $R$-modules. The inverse of the associator isomorphism $\text{assoc}_{R,M,N,P} \colon (M \otimes_R N) \otimes_R P \to M \otimes_R (N \otimes_R P)$ satisfies \[ \text{assoc}_{R,M,N,P}^{-1}(m \otimes (n \otimes p)) = (m \otimes n) \otimes p \] for all $m \in M$, $n \in N$, and $p \in P$.

TensorProduct.map_map_comp_assoc_eq theorem

 (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :
  map f (map g h) ∘ₗ TensorProduct.assoc R M N P = TensorProduct.assoc R Q S T ∘ₗ map (map f g) h

Full source

/-- Given linear maps `f : M → Q`, `g : N → S`, and `h : P → T`, if we identify `(M ⊗ N) ⊗ P`
with `M ⊗ (N ⊗ P)` and `(Q ⊗ S) ⊗ T` with `Q ⊗ (S ⊗ T)`, then this lemma states that
`f ⊗ (g ⊗ h) = (f ⊗ g) ⊗ h`. -/
lemma map_map_comp_assoc_eq (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :
    mapmap f (map g h) ∘ₗ TensorProduct.assoc R M N P =
      TensorProduct.assocTensorProduct.assoc R Q S T ∘ₗ map (map f g) h :=
  ext <| ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => LinearMap.ext fun _ => rfl

Naturality of Associator with Respect to Tensor Product of Linear Maps

Informal description

Let $R$ be a commutative ring, and let $M$, $N$, $P$, $Q$, $S$, $T$ be $R$-modules. Given linear maps $f \colon M \to Q$, $g \colon N \to S$, and $h \colon P \to T$, the following diagram commutes: \[ (f \otimes (g \otimes h)) \circ \text{assoc}_{R,M,N,P} = \text{assoc}_{R,Q,S,T} \circ ((f \otimes g) \otimes h), \] where $\text{assoc}_{R,A,B,C} \colon (A \otimes_R B) \otimes_R C \to A \otimes_R (B \otimes_R C)$ is the associator isomorphism for any $R$-modules $A$, $B$, $C$.

TensorProduct.map_map_assoc theorem

 (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : (M ⊗[R] N) ⊗[R] P) :
  map f (map g h) (TensorProduct.assoc R M N P x) = TensorProduct.assoc R Q S T (map (map f g) h x)

Full source

lemma map_map_assoc (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : (M ⊗[R] N) ⊗[R] P) :
    map f (map g h) (TensorProduct.assoc R M N P x) =
      TensorProduct.assoc R Q S T (map (map f g) h x) :=
  DFunLike.congr_fun (map_map_comp_assoc_eq _ _ _) _

Naturality of Associator with Respect to Tensor Product of Linear Maps

Informal description

Let $R$ be a commutative ring, and let $M$, $N$, $P$, $Q$, $S$, $T$ be $R$-modules. Given linear maps $f \colon M \to Q$, $g \colon N \to S$, and $h \colon P \to T$, the following diagram commutes: \[ \begin{tikzcd} (M \otimes_R N) \otimes_R P \arrow[r, "{\text{assoc}_{R,M,N,P}}"] \arrow[d, "{(f \otimes g) \otimes h}"'] & M \otimes_R (N \otimes_R P) \arrow[d, "{f \otimes (g \otimes h)}"] \\ (Q \otimes_R S) \otimes_R T \arrow[r, "{\text{assoc}_{R,Q,S,T}}"'] & Q \otimes_R (S \otimes_R T) \end{tikzcd} \] That is, for any $x \in (M \otimes_R N) \otimes_R P$, we have \[ f \otimes (g \otimes h) \left( \text{assoc}_{R,M,N,P}(x) \right) = \text{assoc}_{R,Q,S,T} \left( (f \otimes g) \otimes h (x) \right), \] where $\text{assoc}_{R,A,B,C} \colon (A \otimes_R B) \otimes_R C \to A \otimes_R (B \otimes_R C)$ is the associator isomorphism for any $R$-modules $A$, $B$, $C$.

TensorProduct.map_map_comp_assoc_symm_eq theorem

 (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :
  map (map f g) h ∘ₗ (TensorProduct.assoc R M N P).symm = (TensorProduct.assoc R Q S T).symm ∘ₗ map f (map g h)

Full source

/-- Given linear maps `f : M → Q`, `g : N → S`, and `h : P → T`, if we identify `M ⊗ (N ⊗ P)`
with `(M ⊗ N) ⊗ P` and `Q ⊗ (S ⊗ T)` with `(Q ⊗ S) ⊗ T`, then this lemma states that
`(f ⊗ g) ⊗ h = f ⊗ (g ⊗ h)`. -/
lemma map_map_comp_assoc_symm_eq (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :
    mapmap (map f g) h ∘ₗ (TensorProduct.assoc R M N P).symm =
      (TensorProduct.assoc R Q S T).symm ∘ₗ map f (map g h) :=
  ext <| LinearMap.ext fun _ => ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => rfl

Naturality of the Associator Symmetry for Tensor Products of Linear Maps

Informal description

Let $R$ be a commutative ring, and let $M, N, P, Q, S, T$ be $R$-modules. Given linear maps $f \colon M \to Q$, $g \colon N \to S$, and $h \colon P \to T$, the following diagram commutes: \[ \begin{tikzcd} (M \otimes_R N) \otimes_R P \arrow[r, "{(f \otimes g) \otimes h}"] \arrow[d, "\text{assoc}_{M,N,P}^{-1}"'] & (Q \otimes_R S) \otimes_R T \arrow[d, "\text{assoc}_{Q,S,T}^{-1}"] \\ M \otimes_R (N \otimes_R P) \arrow[r, "{f \otimes (g \otimes h)}"'] & Q \otimes_R (S \otimes_R T) \end{tikzcd} \] That is, $(f \otimes (g \otimes h)) \circ \text{assoc}_{M,N,P}^{-1} = \text{assoc}_{Q,S,T}^{-1} \circ ((f \otimes g) \otimes h)$.

TensorProduct.map_map_assoc_symm theorem

 (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : M ⊗[R] (N ⊗[R] P)) :
  map (map f g) h ((TensorProduct.assoc R M N P).symm x) = (TensorProduct.assoc R Q S T).symm (map f (map g h) x)

Full source

lemma map_map_assoc_symm (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : M ⊗[R] (N ⊗[R] P)) :
    map (map f g) h ((TensorProduct.assoc R M N P).symm x) =
      (TensorProduct.assoc R Q S T).symm (map f (map g h) x) :=
  DFunLike.congr_fun (map_map_comp_assoc_symm_eq _ _ _) _

Naturality of Associator Symmetry for Tensor Products of Linear Maps (Pointwise Version)

Informal description

Let $R$ be a commutative ring, and let $M, N, P, Q, S, T$ be $R$-modules. Given linear maps $f \colon M \to Q$, $g \colon N \to S$, and $h \colon P \to T$, for any element $x \in M \otimes_R (N \otimes_R P)$, we have $$(f \otimes g) \otimes h \circ \text{assoc}_{M,N,P}^{-1}(x) = \text{assoc}_{Q,S,T}^{-1} \circ f \otimes (g \otimes h)(x).$$

TensorProduct.leftComm_tmul theorem

(m : M) (n : N) (p : P) : leftComm R M N P (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p)

Full source

@[simp]
theorem leftComm_tmul (m : M) (n : N) (p : P) : leftComm R M N P (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p) :=
  rfl

Left Commutativity Isomorphism for Tensor Products

Informal description

For any elements $m \in M$, $n \in N$, and $p \in P$ in modules over a commutative ring $R$, the left commutativity isomorphism $\text{leftComm}_{R,M,N,P}$ satisfies \[ \text{leftComm}_{R,M,N,P}(m \otimes (n \otimes p)) = n \otimes (m \otimes p). \]

TensorProduct.leftComm_symm_tmul theorem

(m : M) (n : N) (p : P) : (leftComm R M N P).symm (n ⊗ₜ (m ⊗ₜ p)) = m ⊗ₜ (n ⊗ₜ p)

Full source

@[simp]
theorem leftComm_symm_tmul (m : M) (n : N) (p : P) :
    (leftComm R M N P).symm (n ⊗ₜ (m ⊗ₜ p)) = m ⊗ₜ (n ⊗ₜ p) :=
  rfl

Inverse of Left Commutativity Isomorphism for Tensor Products

Informal description

For any elements $m \in M$, $n \in N$, and $p \in P$ in modules over a commutative ring $R$, the inverse of the left commutativity isomorphism `leftComm` satisfies $$(\text{leftComm}_{R,M,N,P})^{-1}(n \otimes (m \otimes p)) = m \otimes (n \otimes p).$$

TensorProduct.tensorTensorTensorComm_tmul theorem

 (m : M) (n : N) (p : P) (q : Q) : tensorTensorTensorComm R M N P Q (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ p ⊗ₜ (n ⊗ₜ q)

Full source

@[simp]
theorem tensorTensorTensorComm_tmul (m : M) (n : N) (p : P) (q : Q) :
    tensorTensorTensorComm R M N P Q (m ⊗ₜ nm ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ pm ⊗ₜ p ⊗ₜ (n ⊗ₜ q) :=
  rfl

Tensor Tensor Tensor Commutativity Isomorphism: $m \otimes n \otimes (p \otimes q) \mapsto m \otimes p \otimes (n \otimes q)$

Informal description

For any elements $m \in M$, $n \in N$, $p \in P$, and $q \in Q$ in modules over a commutative ring $R$, the tensor tensor tensor commutativity isomorphism satisfies \[ \text{tensorTensorTensorComm}_{R,M,N,P,Q}(m \otimes n \otimes (p \otimes q)) = m \otimes p \otimes (n \otimes q). \]

TensorProduct.tensorTensorTensorComm_symm theorem

: (tensorTensorTensorComm R M N P Q).symm = tensorTensorTensorComm R M P N Q

Full source

@[simp]
theorem tensorTensorTensorComm_symm :
    (tensorTensorTensorComm R M N P Q).symm = tensorTensorTensorComm R M P N Q :=
  rfl

Inverse of Tensor Commutativity Isomorphism Equals Commutativity Isomorphism with Swapped Factors

Informal description

Let $R$ be a commutative ring and let $M$, $N$, $P$, $Q$ be $R$-modules. The inverse of the tensor commutativity isomorphism $$\text{tensorTensorTensorComm}_{R,M,N,P,Q}$$ is equal to the tensor commutativity isomorphism $$\text{tensorTensorTensorComm}_{R,M,P,N,Q}.$$

TensorProduct.tensorTensorTensorComm_comp_map theorem

 {V W : Type*} [AddCommMonoid V] [AddCommMonoid W] [Module R V] [Module R W] (f : M →ₗ[R] S) (g : N →ₗ[R] T)
  (h : P →ₗ[R] V) (j : Q →ₗ[R] W) :
  tensorTensorTensorComm R S T V W ∘ₗ map (map f g) (map h j) =
    map (map f h) (map g j) ∘ₗ tensorTensorTensorComm R M N P Q

Full source

theorem tensorTensorTensorComm_comp_map {V W : Type*}
    [AddCommMonoid V] [AddCommMonoid W] [Module R V] [Module R W]
    (f : M →ₗ[R] S) (g : N →ₗ[R] T) (h : P →ₗ[R] V) (j : Q →ₗ[R] W) :
    tensorTensorTensorCommtensorTensorTensorComm R S T V W ∘ₗ map (map f g) (map h j) =
      mapmap (map f h) (map g j) ∘ₗ tensorTensorTensorComm R M N P Q :=
  ext_fourfold' fun _ _ _ _ => rfl

Naturality of Commutativity Isomorphism for Quadruple Tensor Products with Respect to Linear Maps

Informal description

Let $R$ be a commutative ring, and let $M$, $N$, $P$, $Q$, $S$, $T$, $V$, $W$ be $R$-modules. Given $R$-linear maps $f: M \to S$, $g: N \to T$, $h: P \to V$, and $j: Q \to W$, the following diagram commutes: $$ \text{tensorTensorTensorComm}_{R,S,T,V,W} \circ \text{map}(\text{map}(f, g), \text{map}(h, j)) = \text{map}(\text{map}(f, h), \text{map}(g, j)) \circ \text{tensorTensorTensorComm}_{R,M,N,P,Q} $$ where $\text{map}$ denotes the induced linear map on tensor products and $\text{tensorTensorTensorComm}$ is the commutativity isomorphism for quadruple tensor products.

TensorProduct.tensorTensorTensorAssoc_tmul theorem

 (m : M) (n : N) (p : P) (q : Q) : tensorTensorTensorAssoc R M N P Q (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q

Full source

@[simp]
theorem tensorTensorTensorAssoc_tmul (m : M) (n : N) (p : P) (q : Q) :
    tensorTensorTensorAssoc R M N P Q (m ⊗ₜ nm ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ (n ⊗ₜ p)m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q :=
  rfl

Associator isomorphism for quadruple tensor product

Informal description

Let $R$ be a commutative ring and let $M$, $N$, $P$, $Q$ be $R$-modules. For any elements $m \in M$, $n \in N$, $p \in P$, $q \in Q$, the associator isomorphism $$\text{tensorTensorTensorAssoc}_{R,M,N,P,Q}(m \otimes n \otimes (p \otimes q)) = m \otimes (n \otimes p) \otimes q$$ holds, where $\otimes$ denotes the tensor product over $R$.

TensorProduct.tensorTensorTensorAssoc_symm_tmul theorem

 (m : M) (n : N) (p : P) (q : Q) : (tensorTensorTensorAssoc R M N P Q).symm (m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q) = m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)

Full source

@[simp]
theorem tensorTensorTensorAssoc_symm_tmul (m : M) (n : N) (p : P) (q : Q) :
    (tensorTensorTensorAssoc R M N P Q).symm (m ⊗ₜ (n ⊗ₜ p)m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q) = m ⊗ₜ nm ⊗ₜ n ⊗ₜ (p ⊗ₜ q) :=
  rfl

Inverse Associator Identity for Quadruple Tensor Product

Informal description

For any elements $m \in M$, $n \in N$, $p \in P$, and $q \in Q$ in modules over a commutative ring $R$, the inverse of the associator isomorphism satisfies $$(tensorTensorTensorAssoc_{R,M,N,P,Q})^{-1}(m \otimes (n \otimes p) \otimes q) = m \otimes n \otimes (p \otimes q).$$

LinearMap.rTensor_tensor theorem

 : rTensor (M ⊗[R] N) g = TensorProduct.assoc R Q M N ∘ₗ rTensor N (rTensor M g) ∘ₗ (TensorProduct.assoc R P M N).symm

Full source

theorem rTensor_tensor : rTensor (M ⊗[R] N) g =
    TensorProduct.assocTensorProduct.assoc R Q M N ∘ₗ rTensor N (rTensor M g) ∘ₗ (TensorProduct.assoc R P M N).symm :=
  TensorProduct.ext <| LinearMap.ext fun _ ↦ TensorProduct.ext rfl

Composition Identity for Right Tensor Product with Associators

Informal description

Let $R$ be a commutative ring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any linear map $g : P \to_{[R]} Q$, the right tensor product map $\text{rTensor}_{M \otimes_R N}(g)$ is equal to the composition of the associator isomorphism $\text{assoc}_{R,Q,M,N}$, the iterated right tensor product map $\text{rTensor}_N(\text{rTensor}_M(g))$, and the inverse of the associator isomorphism $\text{assoc}_{R,P,M,N}^{-1}$. In symbols: $$\text{rTensor}_{M \otimes_R N}(g) = \text{assoc}_{R,Q,M,N} \circ \text{rTensor}_N(\text{rTensor}_M(g)) \circ \text{assoc}_{R,P,M,N}^{-1}.$$

LinearMap.lid_comp_rTensor theorem

(f : N →ₗ[R] R) : (TensorProduct.lid R M).comp (rTensor M f) = lift ((lsmul R M).comp f)

Full source

theorem lid_comp_rTensor (f : N →ₗ[R] R) :
    (TensorProduct.lid R M).comp (rTensor M f) = lift ((lsmul R M).comp f) := ext' fun _ _ ↦ rfl

Composition Identity for Left Unitor and Right Tensor Map

Informal description

For any linear map $f \colon N \to R$ over a commutative ring $R$, the composition of the left unitor isomorphism $\text{lid}_R M$ with the right tensor product map $\text{rTensor}_M f$ is equal to the lifting of the composition of the scalar multiplication map $\text{lsmul}_R M$ with $f$. In symbols: $$(\text{lid}_R M) \circ (\text{rTensor}_M f) = \text{lift} ((\text{lsmul}_R M) \circ f).$$