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

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

source
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
Instances for tensor_product
source
@[protected, instance]
def tensor_product.add_zero_class {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] :
add_zero_class (tensor_product R M N)
Equations
source
@[protected, 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] :
add_comm_semigroup (tensor_product R M N)
Equations
source
@[protected, 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] :
inhabited (tensor_product R M N)
Equations
source
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) :
tensor_product R 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
source
@[protected]
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 : tensor_product R M N → Prop} (z : tensor_product R M N) (C0 : C 0) (C1 : ∀ {x : M} {y : N}, C (x ⊗ₜ[R] y)) (Cp : ∀ {x y : tensor_product R M N}, C x → C y → C (x + y)) :
C z
source
@[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
source
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
source
@[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
source
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₂
source
@[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 of this typeclass
Instances of other typeclasses for tensor_product.compatible_smul
  • tensor_product.compatible_smul.has_sizeof_inst
source
@[protected, 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] :
tensor_product.compatible_smul R R' M N

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

Equations
source
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 .

source
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') :
free_add_monoid (M × N) →+ tensor_product R M N

Auxiliary function to defining scalar multiplication on tensor product.

Equations
source
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) :
⇑(tensor_product.smul.aux r) (free_add_monoid.of (m, n)) = (r • m) ⊗ₜ[R] n
source
@[protected, 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' (tensor_product 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
source
@[protected, 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 (tensor_product R M N)
Equations
source
@[protected]
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
source
@[protected]
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 : tensor_product R M N) :
r • (x + y) = r • x + r • y
source
@[protected]
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 : tensor_product R M N) :
0 • x = 0
source
@[protected]
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 : tensor_product R M N) :
1 • x = x
source
@[protected]
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 : tensor_product R M N) :
(r + s) • x = r • x + s • x
source
@[protected, 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] :
add_comm_monoid (tensor_product R M N)
Equations
source
@[protected, 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] :
distrib_mul_action R' (tensor_product R M N)
Equations
source
@[protected, instance]
def tensor_product.distrib_mul_action {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] :
distrib_mul_action R (tensor_product R M N)
Equations
source
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
source
@[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
source
theorem tensor_product.smul_tmul_smul {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 s : R) (m : M) (n : N) :
(r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n
source
@[protected, 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'' (tensor_product R M N)
Equations
source
@[protected, 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 (tensor_product R M N)
Equations
source
@[protected, instance]
def tensor_product.is_central_scalar {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] [is_central_scalar R'' M] :
is_central_scalar R'' (tensor_product R M N)
source
@[protected, 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' (tensor_product R M N)

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

source
@[protected, 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' (tensor_product R M N)

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

source
@[protected, 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 (tensor_product R M N)

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

source
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] :
M →ₗ[R] N →ₗ[R] tensor_product R M N

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

Equations
source
@[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) :
⇑(⇑(tensor_product.mk R M N) m) n = m ⊗ₜ[R] n
source
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
source
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
source
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) :
s.sum (λ (a : α), m a) ⊗ₜ[R] n = s.sum (λ (a : α), m a ⊗ₜ[R] n)
source
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] s.sum (λ (a : α), n a) = s.sum (λ (a : α), m ⊗ₜ[R] n a)
source
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 : tensor_product R M N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t} = ⊤

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

source
@[simp]
theorem tensor_product.map₂_mk_top_top_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.map₂ (tensor_product.mk R M N) ⊤ ⊤ = ⊤
source
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) :
tensor_product R 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
source
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) :
⇑(tensor_product.lift_aux f) (m ⊗ₜ[R] n) = ⇑(⇑f m) n
source
@[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 : tensor_product R M N) :
⇑(tensor_product.lift_aux f) (r • x) = r • ⇑(tensor_product.lift_aux f) x
source
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) :
tensor_product R 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
source
@[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) :
⇑(tensor_product.lift f) (x ⊗ₜ[R] y) = ⇑(⇑f x) y
source
@[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) :
(tensor_product.lift f).to_fun (x ⊗ₜ[R] y) = ⇑(⇑f x) y
source
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 : tensor_product R M N →ₗ[R] P} (H : ∀ (x : M) (y : N), ⇑g (x ⊗ₜ[R] y) = ⇑h (x ⊗ₜ[R] y)) :
g = h
source
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 : tensor_product R M N →ₗ[R] P} (H : ∀ (x : M) (y : N), ⇑g (x ⊗ₜ[R] y) = ⇑(⇑f x) y) :
g = tensor_product.lift f
source
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] :
tensor_product.lift (tensor_product.mk R M N) = linear_map.id
source
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) :
tensor_product.lift (f.compr₂ g) = g.comp (tensor_product.lift f)
source
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 : tensor_product R M N →ₗ[R] P) :
tensor_product.lift ((tensor_product.mk R M N).compr₂ f) = f
source
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 : tensor_product R 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].

