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.
@[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
- f.flip = linear_map.mk₂ R (λ (n : N) (m : M), ⇑(⇑f m) n) _ _ _ _
@[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) :
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
- linear_map.lflip R M N P = {to_fun := linear_map.flip _inst_9, map_add' := _, map_smul' := _}
@[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) :
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) :
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) :
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) :
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) :
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
- linear_map.lcomp R P f = (linear_map.id.flip.comp f).flip
@[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) :
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
- linear_map.llcomp R M N P = {to_fun := linear_map.lcomp R P _inst_9, map_add' := _, map_smul' := _}.flip
@[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) :
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
- f.compl₂ g = (linear_map.lcomp R P g).comp f
@[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) :
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
- f.compr₂ g = (⇑(linear_map.llcomp R N P Q) g).comp f
@[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) :
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
- linear_map.lsmul R M = linear_map.mk₂ R has_scalar.smul _ _ _ _
@[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]
(a a_1 : free_add_monoid (M × N)) :
Prop
- of_zero_left : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) (N : Type u_3) [_inst_2 : add_comm_monoid M] [_inst_3 : add_comm_monoid N] [_inst_7 : semimodule R M] [_inst_8 : semimodule R N] (n : N), tensor_product.eqv R M N (free_add_monoid.of (0, n)) 0
- of_zero_right : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) (N : Type u_3) [_inst_2 : add_comm_monoid M] [_inst_3 : add_comm_monoid N] [_inst_7 : semimodule R M] [_inst_8 : semimodule R N] (m : M), tensor_product.eqv R M N (free_add_monoid.of (m, 0)) 0
- of_add_left : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) (N : Type u_3) [_inst_2 : add_comm_monoid M] [_inst_3 : add_comm_monoid N] [_inst_7 : semimodule R M] [_inst_8 : semimodule R N] (m₁ m₂ : M) (n : N), tensor_product.eqv R M N (free_add_monoid.of (m₁, n) + free_add_monoid.of (m₂, n)) (free_add_monoid.of (m₁ + m₂, n))
- of_add_right : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) (N : Type u_3) [_inst_2 : add_comm_monoid M] [_inst_3 : add_comm_monoid N] [_inst_7 : semimodule R M] [_inst_8 : semimodule R N] (m : M) (n₁ n₂ : N), tensor_product.eqv R M N (free_add_monoid.of (m, n₁) + free_add_monoid.of (m, n₂)) (free_add_monoid.of (m, n₁ + n₂))
- of_smul : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) (N : Type u_3) [_inst_2 : add_comm_monoid M] [_inst_3 : add_comm_monoid N] [_inst_7 : semimodule R M] [_inst_8 : semimodule R N] (r : R) (m : M) (n : N), tensor_product.eqv R M N (free_add_monoid.of (r • m, n)) (free_add_monoid.of (m, r • n))
- add_comm : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) (N : Type u_3) [_inst_2 : add_comm_monoid M] [_inst_3 : add_comm_monoid N] [_inst_7 : semimodule R M] [_inst_8 : semimodule R N] (x y : free_add_monoid (M × N)), tensor_product.eqv R M N (x + y) (y + x)
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
- M ⊗ N = (add_con_gen (tensor_product.eqv R M N)).quotient
@[instance]
def
tensor_product.add_comm_monoid
{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] :
add_comm_monoid (M ⊗ N)
Equations
- tensor_product.add_comm_monoid M N = {add := add_monoid.add (add_con_gen (tensor_product.eqv R M N)).add_monoid, add_assoc := _, zero := add_monoid.zero (add_con_gen (tensor_product.eqv R M N)).add_monoid, zero_add := _, add_zero := _, add_comm := _}
@[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
- tensor_product.inhabited M N = {default := 0}
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 : 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
- (m ⊗ₜ[R] n) = ⇑((add_con_gen (tensor_product.eqv R M N)).mk') (free_add_monoid.of (m, n))
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)
(C0 : C 0)
(C1 : ∀ {x : M} {y : N}, C (x ⊗ₜ[R] y))
(Cp : ∀ {x y : M ⊗ N}, C x → C y → C (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) :
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) :
@[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) :
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) :
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) :
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 : R) :
free_add_monoid (M × N) →+ M ⊗ N
Auxiliary function to defining scalar multiplication on tensor product.
Equations
- tensor_product.smul.aux r = ⇑free_add_monoid.lift (λ (p : M × N), (r • p.fst) ⊗ₜ[R] p.snd)
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) :
⇑(tensor_product.smul.aux r) (free_add_monoid.of (m, n)) = (r • m) ⊗ₜ[R] 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
- tensor_product.has_scalar = {smul := λ (r : R), ⇑((add_con_gen (tensor_product.eqv R M N)).lift (tensor_product.smul.aux r) _)}
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) :
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) :
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) :
@[instance]
def
tensor_product.semimodule
{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] :
semimodule R (M ⊗ N)
Equations
- tensor_product.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul tensor_product.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[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) :
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
- tensor_product.mk R M N = linear_map.mk₂ R (λ (_x : M) (_y : N), _x ⊗ₜ[R] _y) tensor_product.add_tmul _ tensor_product.tmul_add tensor_product.tmul_smul
@[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] :
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] :
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) :
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) :
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]
(f : M →ₗ[R] N →ₗ[R] 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
- tensor_product.lift_aux f = (add_con_gen (tensor_product.eqv R M N)).lift (⇑free_add_monoid.lift (λ (p : M × N), ⇑(⇑f p.fst) p.snd)) _
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) :
⇑(tensor_product.lift_aux f) (r • x) = r • ⇑(tensor_product.lift_aux f) x
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]
(f : M →ₗ[R] 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
- tensor_product.lift f = {to_fun := (tensor_product.lift_aux f).to_fun, map_add' := _, map_smul' := _}
@[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}
(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_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}
(H : ∀ (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) :
tensor_product.lift (f.compr₂ g) = g.comp (tensor_product.lift f)
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) :
tensor_product.lift ((tensor_product.mk R M N).compr₂ f) = f
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}
(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_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
- tensor_product.uncurry R M N P = (tensor_product.lift ((linear_map.lflip R (M →ₗ[R] N →ₗ[R] P) N P).comp linear_map.id.flip)).flip
@[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) :
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.
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
- tensor_product.lcurry R M N P = ↑((tensor_product.lift.equiv R M N P).symm)
@[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) :
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]
(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
- tensor_product.curry f = ⇑(tensor_product.lcurry R M N P) f
@[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}
(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_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}
(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_2)
[add_comm_monoid M]
[semimodule R M] :
The base ring is a left identity for the tensor product of modules, up to linear equivalence.
Equations
- tensor_product.lid R M = linear_equiv.of_linear (tensor_product.lift (linear_map.lsmul R M)) (⇑(tensor_product.mk R R M) 1) _ _
@[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] :
The tensor product of modules is commutative, up to linear equivalence.
Equations
- tensor_product.comm R M N = linear_equiv.of_linear (tensor_product.lift (tensor_product.mk R N M).flip) (tensor_product.lift (tensor_product.mk R M N).flip) _ _
@[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] :
The base ring is a right identity for the tensor product of modules, up to linear equivalence.
Equations
- tensor_product.rid R M = (tensor_product.comm R M R).trans (tensor_product.lid R M)
@[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] :
The associator for tensor product of R-modules, as a linear equivalence.
Equations
- tensor_product.assoc R M N P = linear_equiv.of_linear (tensor_product.lift (tensor_product.lift ((tensor_product.lcurry R N P (M ⊗ (N ⊗ P))).comp (tensor_product.mk R M (N ⊗ P))))) (tensor_product.lift ((tensor_product.uncurry R N P (M ⊗ N ⊗ P)).comp (tensor_product.curry (tensor_product.mk R (M ⊗ N) P)))) _ _
@[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]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
The tensor product of a pair of linear maps between modules.
Equations
- tensor_product.map f g = tensor_product.lift (((tensor_product.mk R P Q).compl₂ g).comp f)
@[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]
(f : M ≃ₗ[R] P)
(g : N ≃ₗ[R] 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
- tensor_product.congr f g = linear_equiv.of_linear (tensor_product.map ↑f ↑g) (tensor_product.map ↑(f.symm) ↑(g.symm)) _ _
@[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] :
add_comm_group (M ⊗ N)
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) :
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) :