mathlib documentation

linear_algebra.tensor_product

Tensor product of semimodules over commutative semirings.

This file constructs the tensor product of semimodules over commutative semirings. Given a semiring R and semimodules over it M and N, the standard construction of the tensor product is tensor_product R M N. It is also a semimodule 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

def linear_map.mk₂ (R : Type u_1) [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M → N → P) (H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : ∀ (c : R) (m : M) (n : N), f (c m) n = c f m n) (H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : ∀ (c : R) (m : M) (n : N), f m (c n) = c f m n) :

Create a bilinear map from a function that is linear in each component.

Equations
@[simp]
theorem linear_map.mk₂_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M → N → P) {H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n} {H2 : ∀ (c : R) (m : M) (n : N), f (c m) n = c f m n} {H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂} {H4 : ∀ (c : R) (m : M) (n : N), f m (c n) = c f m n} (m : M) (n : N) :
((linear_map.mk₂ R f H1 H2 H3 H4) m) n = f m n

theorem linear_map.ext₂ {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] {f g : M →ₗ[R] N →ₗ[R] P} (H : ∀ (m : M) (n : N), (f m) n = (g m) n) :
f = g

def linear_map.flip {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) :

Given a linear map from M to linear maps from N to P, i.e., a bilinear map from M × N to P, change the order of variables and get a linear map from N to linear maps from M to P.

Equations
@[simp]
theorem linear_map.flip_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
((f.flip) n) m = (f m) n

theorem linear_map.flip_inj {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] {f g : M →ₗ[R] N →ₗ[R] P} (H : f.flip = g.flip) :
f = g

def linear_map.lflip (R : Type u_1) [comm_semiring R] (M : Type u_2) (N : Type u_3) (P : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] :

Given a linear map from M to linear maps from N to P, i.e., a bilinear map M → N → P, change the order of variables and get a linear map from N to linear maps from M to P.

Equations
@[simp]
theorem linear_map.lflip_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
(((linear_map.lflip R M N P) f) n) m = (f m) n

theorem linear_map.map_zero₂ {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (y : N) :
(f 0) y = 0

theorem linear_map.map_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_monoid N] [add_comm_group P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (x : M) (y : N) :
(f (-x)) y = -(f x) y

theorem linear_map.map_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_monoid N] [add_comm_group P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (x y : M) (z : N) :
(f (x - y)) z = (f x) z - (f y) z

theorem linear_map.map_add₂ {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (x₁ x₂ : M) (y : N) :
(f (x₁ + x₂)) y = (f x₁) y + (f x₂) y

theorem linear_map.map_smul₂ {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N →ₗ[R] P) (r : R) (x : M) (y : N) :
(f (r x)) y = r (f x) y

def linear_map.lcomp (R : Type u_1) [comm_semiring R] {M : Type u_2} {N : Type u_3} (P : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N) :

Composing a linear map M → N and a linear map N → P to form a linear map M → P.

Equations
@[simp]
theorem linear_map.lcomp_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (x : M) :
((linear_map.lcomp R P f) g) x = g (f x)

def linear_map.llcomp (R : Type u_1) [comm_semiring R] (M : Type u_2) (N : Type u_3) (P : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] :

Composing a linear map M → N and a linear map N → P to form a linear map M → P.

Equations
@[simp]
theorem linear_map.llcomp_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : N →ₗ[R] P) (g : M →ₗ[R] N) (x : M) :
(((linear_map.llcomp R M N P) f) g) x = f (g x)

def linear_map.compl₂ {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] (f : M →ₗ[R] N →ₗ[R] P) (g : Q →ₗ[R] N) :

Composing a linear map Q → N and a bilinear map M → N → P to form a bilinear map M → Q → P.

Equations
@[simp]
theorem linear_map.compl₂_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] (f : M →ₗ[R] N →ₗ[R] P) (g : Q →ₗ[R] N) (m : M) (q : Q) :
((f.compl₂ g) m) q = (f m) (g q)

def linear_map.compr₂ {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] (f : M →ₗ[R] N →ₗ[R] P) (g : P →ₗ[R] Q) :

Composing a linear map P → Q and a bilinear map M × N → P to form a bilinear map M → N → Q.

