Associators and unitors for tensor products of modules over a commutative ring.

noncomputable def TensorProduct.lid (R : Type u_1) [CommSemiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] : TensorProduct R R M ≃ₗ[R] M

The base ring is a left identity for the tensor product of modules, up to linear equivalence.

Equations

• TensorProduct.lid R M = LinearEquiv.ofLinear (TensorProduct.lift (LinearMap.lsmul R M)) ((TensorProduct.mk R R M) 1) ⋯ ⋯

@[simp]

theorem TensorProduct.lid_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] (m : M) (r : R) : (TensorProduct.lid R M) (r ⊗ₜ[R] m) = r • m

@[simp]

theorem TensorProduct.lid_symm_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] (m : M) : (TensorProduct.lid R M).symm m = 1 ⊗ₜ[R] m

noncomputable def TensorProduct.rid (R : Type u_1) [CommSemiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] : TensorProduct R M R ≃ₗ[R] M

The base ring is a right identity for the tensor product of modules, up to linear equivalence.

Equations

• TensorProduct.rid R M = (TensorProduct.comm R M R).trans (TensorProduct.lid R M)

@[simp]

theorem TensorProduct.rid_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] (m : M) (r : R) : (TensorProduct.rid R M) (m ⊗ₜ[R] r) = r • m

@[simp]

theorem TensorProduct.rid_symm_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] (m : M) : (TensorProduct.rid R M).symm m = m ⊗ₜ[R] 1

theorem TensorProduct.lid_eq_rid (R : Type u_1) [CommSemiring R] : TensorProduct.lid R R = TensorProduct.rid R R

noncomputable def TensorProduct.lidOfCompatibleSMul (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) [AddCommMonoid M] [Module R M] [CommSemiring A] [Module A M] [Module R A] [SMulCommClass R A A] [CompatibleSMul R A A M] [CompatibleSMul A R A M] : TensorProduct R A M ≃ₗ[A] M

If the R- and A- action on A and M satisfy CompatibleSMul both ways, then A ⊗[R] M is canonically isomorphic to M.

Equations

• TensorProduct.lidOfCompatibleSMul R A M = (TensorProduct.equivOfCompatibleSMul R A A M).symm.trans (TensorProduct.lid A M)

theorem TensorProduct.lidOfCompatibleSMul_tmul (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) [AddCommMonoid M] [Module R M] [CommSemiring A] [Module A M] [Module R A] [SMulCommClass R A A] [CompatibleSMul R A A M] [CompatibleSMul A R A M] (a : A) (m : M) : (lidOfCompatibleSMul R A M) (a ⊗ₜ[R] m) = a • m

noncomputable def TensorProduct.assoc (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : TensorProduct R (TensorProduct R M N) P ≃ₗ[R] TensorProduct R M (TensorProduct R N P)

The associator for tensor product of R-modules, as a linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorProduct.assoc_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) : (TensorProduct.assoc R M N P) ((m ⊗ₜ[R] n) ⊗ₜ[R] p) = m ⊗ₜ[R] n ⊗ₜ[R] p

@[simp]

theorem TensorProduct.assoc_symm_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) : (TensorProduct.assoc R M N P).symm (m ⊗ₜ[R] n ⊗ₜ[R] p) = (m ⊗ₜ[R] n) ⊗ₜ[R] p