source
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] :
(M →ₗ[R] N →ₗ[R] P) →ₗ[R] tensor_product R M N →ₗ[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
source
@[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
source
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] :
(M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] tensor_product R M N →ₗ[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
source
@[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
source
@[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 : tensor_product R M N →ₗ[R] P) (m : M) (n : N) :
⇑(⇑(⇑((tensor_product.lift.equiv R M N P).symm) f) m) n = ⇑f (m ⊗ₜ[R] n)
source
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] :
(tensor_product R M N →ₗ[R] P) →ₗ[R] M →ₗ[R] 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
source
@[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 : tensor_product R M N →ₗ[R] P) (m : M) (n : N) :
⇑(⇑(⇑(tensor_product.lcurry R M N P) f) m) n = ⇑f (m ⊗ₜ[R] n)
source
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 : tensor_product R M N →ₗ[R] P) :
M →ₗ[R] 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
source
@[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 : tensor_product R M N →ₗ[R] P) (m : M) (n : N) :
⇑(⇑(tensor_product.curry f) m) n = ⇑f (m ⊗ₜ[R] n)
source
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] :
function.injective tensor_product.curry
source
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 : tensor_product R (tensor_product R 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
source
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 : tensor_product R (tensor_product R (tensor_product R 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
source
@[protected]
def tensor_product.lid (R : Type u_1) [comm_semiring R] (M : Type u_4) [add_comm_monoid M] [module R M] :
tensor_product R R M ≃ₗ[R] M

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

Equations
source
@[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) :
⇑(tensor_product.lid R M) (r ⊗ₜ[R] m) = r • m
source
@[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) :
⇑((tensor_product.lid R M).symm) m = 1 ⊗ₜ[R] m
source
@[protected]
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] :
tensor_product R M N ≃ₗ[R] tensor_product R N M

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

Equations
source
@[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) :
⇑(tensor_product.comm R M N) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
source
@[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) :
⇑((tensor_product.comm R M N).symm) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
source
@[protected]
def tensor_product.rid (R : Type u_1) [comm_semiring R] (M : Type u_4) [add_comm_monoid M] [module R M] :
tensor_product R M R ≃ₗ[R] M

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

Equations
source
@[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) :
⇑(tensor_product.rid R M) (m ⊗ₜ[R] r) = r • m
source
@[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) :
⇑((tensor_product.rid R M).symm) m = m ⊗ₜ[R] 1
source
@[protected]
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] :
tensor_product R (tensor_product R M N) P ≃ₗ[R] tensor_product R M (tensor_product R N P)

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

Equations
source
@[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) :
⇑(tensor_product.assoc R M N P) (m ⊗ₜ[R] n ⊗ₜ[R] p) = m ⊗ₜ[R] (n ⊗ₜ[R] p)
source
@[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) :
⇑((tensor_product.assoc R M N P).symm) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = m ⊗ₜ[R] n ⊗ₜ[R] p
source
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) :
tensor_product R M N →ₗ[R] tensor_product R P Q

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