Equations
@[simp]
theorem linear_map.compr₂_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] (f : M →ₗ[R] N →ₗ[R] P) (g : P →ₗ[R] Q) (m : M) (n : N) :
((f.compr₂ g) m) n = g ((f m) n)

def linear_map.lsmul (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :

Scalar multiplication as a bilinear map R → M → M.

Equations
@[simp]
theorem linear_map.lsmul_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] (r : R) (m : M) :
((linear_map.lsmul R M) r) m = r m

inductive tensor_product.eqv (R : Type u_1) [comm_semiring R] (M : Type u_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
Type (max u_3 u_4)

The tensor product of two semimodules 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.inhabited {R : Type u_1} [comm_semiring R] (M : Type u_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :

Equations
def tensor_product.tmul (R : Type u_1) [comm_semiring R] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3) {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (n : N) :
0 ⊗ₜ[R] n = 0

theorem tensor_product.add_tmul {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3} (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (m : M) :
m ⊗ₜ[R] 0 = 0

theorem tensor_product.tmul_add {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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) [comm_semiring R'] (M : Type u_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule 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 semimodule 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} [comm_semiring R'] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule R' N] [has_scalar R' R] [is_scalar_tower R' R M] [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} [comm_semiring R'] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule 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_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] {R' : Type u_2} [has_scalar R' M] (r : R') (m : M) (n : N) :

@[nolint, instance]
def tensor_product.has_scalar' {R : Type u_1} [comm_semiring R] {R' : Type u_2} [comm_semiring R'] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule R' N] [smul_comm_class R R' M] [smul_comm_class R R' N] :
has_scalar R' (M N)

Equations
@[instance]
def tensor_product.has_scalar {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
has_scalar R (M N)

Equations
theorem tensor_product.smul_zero {R : Type u_1} [comm_semiring R] {R' : Type u_2} [comm_semiring R'] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule R' N] [smul_comm_class R R' M] [smul_comm_class R R' N] (r : R') :
r 0 = 0

theorem tensor_product.smul_add {R : Type u_1} [comm_semiring R] {R' : Type u_2} [comm_semiring R'] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule R' N] [smul_comm_class R R' M] [smul_comm_class R R' N] (r : R') (x y : M N) :
r (x + y) = r x + r y

@[instance]
def tensor_product.semimodule' {R : Type u_1} [comm_semiring R] {R' : Type u_2} [comm_semiring R'] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule R' N] [smul_comm_class R R' M] [smul_comm_class R R' N] :
semimodule R' (M N)

Equations
@[instance]
def tensor_product.semimodule {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
semimodule R (M N)

Equations
@[nolint]
theorem tensor_product.smul_tmul' {R : Type u_1} [comm_semiring R] {R' : Type u_2} [comm_semiring R'] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule R' N] [smul_comm_class R R' M] [smul_comm_class R R' N] [tensor_product.compatible_smul R R' M N] (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} [comm_semiring R'] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [semimodule R' M] [semimodule R' N] [smul_comm_class R R' M] [smul_comm_class R R' N] [tensor_product.compatible_smul R R' M N] (r : R') (x : M) (y : N) :
x ⊗ₜ[R] (r y) = r x ⊗ₜ[R] y

