mathlib documentation

linear_algebra.tensor_product

Tensor product of modules over commutative semirings. #

This file constructs the tensor product of modules over commutative semirings. Given a semiring R and modules over it M and N, the standard construction of the tensor product is tensor_product R M N. It is also a module over R.

It comes with a canonical bilinear map M → N → tensor_product R M N.

Given any bilinear map M → N → P, there is a unique linear map tensor_product R M N → P whose composition with the canonical bilinear map M → N → tensor_product R M N is the given bilinear map M → N → P.

We start by proving basic lemmas about bilinear maps.

Notations #

This file uses the localized notation M ⊗ N and M ⊗[R] N for tensor_product R M N, as well as m ⊗ₜ n and m ⊗ₜ[R] n for tensor_product.tmul R m n.

Tags #

bilinear, tensor, tensor product

inductive tensor_product.eqv (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
free_add_monoid (M × N)free_add_monoid (M × N) → Prop

The relation on free_add_monoid (M × N) that generates a congruence whose quotient is the tensor product.

def tensor_product (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
Type (max u_4 u_5)

The tensor product of two modules M and N over the same commutative semiring R. The localized notations are M ⊗ N and M ⊗[R] N, accessed by open_locale tensor_product.

Equations
@[instance]
def tensor_product.add_comm_semigroup {R : Type u_1} [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
Equations
@[instance]
def tensor_product.inhabited {R : Type u_1} [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
Equations
def tensor_product.tmul (R : Type u_1) [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (m : M) (n : N) :
M N

The canonical function M → N → M ⊗ N. The localized notations are m ⊗ₜ n and m ⊗ₜ[R] n, accessed by open_locale tensor_product.

Equations
theorem tensor_product.induction_on {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] {C : M N → Prop} (z : M N) (C0 : C 0) (C1 : ∀ {x : M} {y : N}, C (x ⊗ₜ[R] y)) (Cp : ∀ {x y : M N}, C xC yC (x + y)) :
C z
@[simp]
theorem tensor_product.zero_tmul {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (n : N) :
0 ⊗ₜ[R] n = 0
theorem tensor_product.add_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (m₁ m₂ : M) (n : N) :
(m₁ + m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n + m₂ ⊗ₜ[R] n
@[simp]
theorem tensor_product.tmul_zero {R : Type u_1} [comm_semiring R] {M : Type u_4} (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (m : M) :
m ⊗ₜ[R] 0 = 0
theorem tensor_product.tmul_add {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (m : M) (n₁ n₂ : N) :
m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂
@[class]
structure tensor_product.compatible_smul (R : Type u_1) [comm_semiring R] (R' : Type u_2) [monoid R'] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [distrib_mul_action R' N] :
Type

A typeclass for has_scalar structures which can be moved across a tensor product.

This typeclass is generated automatically from a is_scalar_tower instance, but exists so that we can also add an instance for add_comm_group.int_module, allowing z • to be moved even if R does not support negation.

Note that module R' (M ⊗[R] N) is available even without this typeclass on R'; it's only needed if tensor_product.smul_tmul, tensor_product.smul_tmul', or tensor_product.tmul_smul is used.

Instances
@[instance]
def tensor_product.compatible_smul.is_scalar_tower {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [has_scalar R' R] [is_scalar_tower R' R M] [distrib_mul_action R' N] [is_scalar_tower R' R N] :

Note that this provides the default compatible_smul R R M N instance through mul_action.is_scalar_tower.left.

Equations
theorem tensor_product.smul_tmul {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [distrib_mul_action R' N] [tensor_product.compatible_smul R R' M N] (r : R') (m : M) (n : N) :
(r m) ⊗ₜ[R] n = m ⊗ₜ[R] (r n)

smul can be moved from one side of the product to the other .

def tensor_product.smul.aux {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] {R' : Type u_2} [has_scalar R' M] (r : R') :

Auxiliary function to defining scalar multiplication on tensor product.

Equations
theorem tensor_product.smul.aux_of {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] {R' : Type u_2} [has_scalar R' M] (r : R') (m : M) (n : N) :
@[instance]
def tensor_product.left_has_scalar {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] :
has_scalar R' (M N)

Given two modules over a commutative semiring R, if one of the factors carries a (distributive) action of a second type of scalars R', which commutes with the action of R, then the tensor product (over R) carries an action of R'.

This instance defines this R' action in the case that it is the left module which has the R' action. Two natural ways in which this situation arises are:

  • Extension of scalars
  • A tensor product of a group representation with a module not carrying an action

Note that in the special case that R = R', since R is commutative, we just get the usual scalar action on a tensor product of two modules. This special case is important enough that, for performance reasons, we define it explicitly below.

Equations
@[instance]
def tensor_product.has_scalar {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
has_scalar R (M N)
Equations
theorem tensor_product.smul_zero {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] (r : R') :
r 0 = 0
theorem tensor_product.smul_add {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] (r : R') (x y : M N) :
r (x + y) = r x + r y
theorem tensor_product.zero_smul {R : Type u_1} [comm_semiring R] {R'' : Type u_3} [semiring R''] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [module R'' M] [smul_comm_class R R'' M] (x : M N) :
0 x = 0
theorem tensor_product.one_smul {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] (x : M N) :
1 x = x
theorem tensor_product.add_smul {R : Type u_1} [comm_semiring R] {R'' : Type u_3} [semiring R''] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [module R'' M] [smul_comm_class R R'' M] (r s : R'') (x : M N) :
(r + s) x = r x + s x
@[instance]
def tensor_product.add_comm_monoid {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
Equations
@[instance]
def tensor_product.left_distrib_mul_action {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] :
Equations
theorem tensor_product.smul_tmul' {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] (r : R') (m : M) (n : N) :
r m ⊗ₜ[R] n = (r m) ⊗ₜ[R] n
@[simp]
theorem tensor_product.tmul_smul {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] [distrib_mul_action R' N] [tensor_product.compatible_smul R R' M N] (r : R') (x : M) (y : N) :
x ⊗ₜ[R] (r y) = r x ⊗ₜ[R] y
@[instance]
def tensor_product.left_module {R : Type u_1} [comm_semiring R] {R'' : Type u_3} [semiring R''] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [module R'' M] [smul_comm_class R R'' M] :
module R'' (M N)
Equations
@[instance]
def tensor_product.module {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
module R (M N)
Equations
@[instance]
def tensor_product.is_scalar_tower_left {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] {R'₂ : Type u_9} [monoid R'₂] [distrib_mul_action R'₂ M] [smul_comm_class R R'₂ M] [has_scalar R'₂ R'] [is_scalar_tower R'₂ R' M] :
is_scalar_tower R'₂ R' (M N)

is_scalar_tower R'₂ R' M implies is_scalar_tower R'₂ R' (M ⊗[R] N)

@[instance]
def tensor_product.is_scalar_tower_right {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] {R'₂ : Type u_9} [monoid R'₂] [distrib_mul_action R'₂ M] [smul_comm_class R R'₂ M] [has_scalar R'₂ R'] [distrib_mul_action R'₂ N] [distrib_mul_action R' N] [tensor_product.compatible_smul R R'₂ M N] [tensor_product.compatible_smul R R' M N] [is_scalar_tower R'₂ R' N] :
is_scalar_tower R'₂ R' (M N)

is_scalar_tower R'₂ R' N implies is_scalar_tower R'₂ R' (M ⊗[R] N)

@[instance]
def tensor_product.is_scalar_tower {R : Type u_1} [comm_semiring R] {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] [distrib_mul_action R' M] [smul_comm_class R R' M] [has_scalar R' R] [is_scalar_tower R' R M] :
is_scalar_tower R' R (M N)

A short-cut instance for the common case, where the requirements for the compatible_smul instances are sufficient.

def tensor_product.mk (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :

The canonical bilinear map M → N → M ⊗[R] N.

Equations
@[simp]
theorem tensor_product.mk_apply {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (m : M) (n : N) :
theorem tensor_product.ite_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (x₁ : M) (x₂ : N) (P : Prop) [decidable P] :
ite P x₁ 0 ⊗ₜ[R] x₂ = ite P (x₁ ⊗ₜ[R] x₂) 0
theorem tensor_product.tmul_ite {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (x₁ : M) (x₂ : N) (P : Prop) [decidable P] :
x₁ ⊗ₜ[R] ite P x₂ 0 = ite P (x₁ ⊗ₜ[R] x₂) 0
theorem tensor_product.sum_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] {α : Type u_2} (s : finset α) (m : α → M) (n : N) :
(∑ (a : α) in s, m a) ⊗ₜ[R] n = ∑ (a : α) in s, m a ⊗ₜ[R] n
theorem tensor_product.tmul_sum {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (m : M) {α : Type u_2} (s : finset α) (n : α → N) :
m ⊗ₜ[R] ∑ (a : α) in s, n a = ∑ (a : α) in s, m ⊗ₜ[R] n a
theorem tensor_product.span_tmul_eq_top (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
submodule.span R {t : M N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t} =

The simple (aka pure) elements span the tensor product.

def tensor_product.lift_aux {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) :
M N →+ P

Auxiliary function to constructing a linear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations
theorem tensor_product.lift_aux_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
@[simp]
theorem tensor_product.lift_aux.smul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {f : M →ₗ[R] N →ₗ[R] P} (r : R) (x : M N) :
def tensor_product.lift {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) :
M N →ₗ[R] P

Constructing a linear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations
@[simp]
theorem tensor_product.lift.tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :
@[simp]
theorem tensor_product.lift.tmul' {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :
theorem tensor_product.ext' {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {g h : M N →ₗ[R] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) :
g = h
theorem tensor_product.lift.unique {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {f : M →ₗ[R] N →ₗ[R] P} {g : M N →ₗ[R] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f x) y) :
theorem tensor_product.lift_mk {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
theorem tensor_product.lift_compr₂ {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] {f : M →ₗ[R] N →ₗ[R] P} (g : P →ₗ[R] Q) :
theorem tensor_product.lift_mk_compr₂ {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M N →ₗ[R] P) :
theorem tensor_product.ext {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {g h : M N →ₗ[R] P} (H : (tensor_product.mk R M N).compr₂ g = (tensor_product.mk R M N).compr₂ h) :
g = h

This used to be an @[ext] lemma, but it fails very slowly when the ext tactic tries to apply it in some cases, notably when one wants to show equality of two linear maps. The @[ext] attribute is now added locally where it is needed. Using this as the @[ext] lemma instead of tensor_product.ext' allows ext to apply lemmas specific to M →ₗ _ and N →ₗ _.

See note [partially-applied ext lemmas].

def tensor_product.uncurry (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :

Linearly constructing a linear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations
@[simp]
theorem tensor_product.uncurry_apply {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
((tensor_product.uncurry R M N P) f) (m ⊗ₜ[R] n) = (f m) n
def tensor_product.lift.equiv (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :

A linear equivalence constructing a linear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations
@[simp]
theorem tensor_product.lift.equiv_apply (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
((tensor_product.lift.equiv R M N P) f) (m ⊗ₜ[R] n) = (f m) n
@[simp]
theorem tensor_product.lift.equiv_symm_apply (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M N →ₗ[R] P) (m : M) (n : N) :
((((tensor_product.lift.equiv R M N P).symm) f) m) n = f (m ⊗ₜ[R] n)
def tensor_product.lcurry (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :

Given a linear map M ⊗ N → P, compose it with the canonical bilinear map M → N → M ⊗ N to form a bilinear map M → N → P.

Equations
@[simp]
theorem tensor_product.lcurry_apply {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M N →ₗ[R] P) (m : M) (n : N) :
(((tensor_product.lcurry R M N P) f) m) n = f (m ⊗ₜ[R] n)
def tensor_product.curry {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M N →ₗ[R] P) :

Given a linear map M ⊗ N → P, compose it with the canonical bilinear map M → N → M ⊗ N to form a bilinear map M → N → P.

Equations
@[simp]
theorem tensor_product.curry_apply {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M N →ₗ[R] P) (m : M) (n : N) :
theorem tensor_product.curry_injective {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
theorem tensor_product.ext_threefold {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] {g h : M N P →ₗ[R] Q} (H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] y ⊗ₜ[R] z) = h (x ⊗ₜ[R] y ⊗ₜ[R] z)) :
g = h
theorem tensor_product.ext_fourfold {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [module R M] [module R N] [module R P] [module R Q] [module R S] {g h : M N P Q →ₗ[R] S} (H : ∀ (w : M) (x : N) (y : P) (z : Q), g (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) = h (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)) :
g = h
def tensor_product.lid (R : Type u_1) [comm_semiring R] (M : Type u_4) [add_comm_monoid M] [module R M] :
R M ≃ₗ[R] M

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

Equations
@[simp]
theorem tensor_product.lid_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} [add_comm_monoid M] [module R M] (m : M) (r : R) :
@[simp]
theorem tensor_product.lid_symm_apply {R : Type u_1} [comm_semiring R] {M : Type u_4} [add_comm_monoid M] [module R M] (m : M) :
def tensor_product.comm (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
M N ≃ₗ[R] N M

The tensor product of modules is commutative, up to linear equivalence.

Equations
@[simp]
theorem tensor_product.comm_tmul (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (m : M) (n : N) :
@[simp]
theorem tensor_product.comm_symm_tmul (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (m : M) (n : N) :
def tensor_product.rid (R : Type u_1) [comm_semiring R] (M : Type u_4) [add_comm_monoid M] [module R M] :
M R ≃ₗ[R] M

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

Equations
@[simp]
theorem tensor_product.rid_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} [add_comm_monoid M] [module R M] (m : M) (r : R) :
@[simp]
theorem tensor_product.rid_symm_apply {R : Type u_1} [comm_semiring R] {M : Type u_4} [add_comm_monoid M] [module R M] (m : M) :
def tensor_product.assoc (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
M N P ≃ₗ[R] M (N P)

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

Equations
@[simp]
theorem tensor_product.assoc_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (m : M) (n : N) (p : P) :
@[simp]
theorem tensor_product.assoc_symm_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (m : M) (n : N) (p : P) :
def tensor_product.map {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
M N →ₗ[R] P Q

The tensor product of a pair of linear maps between modules.

Equations
@[simp]
theorem tensor_product.map_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (m : M) (n : N) :
theorem tensor_product.map_range_eq_span_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
(tensor_product.map f g).range = submodule.span R {t : P Q | ∃ (m : M) (n : N), f m ⊗ₜ[R] g n = t}
@[simp]
def tensor_product.map_incl {R : Type u_1} [comm_semiring R] {P : Type u_6} {Q : Type u_7} [add_comm_monoid P] [add_comm_monoid Q] [module R P] [module R Q] (p : submodule R P) (q : submodule R Q) :

Given submodules p ⊆ P and q ⊆ Q, this is the natural map: p ⊗ q → P ⊗ Q.

Equations
theorem tensor_product.map_comp {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] {P' : Type u_9} {Q' : Type u_10} [add_comm_monoid P'] [module R P'] [add_comm_monoid Q'] [module R Q'] (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :
tensor_product.map (f₂.comp f₁) (g₂.comp g₁) = (tensor_product.map f₂ g₂).comp (tensor_product.map f₁ g₁)
theorem tensor_product.lift_comp_map {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] {Q' : Type u_10} [add_comm_monoid Q'] [module R Q'] (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
@[simp]
theorem tensor_product.map_id {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
@[simp]
theorem tensor_product.map_one {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
theorem tensor_product.map_mul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (f₁ f₂ : M →ₗ[R] M) (g₁ g₂ : N →ₗ[R] N) :
tensor_product.map (f₁ * f₂) (g₁ * g₂) = (tensor_product.map f₁ g₁) * tensor_product.map f₂ g₂
@[simp]
theorem tensor_product.map_pow {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ) :
def tensor_product.congr {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
M N ≃ₗ[R] P Q

If M and P are linearly equivalent and N and Q are linearly equivalent then M ⊗ N and P ⊗ Q are linearly equivalent.

Equations
@[simp]
theorem tensor_product.congr_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) :
@[simp]
theorem tensor_product.congr_symm_tmul {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) :
def tensor_product.left_comm (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
M (N P) ≃ₗ[R] N (M P)

A tensor product analogue of mul_left_comm.

Equations
@[simp]
theorem tensor_product.left_comm_tmul (R : Type u_1) [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (m : M) (n : N) (p : P) :
@[simp]
theorem tensor_product.left_comm_symm_tmul (R : Type u_1) [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (m : M) (n : N) (p : P) :
def tensor_product.tensor_tensor_tensor_comm (R : Type u_1) [comm_semiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] :
M N (P Q) ≃ₗ[R] M P (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 tensor_product.semiring instance (currently defined "by hand" using tensor_product.mul).

See also mul_mul_mul_comm.

Equations
@[simp]
theorem tensor_product.tensor_tensor_tensor_comm_tmul (R : Type u_1) [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (m : M) (n : N) (p : P) (q : Q) :
@[simp]
theorem tensor_product.tensor_tensor_tensor_comm_symm_tmul (R : Type u_1) [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (m : M) (n : N) (p : P) (q : Q) :
def linear_map.ltensor {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : N →ₗ[R] P) :
M N →ₗ[R] M P

ltensor M f : M ⊗ N →ₗ M ⊗ P is the natural linear map induced by f : N →ₗ P.

Equations
def linear_map.rtensor {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : N →ₗ[R] P) :
N M →ₗ[R] P M

rtensor f M : N₁ ⊗ M →ₗ N₂ ⊗ M is the natural linear map induced by f : N₁ →ₗ N₂.

Equations
@[simp]
theorem linear_map.ltensor_tmul {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : N →ₗ[R] P) (m : M) (n : N) :
@[simp]
theorem linear_map.rtensor_tmul {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : N →ₗ[R] P) (m : M) (n : N) :
def linear_map.ltensor_hom {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
(N →ₗ[R] P) →ₗ[R] M N →ₗ[R] M P

ltensor_hom M is the natural linear map that sends a linear map f : N →ₗ P to M ⊗ f.

Equations
def linear_map.rtensor_hom {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
(N →ₗ[R] P) →ₗ[R] N M →ₗ[R] P M

rtensor_hom M is the natural linear map that sends a linear map f : N →ₗ P to M ⊗ f.

Equations
@[simp]
theorem linear_map.coe_ltensor_hom {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
@[simp]
theorem linear_map.coe_rtensor_hom {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
@[simp]
theorem linear_map.ltensor_add {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f g : N →ₗ[R] P) :
@[simp]
theorem linear_map.rtensor_add {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f g : N →ₗ[R] P) :
@[simp]
theorem linear_map.ltensor_zero {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
@[simp]
theorem linear_map.rtensor_zero {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] :
@[simp]
theorem linear_map.ltensor_smul {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (r : R) (f : N →ₗ[R] P) :
@[simp]
theorem linear_map.rtensor_smul {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (r : R) (f : N →ₗ[R] P) :
theorem linear_map.ltensor_comp {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) :
theorem linear_map.rtensor_comp {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) :
theorem linear_map.ltensor_mul {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (f g : module.End R N) :
theorem linear_map.rtensor_mul {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (f g : module.End R N) :
@[simp]
theorem linear_map.ltensor_id {R : Type u_1} [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
@[simp]
theorem linear_map.rtensor_id {R : Type u_1} [comm_semiring R] (M : Type u_4) (N : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
@[simp]
theorem linear_map.ltensor_comp_rtensor {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
@[simp]
theorem linear_map.rtensor_comp_ltensor {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
@[simp]
theorem linear_map.map_comp_rtensor {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [module R M] [module R N] [module R P] [module R Q] [module R S] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) :
@[simp]
theorem linear_map.map_comp_ltensor {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [module R M] [module R N] [module R P] [module R Q] [module R S] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) :
@[simp]
theorem linear_map.rtensor_comp_map {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [module R M] [module R N] [module R P] [module R Q] [module R S] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
@[simp]
theorem linear_map.ltensor_comp_map {R : Type u_1} [comm_semiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [module R M] [module R N] [module R P] [module R Q] [module R S] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
@[simp]
theorem linear_map.rtensor_pow {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (f : M →ₗ[R] M) (n : ) :
@[simp]
theorem linear_map.ltensor_pow {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (f : N →ₗ[R] N) (n : ) :
def tensor_product.neg.aux (R : Type u_1) [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] :

Auxiliary function to defining negation multiplication on tensor product.

Equations
theorem tensor_product.neg.aux_of {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (m : M) (n : N) :
@[instance]
def tensor_product.has_neg {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] :
has_neg (M N)
Equations
theorem tensor_product.add_left_neg {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (x : M N) :
-x + x = 0
theorem tensor_product.neg_tmul {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (m : M) (n : N) :
(-m) ⊗ₜ[R] n = -m ⊗ₜ[R] n
theorem tensor_product.tmul_neg {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (m : M) (n : N) :
theorem tensor_product.tmul_sub {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (m : M) (n₁ n₂ : N) :
m ⊗ₜ[R] (n₁ - n₂) = m ⊗ₜ[R] n₁ - m ⊗ₜ[R] n₂
theorem tensor_product.sub_tmul {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (m₁ m₂ : M) (n : N) :
(m₁ - m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n
@[instance]
def tensor_product.compatible_smul.int {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] [module M] [module N] :

While the tensor product will automatically inherit a ℤ-module structure from add_comm_group.int_module, that structure won't be compatible with lemmas like tmul_smul unless we use a ℤ-module instance provided by tensor_product.left_module.

When R is a ring we get the required tensor_product.compatible_smul instance through is_scalar_tower, but when it is only a semiring we need to build it from scratch. The instance diamond in compatible_smul doesn't matter because it's in Prop.

Equations
@[instance]
def tensor_product.compatible_smul.unit {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] {S : Type u_4} [monoid S] [distrib_mul_action S M] [distrib_mul_action S N] [tensor_product.compatible_smul R S M N] :
Equations
@[simp]
theorem linear_map.ltensor_sub {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] (f g : N →ₗ[R] P) :
@[simp]
theorem linear_map.rtensor_sub {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] (f g : N →ₗ[R] P) :
@[simp]
theorem linear_map.ltensor_neg {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] (f : N →ₗ[R] P) :
@[simp]
theorem linear_map.rtensor_neg {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] (f : N →ₗ[R] P) :