Equations
source
@[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) :
⇑(tensor_product.map f g) (m ⊗ₜ[R] n) = ⇑f m ⊗ₜ[R] ⇑g n
source
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 : tensor_product R P Q | ∃ (m : M) (n : N), ⇑f m ⊗ₜ[R] ⇑g n = t}
source
@[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) :
tensor_product R ↥p ↥q →ₗ[R] tensor_product R P Q

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

Equations
source
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₁)
source
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) :
(tensor_product.lift i).comp (tensor_product.map f g) = tensor_product.lift ((i.comp f).compl₂ g)
source
@[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] :
tensor_product.map linear_map.id linear_map.id = linear_map.id
source
@[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] :
tensor_product.map 1 1 = 1
source
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₂
source
@[protected, 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 : ℕ) :
tensor_product.map f g ^ n = tensor_product.map (f ^ n) (g ^ n)
source
theorem tensor_product.map_add_left {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₁ f₂ : M →ₗ[R] P) (g : N →ₗ[R] Q) :
tensor_product.map (f₁ + f₂) g = tensor_product.map f₁ g + tensor_product.map f₂ g
source
theorem tensor_product.map_add_right {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₁ g₂ : N →ₗ[R] Q) :
tensor_product.map f (g₁ + g₂) = tensor_product.map f g₁ + tensor_product.map f g₂
source
theorem tensor_product.map_smul_left {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] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
tensor_product.map (r • f) g = r • tensor_product.map f g
source
theorem tensor_product.map_smul_right {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] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
tensor_product.map f (r • g) = r • tensor_product.map f g
source
def tensor_product.map_bilinear (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 →ₗ[R] P) →ₗ[R] (N →ₗ[R] Q) →ₗ[R] tensor_product R M N →ₗ[R] tensor_product R P Q

The tensor product of a pair of linear maps between modules, bilinear in both maps.

Equations
source
def tensor_product.ltensor_hom_to_hom_ltensor (R : Type u_1) [comm_semiring R] (M : Type u_4) (P : Type u_6) (Q : Type u_7) [add_comm_monoid M] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R P] [module R Q] :
tensor_product R P (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] tensor_product R P Q

The canonical linear map from P ⊗[R] (M →ₗ[R] Q) to (M →ₗ[R] P ⊗[R] Q)

Equations
source
def tensor_product.rtensor_hom_to_hom_rtensor (R : Type u_1) [comm_semiring R] (M : Type u_4) (P : Type u_6) (Q : Type u_7) [add_comm_monoid M] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R P] [module R Q] :
tensor_product R (M →ₗ[R] P) Q →ₗ[R] M →ₗ[R] tensor_product R P Q

The canonical linear map from (M →ₗ[R] P) ⊗[R] Q to (M →ₗ[R] P ⊗[R] Q)

Equations
source
def tensor_product.hom_tensor_hom_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] :
tensor_product R (M →ₗ[R] P) (N →ₗ[R] Q) →ₗ[R] tensor_product R M N →ₗ[R] tensor_product R P Q

The linear map from (M →ₗ P) ⊗ (N →ₗ Q) to (M ⊗ N →ₗ P ⊗ Q) sending f ⊗ₜ g to the tensor_product.map f g, the tensor product of the two maps.