def tensor_product.mk (R : Type u_1) [comm_semiring R] (M : Type u_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (m : M) (n : N) :

theorem tensor_product.ite_tmul {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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

def tensor_product.lift_aux {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :

@[ext]
theorem tensor_product.ext {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :

theorem tensor_product.lift_compr₂ {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M N →ₗ[R] P) :

theorem tensor_product.mk_compr₂_inj {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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

def tensor_product.uncurry (R : Type u_1) [comm_semiring R] (M : Type u_3) (N : Type u_4) (P : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3) (N : Type u_4) (P : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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
def tensor_product.lcurry (R : Type u_1) [comm_semiring R] (M : Type u_3) (N : Type u_4) (P : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f : M N →ₗ[R] P) (m : M) (n : N) :

theorem tensor_product.ext_threefold {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule 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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} {S : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] [semimodule 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_3) [add_comm_monoid M] [semimodule 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_3} [add_comm_monoid M] [semimodule R M] (m : M) (r : R) :

@[simp]
theorem tensor_product.lid_symm_apply {R : Type u_1} [comm_semiring R] {M : Type u_3} [add_comm_monoid M] [semimodule R M] (m : M) :

def tensor_product.comm (R : Type u_1) [comm_semiring R] (M : Type u_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule 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_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (m : M) (n : N) :

@[simp]
theorem tensor_product.comm_symm_tmul (R : Type u_1) [comm_semiring R] (M : Type u_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (m : M) (n : N) :

def tensor_product.rid (R : Type u_1) [comm_semiring R] (M : Type u_3) [add_comm_monoid M] [semimodule 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_3} [add_comm_monoid M] [semimodule R M] (m : M) (r : R) :

@[simp]
theorem tensor_product.rid_symm_apply {R : Type u_1} [comm_semiring R] {M : Type u_3} [add_comm_monoid M] [semimodule R M] (m : M) :

def tensor_product.assoc (R : Type u_1) [comm_semiring R] (M : Type u_3) (N : Type u_4) (P : Type u_5) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3} {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (m : M) (n : N) (p : P) :

def tensor_product.map {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule 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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (m : M) (n : N) :

theorem tensor_product.map_comp {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] {P' : Type u_8} {Q' : Type u_9} [add_comm_monoid P'] [semimodule R P'] [add_comm_monoid Q'] [semimodule 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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] {Q' : Type u_9} [add_comm_monoid Q'] [semimodule R Q'] (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

def tensor_product.congr {R : Type u_1} [comm_semiring R] {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule 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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule 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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) :

def linear_map.ltensor {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule 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_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] :

@[simp]
theorem linear_map.coe_rtensor_hom {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] :

@[simp]
theorem linear_map.ltensor_add {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f g : N →ₗ[R] P) :

@[simp]
theorem linear_map.rtensor_add {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (f g : N →ₗ[R] P) :

@[simp]
theorem linear_map.ltensor_zero {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] :

@[simp]
theorem linear_map.rtensor_zero {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] :

@[simp]
theorem linear_map.ltensor_smul {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (r : R) (f : N →ₗ[R] P) :

@[simp]
theorem linear_map.rtensor_smul {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [semimodule R M] [semimodule R N] [semimodule R P] (r : R) (f : N →ₗ[R] P) :

theorem linear_map.ltensor_comp {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule 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_3) {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) :

@[simp]
theorem linear_map.ltensor_id {R : Type u_1} [comm_semiring R] (M : Type u_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :

@[simp]
theorem linear_map.rtensor_id {R : Type u_1} [comm_semiring R] (M : Type u_3) (N : Type u_4) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :

@[simp]
theorem linear_map.ltensor_comp_rtensor {R : Type u_1} [comm_semiring R] (M : Type u_3) {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule 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_3) {N : Type u_4} {P : Type u_5} {Q : Type u_6} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule 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_3) {N : Type u_4} {P : Type u_5} {Q : Type u_6} {S : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] [semimodule 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_3) {N : Type u_4} {P : Type u_5} {Q : Type u_6} {S : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] [semimodule 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_3) {N : Type u_4} {P : Type u_5} {Q : Type u_6} {S : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] [semimodule 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_3) {N : Type u_4} {P : Type u_5} {Q : Type u_6} {S : Type u_7} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [add_comm_monoid S] [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] [semimodule R S] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

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] [semimodule R M] [semimodule 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] [semimodule R M] [semimodule 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] [semimodule R M] [semimodule R N] :
has_neg (M N)

Equations
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] [semimodule R M] [semimodule 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] [semimodule R M] [semimodule 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] [semimodule R M] [semimodule 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] [semimodule R M] [semimodule 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] [semimodule R M] [semimodule R N] [semimodule M] [semimodule 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.semimodule'.

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
@[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] [semimodule R M] [semimodule R N] [semimodule 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] [semimodule R M] [semimodule R N] [semimodule 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] [semimodule R M] [semimodule R N] [semimodule 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] [semimodule R M] [semimodule R N] [semimodule R P] (f : N →ₗ[R] P) :