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) :
(∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n)(∀ (c : R) (m : M) (n : N), f (c m) n = c f m n)(∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂)(∀ (c : R) (m : M) (n : N), f m (c n) = c f m n)(M →ₗ[R] N →ₗ[R] P)

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} :
(∀ (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] :
(M →ₗ[R] N →ₗ[R] P)(N →ₗ[R] M →ₗ[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} :
f.flip = g.flipf = 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_ring 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 : M →ₗ[R] N →ₗ[R] P) (x : M) (y : N) :
(f (-x)) y = -(f x) y

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

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] :
(M →ₗ[R] N →ₗ[R] P)(P →ₗ[R] Q)(M →ₗ[R] N →ₗ[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_2) (N : Type u_3) [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_2) (N : Type u_3) [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
Type (max u_2 u_3)

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_2) (N : Type u_3) [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_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
M → 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_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] {C : M N → Prop} (z : M N) :
C 0(∀ {x : M} {y : N}, C (x ⊗ₜ[R] y))(∀ {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_2) {N : Type u_3} [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_2} {N : Type u_3} [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_2} (N : Type u_3) [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_2} {N : Type u_3} [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₂

theorem tensor_product.smul_tmul {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (r : R) (m : M) (n : N) :
((r m) ⊗ₜ[R] n) = m ⊗ₜ[R] r n

def tensor_product.smul.aux {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
R → free_add_monoid (M × N) →+ M N

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_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (r : R) (m : M) (n : N) :

@[instance]
def tensor_product.has_scalar {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [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] {M : Type u_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (r : R) :
r 0 = 0

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

theorem tensor_product.smul_tmul' {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R 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] {M : Type u_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R 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_2) (N : Type u_3) [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_2} {N : Type u_3} [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_2} {N : Type u_3} [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_2} {N : Type u_3} [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_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] {α : Type u_4} (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_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] (m : M) {α : Type u_4} (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_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] :
(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_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) :

@[simp]
theorem tensor_product.lift_aux.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 N) :

def tensor_product.lift {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] :
(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_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 : M) (y : N) :

@[simp]
theorem tensor_product.lift.tmul' {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 : M) (y : N) :

@[ext]
theorem tensor_product.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] {g h : M N →ₗ[R] P} :
(∀ (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_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} {g : M N →ₗ[R] P} :
(∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f x) y)g = tensor_product.lift f

theorem tensor_product.lift_mk {R : Type u_1} [comm_semiring R] {M : Type u_2} {N : Type u_3} [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_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) :

theorem tensor_product.lift_mk_compr₂ {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 →ₗ[R] P) :

theorem tensor_product.mk_compr₂_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] {g h : M N →ₗ[R] P} :

def tensor_product.uncurry (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] :

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_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) :
((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_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] :

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_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 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_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 →ₗ[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_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] :
(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
@[simp]
theorem tensor_product.curry_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 →ₗ[R] P) (m : M) (n : N) :

theorem tensor_product.ext_threefold {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] {g h : M N P →ₗ[R] Q} :
(∀ (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_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} {S : Type u_6} [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} :
(∀ (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_2) [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_2} [add_comm_monoid M] [semimodule R M] (m : M) (r : R) :

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

def tensor_product.assoc (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] :
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_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] (m : M) (n : N) (p : P) :

def tensor_product.map {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] :
(M →ₗ[R] P)(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_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] P) (g : N →ₗ[R] Q) (m : M) (n : N) :

def tensor_product.congr {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] :
(M ≃ₗ[R] P)(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_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] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) :

@[instance]
def tensor_product.add_comm_group {R : Type u_1} [comm_ring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] :

Equations
theorem tensor_product.neg_tmul {R : Type u_1} [comm_ring R] {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [module R M] [module R N] (m : M) (n : N) :
((-m) ⊗ₜ[R] n) = -m ⊗ₜ[R] n

theorem tensor_product.tmul_neg {R : Type u_1} [comm_ring 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