Equations
source
@[simp]
theorem tensor_product.map_bilinear_apply {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_bilinear R M N P Q) f) g = tensor_product.map f g
source
@[simp]
theorem tensor_product.ltensor_hom_to_hom_ltensor_apply {R : Type u_1} [comm_semiring R] {M : Type u_4} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R P] [module R Q] (p : P) (f : M →ₗ[R] Q) (m : M) :
⇑(⇑(tensor_product.ltensor_hom_to_hom_ltensor R M P Q) (p ⊗ₜ[R] f)) m = p ⊗ₜ[R] ⇑f m
source
@[simp]
theorem tensor_product.rtensor_hom_to_hom_rtensor_apply {R : Type u_1} [comm_semiring R] {M : Type u_4} {P : Type u_6} {Q : Type u_7} [add_comm_monoid M] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R P] [module R Q] (f : M →ₗ[R] P) (q : Q) (m : M) :
⇑(⇑(tensor_product.rtensor_hom_to_hom_rtensor R M P Q) (f ⊗ₜ[R] q)) m = ⇑f m ⊗ₜ[R] q
source
@[simp]
theorem tensor_product.hom_tensor_hom_map_apply {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.hom_tensor_hom_map R M N P Q) (f ⊗ₜ[R] g) = tensor_product.map f g
source
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) :
tensor_product R M N ≃ₗ[R] tensor_product 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
source
@[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) :
⇑(tensor_product.congr f g) (m ⊗ₜ[R] n) = ⇑f m ⊗ₜ[R] ⇑g n
source
@[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) :
⇑((tensor_product.congr f g).symm) (p ⊗ₜ[R] q) = ⇑(f.symm) p ⊗ₜ[R] ⇑(g.symm) q
source
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] :
tensor_product R M (tensor_product R N P) ≃ₗ[R] tensor_product R N (tensor_product R M P)

A tensor product analogue of mul_left_comm.

Equations
source
@[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) :
⇑(tensor_product.left_comm R M N P) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = n ⊗ₜ[R] (m ⊗ₜ[R] p)
source
@[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) :
⇑((tensor_product.left_comm R M N P).symm) (n ⊗ₜ[R] (m ⊗ₜ[R] p)) = m ⊗ₜ[R] (n ⊗ₜ[R] p)
source
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] :
tensor_product R (tensor_product R M N) (tensor_product R P Q) ≃ₗ[R] tensor_product R (tensor_product R M P) (tensor_product 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 tensor_product.semiring instance (currently defined "by hand" using tensor_product.mul).

See also mul_mul_mul_comm.

Equations
source
@[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) :
⇑(tensor_product.tensor_tensor_tensor_comm R M N P Q) (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)) = m ⊗ₜ[R] p ⊗ₜ[R] (n ⊗ₜ[R] q)
source
@[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) :
⇑((tensor_product.tensor_tensor_tensor_comm R M N P Q).symm) (m ⊗ₜ[R] p ⊗ₜ[R] (n ⊗ₜ[R] q)) = m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)
source
def tensor_product.tensor_tensor_tensor_assoc (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] :
tensor_product R (tensor_product R M N) (tensor_product R P Q) ≃ₗ[R] tensor_product R (tensor_product R M (tensor_product R N P)) Q

This special case is useful for describing the interplay between dual_tensor_hom_equiv 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 contract_right on N ⊗ N.dual after the suitable rebracketting.

Equations
source
@[simp]
theorem tensor_product.tensor_tensor_tensor_assoc_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) :
⇑(tensor_product.tensor_tensor_tensor_assoc R M N P Q) (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)) = m ⊗ₜ[R] (n ⊗ₜ[R] p) ⊗ₜ[R] q
source
@[simp]
theorem tensor_product.tensor_tensor_tensor_assoc_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) :
⇑((tensor_product.tensor_tensor_tensor_assoc R M N P Q).symm) (m ⊗ₜ[R] (n ⊗ₜ[R] p) ⊗ₜ[R] q) = m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)
source
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) :
tensor_product R M N →ₗ[R] tensor_product R M P

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

Equations
source
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) :
tensor_product R N M →ₗ[R] tensor_product R P M

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

Equations
source
@[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) :
⇑(linear_map.ltensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] ⇑f n
source
@[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) :
⇑(linear_map.rtensor M f) (n ⊗ₜ[R] m) = ⇑f n ⊗ₜ[R] m
source
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] tensor_product R M N →ₗ[R] tensor_product R M P

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

