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)
[semiring R]
(S : Type u_2)
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S 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 : S) (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.
See mk₂ for the special case where both arguments come from modules over the same ring.
@[simp]
theorem
linear_map.mk₂'_apply
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S 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 : S) (m : M) (n : N), f m (c • n) = c • f m n}
(m : M)
(n : N) :
⇑(⇑(linear_map.mk₂' R S f H1 H2 H3 H4) m) n = f m n
theorem
linear_map.ext₂
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S R P]
{f g : M →ₗ[R] N →ₗ[S] P}
(H : ∀ (m : M) (n : N), ⇑(⇑f m) n = ⇑(⇑g m) n) :
f = g
def
linear_map.flip
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S R P]
(f : M →ₗ[R] N →ₗ[S] 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₂' S R (λ (n : N) (m : M), ⇑(⇑f m) n) _ _ _ _
@[simp]
theorem
linear_map.flip_apply
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S R P]
(f : M →ₗ[R] N →ₗ[S] P)
(m : M)
(n : N) :
theorem
linear_map.flip_inj
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S R P]
{f g : M →ₗ[R] N →ₗ[S] P}
(H : f.flip = g.flip) :
f = g
theorem
linear_map.map_zero₂
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S R P]
(f : M →ₗ[R] N →ₗ[S] P)
(y : N) :
theorem
linear_map.map_neg₂
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{N : Type u_4}
{M' : Type u_6}
{P' : Type u_8}
[add_comm_monoid N]
[add_comm_group M']
[add_comm_group P']
[semimodule S N]
[semimodule R M']
[semimodule R P']
[semimodule S P']
[smul_comm_class S R P']
(f : M' →ₗ[R] N →ₗ[S] P')
(x : M')
(y : N) :
theorem
linear_map.map_sub₂
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{N : Type u_4}
{M' : Type u_6}
{P' : Type u_8}
[add_comm_monoid N]
[add_comm_group M']
[add_comm_group P']
[semimodule S N]
[semimodule R M']
[semimodule R P']
[semimodule S P']
[smul_comm_class S R P']
(f : M' →ₗ[R] N →ₗ[S] P')
(x y : M')
(z : N) :
theorem
linear_map.map_add₂
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S R P]
(f : M →ₗ[R] N →ₗ[S] P)
(x₁ x₂ : M)
(y : N) :
theorem
linear_map.map_smul₂
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S R P]
(f : M →ₗ[R] N →ₗ[S] P)
(r : R)
(x : M)
(y : N) :
theorem
linear_map.map_sum₂
{R : Type u_1}
[semiring R]
{S : Type u_2}
[semiring S]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule S N]
[semimodule R P]
[semimodule S P]
[smul_comm_class S R P]
{ι : Type u_6}
(f : M →ₗ[R] N →ₗ[S] P)
(t : finset ι)
(x : ι → M)
(y : N) :
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.
This is a shorthand for mk₂' for the common case when R = S.
Equations
- linear_map.mk₂ R f H1 H2 H3 H4 = linear_map.mk₂' R R f H1 H2 H3 H4
@[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
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 _, 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) :
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_8, 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
theorem
linear_map.lsmul_injective
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
{x : R}
(hx : x ≠ 0) :
function.injective ⇑(⇑(linear_map.lsmul R M) x)
inductive
tensor_product.eqv
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
free_add_monoid (M × N) → free_add_monoid (M × N) → Prop
- of_zero_left : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_3) (N : Type u_4) [_inst_3 : add_comm_monoid M] [_inst_4 : add_comm_monoid N] [_inst_8 : semimodule R M] [_inst_9 : 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_3) (N : Type u_4) [_inst_3 : add_comm_monoid M] [_inst_4 : add_comm_monoid N] [_inst_8 : semimodule R M] [_inst_9 : 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_3) (N : Type u_4) [_inst_3 : add_comm_monoid M] [_inst_4 : add_comm_monoid N] [_inst_8 : semimodule R M] [_inst_9 : 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_3) (N : Type u_4) [_inst_3 : add_comm_monoid M] [_inst_4 : add_comm_monoid N] [_inst_8 : semimodule R M] [_inst_9 : 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_3) (N : Type u_4) [_inst_3 : add_comm_monoid M] [_inst_4 : add_comm_monoid N] [_inst_8 : semimodule R M] [_inst_9 : 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_3) (N : Type u_4) [_inst_3 : add_comm_monoid M] [_inst_4 : add_comm_monoid N] [_inst_8 : semimodule R M] [_inst_9 : 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_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
Type (max u_3 u_4)
The tensor product of two semimodules M and N over the same commutative semiring R.
The localized notations are M ⊗ N and M ⊗[R] N, accessed by open_locale tensor_product.
Equations
- M ⊗ N = (add_con_gen (tensor_product.eqv R M N)).quotient
@[instance]
def
tensor_product.add_zero_class
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
add_zero_class (M ⊗ N)
Equations
- tensor_product.add_zero_class M N = {zero := add_monoid.zero (add_con_gen (tensor_product.eqv R M N)).add_monoid, add := add_monoid.add (add_con_gen (tensor_product.eqv R M N)).add_monoid, zero_add := _, add_zero := _}
@[instance]
def
tensor_product.add_comm_semigroup
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
add_comm_semigroup (M ⊗ N)
Equations
- tensor_product.add_comm_semigroup M N = {add := add_monoid.add (add_con_gen (tensor_product.eqv R M N)).add_monoid, add_assoc := _, add_comm := _}
@[instance]
def
tensor_product.inhabited
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
Equations
- tensor_product.inhabited M N = {default := 0}
def
tensor_product.tmul
(R : Type u_1)
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(m : M)
(n : N) :
M ⊗ N
The canonical function M → N → M ⊗ N. The localized notations are m ⊗ₜ n and m ⊗ₜ[R] n,
accessed by open_locale tensor_product.
Equations
- 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_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
{C : M ⊗ N → Prop}
(z : M ⊗ N)
(C0 : C 0)
(C1 : ∀ {x : M} {y : N}, C (x ⊗ₜ[R] y))
(Cp : ∀ {x y : M ⊗ N}, C x → C y → C (x + y)) :
C z
@[simp]
theorem
tensor_product.zero_tmul
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(n : N) :
theorem
tensor_product.add_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(m₁ m₂ : M)
(n : N) :
@[simp]
theorem
tensor_product.tmul_zero
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(m : M) :
theorem
tensor_product.tmul_add
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(m : M)
(n₁ n₂ : N) :
@[class]
structure
tensor_product.compatible_smul
(R : Type u_1)
[comm_semiring R]
(R' : Type u_2)
[comm_semiring R']
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N] :
Type
A typeclass for has_scalar structures which can be moved across a tensor product.
This typeclass is generated automatically from a is_scalar_tower instance, but exists so that
we can also add an instance for add_comm_group.int_module, allowing z • to be moved even if
R does not support negation.
Note that semimodule R' (M ⊗[R] N) is available even without this typeclass on R'; it's only
needed if tensor_product.smul_tmul, tensor_product.smul_tmul', or tensor_product.tmul_smul is
used.
@[instance]
def
tensor_product.compatible_smul.is_scalar_tower
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[has_scalar R' R]
[is_scalar_tower R' R M]
[is_scalar_tower R' R N] :
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
theorem
tensor_product.smul_tmul
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[tensor_product.compatible_smul R R' M N]
(r : R')
(m : M)
(n : N) :
smul can be moved from one side of the product to the other .
def
tensor_product.smul.aux
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
{R' : Type u_2}
[has_scalar R' M]
(r : R') :
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_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
{R' : Type u_2}
[has_scalar R' M]
(r : R')
(m : M)
(n : N) :
⇑(tensor_product.smul.aux r) (free_add_monoid.of (m, n)) = (r • m) ⊗ₜ[R] n
@[nolint, instance]
def
tensor_product.has_scalar'
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N] :
has_scalar R' (M ⊗ N)
Equations
- tensor_product.has_scalar' = {smul := λ (r : R'), ⇑((add_con_gen (tensor_product.eqv R M N)).lift (tensor_product.smul.aux r) _)}
@[instance]
def
tensor_product.has_scalar
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
has_scalar R (M ⊗ N)
theorem
tensor_product.smul_zero
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N]
(r : R') :
theorem
tensor_product.smul_add
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N]
(r : R')
(x y : M ⊗ N) :
theorem
tensor_product.zero_smul
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N]
(x : M ⊗ N) :
theorem
tensor_product.one_smul
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N]
(x : M ⊗ N) :
theorem
tensor_product.add_smul
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N]
(r s : R')
(x : M ⊗ N) :
@[instance]
def
tensor_product.add_comm_monoid
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
add_comm_monoid (M ⊗ N)
Equations
- tensor_product.add_comm_monoid = {add := add_comm_semigroup.add (tensor_product.add_comm_semigroup M N), add_assoc := _, zero := add_zero_class.zero (tensor_product.add_zero_class M N), zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (v : M ⊗ N), n • v, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[instance]
def
tensor_product.semimodule'
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N] :
semimodule R' (M ⊗ N)
Equations
- tensor_product.semimodule' = have this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n, from tensor_product.semimodule'._proof_3, {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 := _}
@[instance]
def
tensor_product.semimodule
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
semimodule R (M ⊗ N)
@[nolint]
theorem
tensor_product.smul_tmul'
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N]
[tensor_product.compatible_smul R R' M N]
(r : R')
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.tmul_smul
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[comm_semiring R']
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
[semimodule R' M]
[semimodule R' N]
[smul_comm_class R R' M]
[smul_comm_class R R' N]
[tensor_product.compatible_smul R R' M N]
(r : R')
(x : M)
(y : N) :
def
tensor_product.mk
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
The canonical bilinear map M → N → M ⊗[R] N.
Equations
- 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 _
@[simp]
theorem
tensor_product.mk_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(m : M)
(n : N) :
theorem
tensor_product.ite_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(x₁ : M)
(x₂ : N)
(P : Prop)
[decidable P] :
theorem
tensor_product.tmul_ite
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(x₁ : M)
(x₂ : N)
(P : Prop)
[decidable P] :
theorem
tensor_product.sum_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
{α : Type u_2}
(s : finset α)
(m : α → M)
(n : N) :
theorem
tensor_product.tmul_sum
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(m : M)
{α : Type u_2}
(s : finset α)
(n : α → N) :
def
tensor_product.lift_aux
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : M →ₗ[R] N →ₗ[R] P) :
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_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : M →ₗ[R] N →ₗ[R] P)
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.lift_aux.smul
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
{f : M →ₗ[R] N →ₗ[R] P}
(r : R)
(x : M ⊗ N) :
⇑(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_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : M →ₗ[R] N →ₗ[R] P) :
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_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
{f : M →ₗ[R] N →ₗ[R] P}
(x : M)
(y : N) :
@[simp]
theorem
tensor_product.lift.tmul'
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
{f : M →ₗ[R] N →ₗ[R] P}
(x : M)
(y : N) :
theorem
tensor_product.ext
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
{g h : M ⊗ N →ₗ[R] P}
(H : ∀ (x : M) (y : N), ⇑g (x ⊗ₜ[R] y) = ⇑h (x ⊗ₜ[R] y)) :
g = h
theorem
tensor_product.lift.unique
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
{f : M →ₗ[R] N →ₗ[R] P}
{g : M ⊗ N →ₗ[R] P}
(H : ∀ (x : M) (y : N), ⇑g (x ⊗ₜ[R] y) = ⇑(⇑f x) y) :
g = tensor_product.lift f
theorem
tensor_product.lift_mk
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
theorem
tensor_product.lift_compr₂
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
{f : M →ₗ[R] N →ₗ[R] P}
(g : P →ₗ[R] Q) :
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_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : M ⊗ N →ₗ[R] P) :
tensor_product.lift ((tensor_product.mk R M N).compr₂ f) = f
@[ext]
theorem
tensor_product.mk_compr₂_inj
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
{g h : M ⊗ N →ₗ[R] P}
(H : (tensor_product.mk R M N).compr₂ g = (tensor_product.mk R M N).compr₂ h) :
g = h
Using this as the @[ext] lemma instead of tensor_product.ext allows ext to apply lemmas
specific to M →ₗ _ and N →ₗ _.
def
tensor_product.uncurry
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
(P : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
Linearly constructing a linear map M ⊗ N → P given a bilinear map M → N → P
with the property that its composition with the canonical bilinear map M → N → M ⊗ N is
the given bilinear map M → N → P.
Equations
- 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_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : M →ₗ[R] N →ₗ[R] P)
(m : M)
(n : N) :
def
tensor_product.lift.equiv
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
(P : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
A linear equivalence constructing a linear map M ⊗ N → P given a bilinear map M → N → P
with the property that its composition with the canonical bilinear map M → N → M ⊗ N is
the given bilinear map M → N → P.
def
tensor_product.lcurry
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
(P : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
Given a linear map M ⊗ N → P, compose it with the canonical bilinear map M → N → M ⊗ N to
form a bilinear map M → N → P.
Equations
- 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_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : M ⊗ N →ₗ[R] P)
(m : M)
(n : N) :
def
tensor_product.curry
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : M ⊗ N →ₗ[R] P) :
Given a linear map M ⊗ N → P, compose it with the canonical bilinear map M → N → M ⊗ N to
form a bilinear map M → N → P.
Equations
- 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_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : M ⊗ N →ₗ[R] P)
(m : M)
(n : N) :
theorem
tensor_product.ext_threefold
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
{g h : M ⊗ N ⊗ P →ₗ[R] Q}
(H : ∀ (x : M) (y : N) (z : P), ⇑g (x ⊗ₜ[R] y ⊗ₜ[R] z) = ⇑h (x ⊗ₜ[R] y ⊗ₜ[R] z)) :
g = h
theorem
tensor_product.ext_fourfold
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
{S : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
[semimodule R S]
{g h : M ⊗ N ⊗ P ⊗ Q →ₗ[R] S}
(H : ∀ (w : M) (x : N) (y : P) (z : Q), ⇑g (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) = ⇑h (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)) :
g = h
def
tensor_product.lid
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
[add_comm_monoid M]
[semimodule R M] :
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_3}
[add_comm_monoid M]
[semimodule R M]
(m : M)
(r : R) :
@[simp]
theorem
tensor_product.lid_symm_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
[add_comm_monoid M]
[semimodule R M]
(m : M) :
def
tensor_product.comm
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
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_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.comm_symm_tmul
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N]
(m : M)
(n : N) :
def
tensor_product.rid
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
[add_comm_monoid M]
[semimodule R M] :
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_3}
[add_comm_monoid M]
[semimodule R M]
(m : M)
(r : R) :
@[simp]
theorem
tensor_product.rid_symm_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
[add_comm_monoid M]
[semimodule R M]
(m : M) :
def
tensor_product.assoc
(R : Type u_1)
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
(P : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
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_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(m : M)
(n : N)
(p : P) :
@[simp]
theorem
tensor_product.assoc_symm_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(m : M)
(n : N)
(p : P) :
def
tensor_product.map
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
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_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q)
(m : M)
(n : N) :
theorem
tensor_product.map_comp
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
{P' : Type u_8}
{Q' : Type u_9}
[add_comm_monoid P']
[semimodule R P']
[add_comm_monoid Q']
[semimodule R Q']
(f₂ : P →ₗ[R] P')
(f₁ : M →ₗ[R] P)
(g₂ : Q →ₗ[R] Q')
(g₁ : N →ₗ[R] Q) :
tensor_product.map (f₂.comp f₁) (g₂.comp g₁) = (tensor_product.map f₂ g₂).comp (tensor_product.map f₁ g₁)
theorem
tensor_product.lift_comp_map
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
{Q' : Type u_9}
[add_comm_monoid Q']
[semimodule R Q']
(i : P →ₗ[R] Q →ₗ[R] Q')
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(tensor_product.lift i).comp (tensor_product.map f g) = tensor_product.lift ((i.comp f).compl₂ g)
def
tensor_product.congr
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(f : M ≃ₗ[R] P)
(g : N ≃ₗ[R] Q) :
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_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(f : M ≃ₗ[R] P)
(g : N ≃ₗ[R] Q)
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.congr_symm_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(f : M ≃ₗ[R] P)
(g : N ≃ₗ[R] Q)
(p : P)
(q : Q) :
def
linear_map.ltensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : N →ₗ[R] P) :
ltensor M f : M ⊗ N →ₗ M ⊗ P is the natural linear map induced by f : N →ₗ P.
Equations
def
linear_map.rtensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : N →ₗ[R] P) :
rtensor f M : N₁ ⊗ M →ₗ N₂ ⊗ M is the natural linear map induced by f : N₁ →ₗ N₂.
Equations
@[simp]
theorem
linear_map.ltensor_tmul
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : N →ₗ[R] P)
(m : M)
(n : N) :
@[simp]
theorem
linear_map.rtensor_tmul
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : N →ₗ[R] P)
(m : M)
(n : N) :
def
linear_map.ltensor_hom
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
ltensor_hom M is the natural linear map that sends a linear map f : N →ₗ P to M ⊗ f.
Equations
- linear_map.ltensor_hom M = {to_fun := linear_map.ltensor M _inst_10, map_add' := _, map_smul' := _}
def
linear_map.rtensor_hom
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
rtensor_hom M is the natural linear map that sends a linear map f : N →ₗ P to M ⊗ f.
Equations
- linear_map.rtensor_hom M = {to_fun := λ (f : N →ₗ[R] P), linear_map.rtensor M f, map_add' := _, map_smul' := _}
@[simp]
theorem
linear_map.coe_ltensor_hom
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
@[simp]
theorem
linear_map.coe_rtensor_hom
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
@[simp]
theorem
linear_map.ltensor_add
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f g : N →ₗ[R] P) :
linear_map.ltensor M (f + g) = linear_map.ltensor M f + linear_map.ltensor M g
@[simp]
theorem
linear_map.rtensor_add
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f g : N →ₗ[R] P) :
linear_map.rtensor M (f + g) = linear_map.rtensor M f + linear_map.rtensor M g
@[simp]
theorem
linear_map.ltensor_zero
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
linear_map.ltensor M 0 = 0
@[simp]
theorem
linear_map.rtensor_zero
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P] :
linear_map.rtensor M 0 = 0
@[simp]
theorem
linear_map.ltensor_smul
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(r : R)
(f : N →ₗ[R] P) :
linear_map.ltensor M (r • f) = r • linear_map.ltensor M f
@[simp]
theorem
linear_map.rtensor_smul
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(r : R)
(f : N →ₗ[R] P) :
linear_map.rtensor M (r • f) = r • linear_map.rtensor M f
theorem
linear_map.ltensor_comp
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(g : P →ₗ[R] Q)
(f : N →ₗ[R] P) :
linear_map.ltensor M (g.comp f) = (linear_map.ltensor M g).comp (linear_map.ltensor M f)
theorem
linear_map.rtensor_comp
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(g : P →ₗ[R] Q)
(f : N →ₗ[R] P) :
linear_map.rtensor M (g.comp f) = (linear_map.rtensor M g).comp (linear_map.rtensor M f)
@[simp]
theorem
linear_map.ltensor_id
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
@[simp]
theorem
linear_map.rtensor_id
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
(N : Type u_4)
[add_comm_monoid M]
[add_comm_monoid N]
[semimodule R M]
[semimodule R N] :
@[simp]
theorem
linear_map.ltensor_comp_rtensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(linear_map.ltensor P g).comp (linear_map.rtensor N f) = tensor_product.map f g
@[simp]
theorem
linear_map.rtensor_comp_ltensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(linear_map.rtensor Q f).comp (linear_map.ltensor M g) = tensor_product.map f g
@[simp]
theorem
linear_map.map_comp_rtensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
{S : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
[semimodule R S]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q)
(f' : S →ₗ[R] M) :
(tensor_product.map f g).comp (linear_map.rtensor N f') = tensor_product.map (f.comp f') g
@[simp]
theorem
linear_map.map_comp_ltensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
{S : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
[semimodule R S]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q)
(g' : S →ₗ[R] N) :
(tensor_product.map f g).comp (linear_map.ltensor M g') = tensor_product.map f (g.comp g')
@[simp]
theorem
linear_map.rtensor_comp_map
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
{S : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
[semimodule R S]
(f' : P →ₗ[R] S)
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(linear_map.rtensor Q f').comp (tensor_product.map f g) = tensor_product.map (f'.comp f) g
@[simp]
theorem
linear_map.ltensor_comp_map
{R : Type u_1}
[comm_semiring R]
(M : Type u_3)
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
{S : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[semimodule R M]
[semimodule R N]
[semimodule R P]
[semimodule R Q]
[semimodule R S]
(g' : Q →ₗ[R] S)
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(linear_map.ltensor P g').comp (tensor_product.map f g) = tensor_product.map f (g'.comp g)
def
tensor_product.neg.aux
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[semimodule R M]
[semimodule R N] :
free_add_monoid (M × N) →+ M ⊗ N
Auxiliary function to defining negation multiplication on tensor product.
Equations
- tensor_product.neg.aux R = ⇑free_add_monoid.lift (λ (p : M × N), (-p.fst) ⊗ₜ[R] p.snd)
theorem
tensor_product.neg.aux_of
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[semimodule R M]
[semimodule R N]
(m : M)
(n : N) :
⇑(tensor_product.neg.aux R) (free_add_monoid.of (m, n)) = (-m) ⊗ₜ[R] n
@[instance]
def
tensor_product.has_neg
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[semimodule R M]
[semimodule R N] :
Equations
- tensor_product.has_neg = {neg := ⇑((add_con_gen (tensor_product.eqv R M N)).lift (tensor_product.neg.aux R) tensor_product.has_neg._proof_1)}
@[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]
[semimodule R M]
[semimodule R N] :
add_comm_group (M ⊗ N)
Equations
- tensor_product.add_comm_group = {add := add_comm_monoid.add infer_instance, add_assoc := _, zero := add_comm_monoid.zero infer_instance, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg tensor_product.has_neg, sub := λ (_x _x_1 : M ⊗ N), add_zero_class.add _x (-_x_1), sub_eq_add_neg := _, add_left_neg := _, add_comm := _}
theorem
tensor_product.neg_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[semimodule R M]
[semimodule R N]
(m : M)
(n : N) :
theorem
tensor_product.tmul_neg
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[semimodule R M]
[semimodule R N]
(m : M)
(n : N) :
theorem
tensor_product.tmul_sub
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[semimodule R M]
[semimodule R N]
(m : M)
(n₁ n₂ : N) :
theorem
tensor_product.sub_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[semimodule R M]
[semimodule R N]
(m₁ m₂ : M)
(n : N) :
@[instance]
def
tensor_product.compatible_smul.int
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[semimodule R M]
[semimodule R N]
[semimodule ℤ M]
[semimodule ℤ N] :
While the tensor product will automatically inherit a ℤ-module structure from
add_comm_group.int_module, that structure won't be compatible with lemmas like tmul_smul unless
we use a ℤ-module instance provided by tensor_product.semimodule'.
When R is a ring we get the required tensor_product.compatible_smul instance through
is_scalar_tower, but when it is only a semiring we need to build it from scratch.
The instance diamond in compatible_smul doesn't matter because it's in Prop.
Equations
@[simp]
theorem
linear_map.ltensor_sub
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f g : N →ₗ[R] P) :
linear_map.ltensor M (f - g) = linear_map.ltensor M f - linear_map.ltensor M g
@[simp]
theorem
linear_map.rtensor_sub
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f g : N →ₗ[R] P) :
linear_map.rtensor M (f - g) = linear_map.rtensor M f - linear_map.rtensor M g
@[simp]
theorem
linear_map.ltensor_neg
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : N →ₗ[R] P) :
linear_map.ltensor M (-f) = -linear_map.ltensor M f
@[simp]
theorem
linear_map.rtensor_neg
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[semimodule R M]
[semimodule R N]
[semimodule R P]
(f : N →ₗ[R] P) :
linear_map.rtensor M (-f) = -linear_map.rtensor M f