theorem TensorProduct.map_map_comp_assoc_eq {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (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

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.

theorem TensorProduct.map_map_assoc {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R (TensorProduct R M N) 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)

theorem TensorProduct.map_map_comp_assoc_symm_eq {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (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)

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).

theorem TensorProduct.map_map_assoc_symm {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R M (TensorProduct R N 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)

noncomputable def TensorProduct.leftComm (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : TensorProduct R M (TensorProduct R N P) ≃ₗ[R] TensorProduct R N (TensorProduct R M P)

A tensor product analogue of mul_left_comm.

Equations

• TensorProduct.leftComm R M N P = (TensorProduct.assoc R M N P).symm.trans ((TensorProduct.congr (TensorProduct.comm R M N) 1).trans (TensorProduct.assoc R N M P))

@[simp]

theorem TensorProduct.leftComm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) : (leftComm R M N P) (m ⊗ₜ[R] n ⊗ₜ[R] p) = n ⊗ₜ[R] m ⊗ₜ[R] p

@[simp]

theorem TensorProduct.leftComm_symm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) : (leftComm R M N P).symm (n ⊗ₜ[R] m ⊗ₜ[R] p) = m ⊗ₜ[R] n ⊗ₜ[R] p

noncomputable def TensorProduct.tensorTensorTensorComm (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) ≃ₗ[R] TensorProduct R (TensorProduct R M P) (TensorProduct R N Q)

This special case is worth defining explicitly since it is useful for defining multiplication on tensor products of modules carrying multiplications (e.g., associative rings, Lie rings, ...).

E.g., suppose M = P and N = Q and that M and N carry bilinear multiplications: M ⊗ M → M and N ⊗ N → N. Using map, we can define (M ⊗ M) ⊗ (N ⊗ N) → M ⊗ N which, when combined with this definition, yields a bilinear multiplication on M ⊗ N: (M ⊗ N) ⊗ (M ⊗ N) → M ⊗ N. In particular we could use this to define the multiplication in the TensorProduct.semiring instance (currently defined "by hand" using TensorProduct.mul).

See also mul_mul_mul_comm.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorProduct.tensorTensorTensorComm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (m : M) (n : N) (p : P) (q : Q) : (tensorTensorTensorComm R M N P Q) ((m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q) = (m ⊗ₜ[R] p) ⊗ₜ[R] n ⊗ₜ[R] q

@[simp]

theorem TensorProduct.tensorTensorTensorComm_symm (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] : (tensorTensorTensorComm R M N P Q).symm = tensorTensorTensorComm R M P N Q

theorem TensorProduct.tensorTensorTensorComm_comp_map (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] {V : Type u_13} {W : Type u_14} [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)

noncomputable def TensorProduct.tensorTensorTensorAssoc (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) ≃ₗ[R] TensorProduct R (TensorProduct R M (TensorProduct R N P)) Q

This special case is useful for describing the interplay between dualTensorHomEquiv and composition of linear maps.

E.g., composition of linear maps gives a map (M → N) ⊗ (N → P) → (M → P), and applying dual_tensor_hom_equiv.symm to the three hom-modules gives a map (M.dual ⊗ N) ⊗ (N.dual ⊗ P) → (M.dual ⊗ P), which agrees with the application of contractRight on N ⊗ N.dual after the suitable rebracketting.

Equations

• TensorProduct.tensorTensorTensorAssoc R M N P Q = (TensorProduct.assoc R (TensorProduct R M N) P Q).symm.trans (TensorProduct.congr (TensorProduct.assoc R M N P) 1)

@[simp]

theorem TensorProduct.tensorTensorTensorAssoc_tmul (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (m : M) (n : N) (p : P) (q : Q) : (tensorTensorTensorAssoc R M N P Q) ((m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q) = (m ⊗ₜ[R] n ⊗ₜ[R] p) ⊗ₜ[R] q

@[simp]

theorem TensorProduct.tensorTensorTensorAssoc_symm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (m : M) (n : N) (p : P) (q : Q) : (tensorTensorTensorAssoc R M N P Q).symm ((m ⊗ₜ[R] n ⊗ₜ[R] p) ⊗ₜ[R] q) = (m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q

theorem LinearMap.rTensor_tensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) : rTensor (TensorProduct R M N) g = ↑(TensorProduct.assoc R Q M N) ∘ₗ rTensor N (rTensor M g) ∘ₗ ↑(TensorProduct.assoc R P M N).symm

theorem LinearMap.lid_comp_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N →ₗ[R] R) : ↑(TensorProduct.lid R M) ∘ₗ rTensor M f = TensorProduct.lift (lsmul R M ∘ₗ f)