Equations
source
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] tensor_product R N M →ₗ[R] tensor_product R P M

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

Equations
source
@[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] :
⇑(linear_map.ltensor_hom M) = linear_map.ltensor M
source
@[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] :
⇑(linear_map.rtensor_hom M) = linear_map.rtensor M
source
@[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) :
linear_map.ltensor M (f + g) = linear_map.ltensor M f + linear_map.ltensor M g
source
@[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) :
linear_map.rtensor M (f + g) = linear_map.rtensor M f + linear_map.rtensor M g
source
@[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] :
linear_map.ltensor M 0 = 0
source
@[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] :
linear_map.rtensor M 0 = 0
source
@[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) :
linear_map.ltensor M (r • f) = r • linear_map.ltensor M f
source
@[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) :
linear_map.rtensor M (r • f) = r • linear_map.rtensor M f
source
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) :
linear_map.ltensor M (g.comp f) = (linear_map.ltensor M g).comp (linear_map.ltensor M f)
source
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) :
linear_map.rtensor M (g.comp f) = (linear_map.rtensor M g).comp (linear_map.rtensor M f)
source
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) :
linear_map.ltensor M (f * g) = linear_map.ltensor M f * linear_map.ltensor M g
source
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) :
linear_map.rtensor M (f * g) = linear_map.rtensor M f * linear_map.rtensor M g
source
@[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] :
linear_map.ltensor M linear_map.id = linear_map.id
source
@[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] :
linear_map.rtensor M linear_map.id = linear_map.id
source
@[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) :
(linear_map.ltensor P g).comp (linear_map.rtensor N f) = tensor_product.map f g
source
@[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) :
(linear_map.rtensor Q f).comp (linear_map.ltensor M g) = tensor_product.map f g
source
@[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) :
(tensor_product.map f g).comp (linear_map.rtensor N f') = tensor_product.map (f.comp f') g
source
@[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) :
(tensor_product.map f g).comp (linear_map.ltensor M g') = tensor_product.map f (g.comp g')
source
@[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) :
(linear_map.rtensor Q f').comp (tensor_product.map f g) = tensor_product.map (f'.comp f) g
source
@[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) :
(linear_map.ltensor P g').comp (tensor_product.map f g) = tensor_product.map f (g'.comp g)
source
@[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 : ℕ) :
linear_map.rtensor N f ^ n = linear_map.rtensor N (f ^ n)
source
@[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 : ℕ) :
linear_map.ltensor M f ^ n = linear_map.ltensor M (f ^ n)
source
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] :
free_add_monoid (M × N) →+ tensor_product R M N

Auxiliary function to defining negation multiplication on tensor product.

Equations
source
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) :
⇑(tensor_product.neg.aux R) (free_add_monoid.of (m, n)) = (-m) ⊗ₜ[R] n
source
@[protected, 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 (tensor_product R M N)
Equations
source
@[protected]
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 : tensor_product R M N) :
-x + x = 0
source
@[protected, instance]
def tensor_product.add_comm_group {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] :
add_comm_group (tensor_product R M N)
Equations
source
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
source
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) :
m ⊗ₜ[R] -n = -m ⊗ₜ[R] n
source
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₂
source
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
source
@[protected, 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] :
tensor_product.compatible_smul R ℤ M 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
source
@[protected, 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] :
tensor_product.compatible_smul R Sˣ M N
Equations
source
@[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) :
linear_map.ltensor M (f - g) = linear_map.ltensor M f - linear_map.ltensor M g
source
@[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) :
linear_map.rtensor M (f - g) = linear_map.rtensor M f - linear_map.rtensor M g
source
@[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) :
linear_map.ltensor M (-f) = -linear_map.ltensor M f
source
@[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) :
linear_map.rtensor M (-f) = -linear_map.rtensor M f