Tensor product of modules over commutative semirings. #
This file constructs the tensor product of modules over commutative semirings. Given a semiring
R and modules over it M and N, the standard construction of the tensor product is
tensor_product R M N. It is also a module over R.
It comes with a canonical bilinear map M → N → tensor_product R M N.
Given any bilinear map M → N → P, there is a unique linear map tensor_product R M N → P whose
composition with the canonical bilinear map M → N → tensor_product R M N is the given bilinear
map M → N → P.
We start by proving basic lemmas about bilinear maps.
Notations #
This file uses the localized notation M ⊗ N and M ⊗[R] N for tensor_product R M N, as well
as m ⊗ₜ n and m ⊗ₜ[R] n for tensor_product.tmul R m n.
Tags #
bilinear, tensor, tensor product
inductive
tensor_product.eqv
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
free_add_monoid (M × N) → free_add_monoid (M × N) → Prop
- of_zero_left : ∀ {R : Type u_1} [_inst_1 : comm_semiring R] {M : Type u_4} {N : Type u_5} [_inst_4 : add_comm_monoid M] [_inst_5 : add_comm_monoid N] [_inst_9 : module R M] [_inst_10 : module 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_4} {N : Type u_5} [_inst_4 : add_comm_monoid M] [_inst_5 : add_comm_monoid N] [_inst_9 : module R M] [_inst_10 : module 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_4} {N : Type u_5} [_inst_4 : add_comm_monoid M] [_inst_5 : add_comm_monoid N] [_inst_9 : module R M] [_inst_10 : module 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_4} {N : Type u_5} [_inst_4 : add_comm_monoid M] [_inst_5 : add_comm_monoid N] [_inst_9 : module R M] [_inst_10 : module 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_4} {N : Type u_5} [_inst_4 : add_comm_monoid M] [_inst_5 : add_comm_monoid N] [_inst_9 : module R M] [_inst_10 : module 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_4} {N : Type u_5} [_inst_4 : add_comm_monoid M] [_inst_5 : add_comm_monoid N] [_inst_9 : module R M] [_inst_10 : module 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_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
Type (max u_4 u_5)
The tensor product of two modules M and N over the same commutative semiring R.
The localized notations are M ⊗ N and M ⊗[R] N, accessed by open_locale tensor_product.
Equations
- M ⊗ N = (add_con_gen (tensor_product.eqv R M N)).quotient
@[protected, instance]
def
tensor_product.add_zero_class
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
add_zero_class (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 := _}
@[protected, instance]
def
tensor_product.add_comm_semigroup
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
add_comm_semigroup (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 := _}
@[protected, instance]
def
tensor_product.inhabited
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
Equations
- tensor_product.inhabited M N = {default := 0}
def
tensor_product.tmul
(R : Type u_1)
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(m : M)
(n : N) :
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))
@[protected]
theorem
tensor_product.induction_on
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
{C : 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_4)
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(n : N) :
theorem
tensor_product.add_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(m₁ m₂ : M)
(n : N) :
@[simp]
theorem
tensor_product.tmul_zero
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(m : M) :
theorem
tensor_product.tmul_add
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(m : M)
(n₁ n₂ : N) :
@[class]
structure
tensor_product.compatible_smul
(R : Type u_1)
[comm_semiring R]
(R' : Type u_2)
[monoid R']
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[distrib_mul_action R' N] :
Type
A typeclass for has_scalar structures which can be moved across a tensor product.
This typeclass is generated automatically from a is_scalar_tower instance, but exists so that
we can also add an instance for add_comm_group.int_module, allowing z • to be moved even if
R does not support negation.
Note that module R' (M ⊗[R] N) is available even without this typeclass on R'; it's only
needed if tensor_product.smul_tmul, tensor_product.smul_tmul', or tensor_product.tmul_smul is
used.
@[protected, instance]
def
tensor_product.compatible_smul.is_scalar_tower
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[has_scalar R' R]
[is_scalar_tower R' R M]
[distrib_mul_action R' N]
[is_scalar_tower R' R N] :
tensor_product.compatible_smul R R' M N
Note that this provides the default compatible_smul R R M N instance through
mul_action.is_scalar_tower.left.
Equations
theorem
tensor_product.smul_tmul
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[distrib_mul_action R' N]
[tensor_product.compatible_smul R R' M N]
(r : R')
(m : M)
(n : N) :
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_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
{R' : Type u_2}
[has_scalar R' M]
(r : R') :
free_add_monoid (M × N) →+ 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_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
{R' : Type u_2}
[has_scalar R' M]
(r : R')
(m : M)
(n : N) :
⇑(tensor_product.smul.aux r) (free_add_monoid.of (m, n)) = (r • m) ⊗ₜ[R] n
@[protected, instance]
def
tensor_product.left_has_scalar
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M] :
has_scalar R' (M ⊗ N)
Given two modules over a commutative semiring R, if one of the factors carries a
(distributive) action of a second type of scalars R', which commutes with the action of R, then
the tensor product (over R) carries an action of R'.
This instance defines this R' action in the case that it is the left module which has the R'
action. Two natural ways in which this situation arises are:
- Extension of scalars
- A tensor product of a group representation with a module not carrying an action
Note that in the special case that R = R', since R is commutative, we just get the usual scalar
action on a tensor product of two modules. This special case is important enough that, for
performance reasons, we define it explicitly below.
Equations
- tensor_product.left_has_scalar = {smul := λ (r : R'), ⇑((add_con_gen (tensor_product.eqv R M N)).lift (tensor_product.smul.aux r) _)}
@[protected, instance]
def
tensor_product.has_scalar
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
has_scalar R (M ⊗ N)
@[protected]
theorem
tensor_product.smul_zero
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M]
(r : R') :
@[protected]
theorem
tensor_product.smul_add
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M]
(r : R')
(x y : M ⊗ N) :
@[protected]
theorem
tensor_product.zero_smul
{R : Type u_1}
[comm_semiring R]
{R'' : Type u_3}
[semiring R'']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[module R'' M]
[smul_comm_class R R'' M]
(x : M ⊗ N) :
@[protected]
theorem
tensor_product.one_smul
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M]
(x : M ⊗ N) :
@[protected]
theorem
tensor_product.add_smul
{R : Type u_1}
[comm_semiring R]
{R'' : Type u_3}
[semiring R'']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[module R'' M]
[smul_comm_class R R'' M]
(r s : R'')
(x : M ⊗ N) :
@[protected, instance]
def
tensor_product.add_comm_monoid
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
add_comm_monoid (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 := _}
@[protected, instance]
def
tensor_product.left_distrib_mul_action
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M] :
distrib_mul_action R' (M ⊗ N)
Equations
- tensor_product.left_distrib_mul_action = have this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n, from tensor_product.left_distrib_mul_action._proof_3, {to_mul_action := {to_has_scalar := {smul := has_scalar.smul tensor_product.left_has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[protected, instance]
def
tensor_product.distrib_mul_action
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
distrib_mul_action R (M ⊗ N)
theorem
tensor_product.smul_tmul'
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M]
(r : R')
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.tmul_smul
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M]
[distrib_mul_action R' N]
[tensor_product.compatible_smul R R' M N]
(r : R')
(x : M)
(y : N) :
@[protected, instance]
def
tensor_product.left_module
{R : Type u_1}
[comm_semiring R]
{R'' : Type u_3}
[semiring R'']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[module R'' M]
[smul_comm_class R R'' M] :
Equations
- tensor_product.left_module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul tensor_product.left_has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[protected, instance]
def
tensor_product.module
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
Equations
@[protected, instance]
def
tensor_product.is_central_scalar
{R : Type u_1}
[comm_semiring R]
{R'' : Type u_3}
[semiring R'']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[module R'' M]
[smul_comm_class R R'' M]
[module R''ᵐᵒᵖ M]
[is_central_scalar R'' M] :
is_central_scalar R'' (M ⊗ N)
@[protected, instance]
def
tensor_product.is_scalar_tower_left
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M]
{R'₂ : Type u_9}
[monoid R'₂]
[distrib_mul_action R'₂ M]
[smul_comm_class R R'₂ M]
[has_scalar R'₂ R']
[is_scalar_tower R'₂ R' M] :
is_scalar_tower R'₂ R' (M ⊗ N)
is_scalar_tower R'₂ R' M implies is_scalar_tower R'₂ R' (M ⊗[R] N)
@[protected, instance]
def
tensor_product.is_scalar_tower_right
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M]
{R'₂ : Type u_9}
[monoid R'₂]
[distrib_mul_action R'₂ M]
[smul_comm_class R R'₂ M]
[has_scalar R'₂ R']
[distrib_mul_action R'₂ N]
[distrib_mul_action R' N]
[tensor_product.compatible_smul R R'₂ M N]
[tensor_product.compatible_smul R R' M N]
[is_scalar_tower R'₂ R' N] :
is_scalar_tower R'₂ R' (M ⊗ N)
is_scalar_tower R'₂ R' N implies is_scalar_tower R'₂ R' (M ⊗[R] N)
@[protected, instance]
def
tensor_product.is_scalar_tower
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
[smul_comm_class R R' M]
[has_scalar R' R]
[is_scalar_tower R' R M] :
is_scalar_tower R' R (M ⊗ N)
A short-cut instance for the common case, where the requirements for the compatible_smul
instances are sufficient.
def
tensor_product.mk
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
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_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(m : M)
(n : N) :
theorem
tensor_product.ite_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(x₁ : M)
(x₂ : N)
(P : Prop)
[decidable P] :
theorem
tensor_product.tmul_ite
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(x₁ : M)
(x₂ : N)
(P : Prop)
[decidable P] :
theorem
tensor_product.sum_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
{α : Type u_2}
(s : finset α)
(m : α → M)
(n : N) :
theorem
tensor_product.tmul_sum
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(m : M)
{α : Type u_2}
(s : finset α)
(n : α → N) :
theorem
tensor_product.span_tmul_eq_top
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
The simple (aka pure) elements span the tensor product.
def
tensor_product.lift_aux
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M →ₗ[R] N →ₗ[R] P) :
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_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.lift_aux.smul
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
{f : M →ₗ[R] N →ₗ[R] P}
(r : R)
(x : 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_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M →ₗ[R] N →ₗ[R] P) :
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_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
{f : M →ₗ[R] N →ₗ[R] P}
(x : M)
(y : N) :
@[simp]
theorem
tensor_product.lift.tmul'
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
{f : M →ₗ[R] N →ₗ[R] P}
(x : M)
(y : N) :
theorem
tensor_product.ext'
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
{g h : 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_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
{f : M →ₗ[R] N →ₗ[R] P}
{g : 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_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
theorem
tensor_product.lift_compr₂
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
{f : M →ₗ[R] N →ₗ[R] P}
(g : P →ₗ[R] Q) :
tensor_product.lift (f.compr₂ g) = g.comp (tensor_product.lift f)
theorem
tensor_product.lift_mk_compr₂
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M ⊗ N →ₗ[R] P) :
tensor_product.lift ((tensor_product.mk R M N).compr₂ f) = f
theorem
tensor_product.ext
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
{g h : M ⊗ N →ₗ[R] P}
(H : (tensor_product.mk R M N).compr₂ g = (tensor_product.mk R M N).compr₂ h) :
g = h
This used to be an @[ext] lemma, but it fails very slowly when the ext tactic tries to apply
it in some cases, notably when one wants to show equality of two linear maps. The @[ext]
attribute is now added locally where it is needed. Using this as the @[ext] lemma instead of
tensor_product.ext' allows ext to apply lemmas specific to M →ₗ _ and N →ₗ _.
def
tensor_product.uncurry
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
(P : Type u_6)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
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_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(m : M)
(n : N) :
def
tensor_product.lift.equiv
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
(P : Type u_6)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
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.
@[simp]
theorem
tensor_product.lift.equiv_apply
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
(P : Type u_6)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.lift.equiv_symm_apply
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
(P : Type u_6)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M ⊗ N →ₗ[R] P)
(m : M)
(n : N) :
def
tensor_product.lcurry
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
(P : Type u_6)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
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_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M ⊗ N →ₗ[R] P)
(m : M)
(n : N) :
def
tensor_product.curry
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : 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_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M ⊗ N →ₗ[R] P)
(m : M)
(n : N) :
theorem
tensor_product.curry_injective
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
theorem
tensor_product.ext_threefold
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
{g h : 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_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
{S : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[module R M]
[module R N]
[module R P]
[module R Q]
[module R S]
{g h : 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
@[protected]
def
tensor_product.lid
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
[add_comm_monoid M]
[module 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_4}
[add_comm_monoid M]
[module R M]
(m : M)
(r : R) :
@[simp]
theorem
tensor_product.lid_symm_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
[add_comm_monoid M]
[module R M]
(m : M) :
@[protected]
def
tensor_product.comm
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
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_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.comm_symm_tmul
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(m : M)
(n : N) :
@[protected]
def
tensor_product.rid
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
[add_comm_monoid M]
[module 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_4}
[add_comm_monoid M]
[module R M]
(m : M)
(r : R) :
@[simp]
theorem
tensor_product.rid_symm_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
[add_comm_monoid M]
[module R M]
(m : M) :
@[protected]
def
tensor_product.assoc
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
(P : Type u_6)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
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_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(m : M)
(n : N)
(p : P) :
@[simp]
theorem
tensor_product.assoc_symm_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(m : M)
(n : N)
(p : P) :
def
tensor_product.map
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
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_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q)
(m : M)
(n : N) :
theorem
tensor_product.map_range_eq_span_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(tensor_product.map f g).range = submodule.span R {t : P ⊗ Q | ∃ (m : M) (n : N), ⇑f m ⊗ₜ[R] ⇑g n = t}
@[simp]
def
tensor_product.map_incl
{R : Type u_1}
[comm_semiring R]
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid P]
[add_comm_monoid Q]
[module R P]
[module R Q]
(p : submodule R P)
(q : submodule R Q) :
Given submodules p ⊆ P and q ⊆ Q, this is the natural map: p ⊗ q → P ⊗ Q.
Equations
theorem
tensor_product.map_comp
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
{P' : Type u_9}
{Q' : Type u_10}
[add_comm_monoid P']
[module R P']
[add_comm_monoid Q']
[module R Q']
(f₂ : P →ₗ[R] P')
(f₁ : M →ₗ[R] P)
(g₂ : Q →ₗ[R] Q')
(g₁ : N →ₗ[R] Q) :
tensor_product.map (f₂.comp f₁) (g₂.comp g₁) = (tensor_product.map f₂ g₂).comp (tensor_product.map f₁ g₁)
theorem
tensor_product.lift_comp_map
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
{Q' : Type u_10}
[add_comm_monoid Q']
[module R Q']
(i : P →ₗ[R] Q →ₗ[R] Q')
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(tensor_product.lift i).comp (tensor_product.map f g) = tensor_product.lift ((i.comp f).compl₂ g)
@[simp]
theorem
tensor_product.map_id
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
@[simp]
theorem
tensor_product.map_one
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
tensor_product.map 1 1 = 1
theorem
tensor_product.map_mul
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f₁ f₂ : M →ₗ[R] M)
(g₁ g₂ : N →ₗ[R] N) :
tensor_product.map (f₁ * f₂) (g₁ * g₂) = (tensor_product.map f₁ g₁) * tensor_product.map f₂ g₂
@[protected, simp]
theorem
tensor_product.map_pow
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f : M →ₗ[R] M)
(g : N →ₗ[R] N)
(n : ℕ) :
tensor_product.map f g ^ n = tensor_product.map (f ^ n) (g ^ n)
def
tensor_product.congr
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M ≃ₗ[R] P)
(g : N ≃ₗ[R] Q) :
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_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M ≃ₗ[R] P)
(g : N ≃ₗ[R] Q)
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.congr_symm_tmul
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M ≃ₗ[R] P)
(g : N ≃ₗ[R] Q)
(p : P)
(q : Q) :
def
tensor_product.left_comm
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
(P : Type u_6)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
A tensor product analogue of mul_left_comm.
@[simp]
theorem
tensor_product.left_comm_tmul
(R : Type u_1)
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(m : M)
(n : N)
(p : P) :
@[simp]
theorem
tensor_product.left_comm_symm_tmul
(R : Type u_1)
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(m : M)
(n : N)
(p : P) :
def
tensor_product.tensor_tensor_tensor_comm
(R : Type u_1)
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
(P : Type u_6)
(Q : Type u_7)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q] :
This special case is worth defining explicitly since it is useful for defining multiplication on tensor products of modules carrying multiplications (e.g., associative rings, Lie rings, ...).
E.g., suppose M = P and N = Q and that M and N carry bilinear multiplications:
M ⊗ M → M and N ⊗ N → N. Using map, we can define (M ⊗ M) ⊗ (N ⊗ N) → M ⊗ N which, when
combined with this definition, yields a bilinear multiplication on M ⊗ N:
(M ⊗ N) ⊗ (M ⊗ N) → M ⊗ N. In particular we could use this to define the multiplication in
the tensor_product.semiring instance (currently defined "by hand" using tensor_product.mul).
See also mul_mul_mul_comm.
Equations
- tensor_product.tensor_tensor_tensor_comm R M N P Q = let e₁ : M ⊗ N ⊗ (P ⊗ Q) ≃ₗ[R] M ⊗ (N ⊗ (P ⊗ Q)) := tensor_product.assoc R M N (P ⊗ Q), e₂ : M ⊗ (N ⊗ (P ⊗ Q)) ≃ₗ[R] M ⊗ (P ⊗ (N ⊗ Q)) := tensor_product.congr 1 (tensor_product.left_comm R N P Q), e₃ : M ⊗ (P ⊗ (N ⊗ Q)) ≃ₗ[R] M ⊗ P ⊗ (N ⊗ Q) := (tensor_product.assoc R M P (N ⊗ Q)).symm in e₁.trans (e₂.trans e₃)
@[simp]
theorem
tensor_product.tensor_tensor_tensor_comm_tmul
(R : Type u_1)
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(m : M)
(n : N)
(p : P)
(q : Q) :
@[simp]
theorem
tensor_product.tensor_tensor_tensor_comm_symm_tmul
(R : Type u_1)
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(m : M)
(n : N)
(p : P)
(q : Q) :
def
linear_map.ltensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : N →ₗ[R] P) :
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_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : N →ₗ[R] P) :
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_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : N →ₗ[R] P)
(m : M)
(n : N) :
@[simp]
theorem
linear_map.rtensor_tmul
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : N →ₗ[R] P)
(m : M)
(n : N) :
def
linear_map.ltensor_hom
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
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_11, map_add' := _, map_smul' := _}
def
linear_map.rtensor_hom
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
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_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
@[simp]
theorem
linear_map.coe_rtensor_hom
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
@[simp]
theorem
linear_map.ltensor_add
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f g : N →ₗ[R] P) :
linear_map.ltensor M (f + g) = linear_map.ltensor M f + linear_map.ltensor M g
@[simp]
theorem
linear_map.rtensor_add
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f g : N →ₗ[R] P) :
linear_map.rtensor M (f + g) = linear_map.rtensor M f + linear_map.rtensor M g
@[simp]
theorem
linear_map.ltensor_zero
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
linear_map.ltensor M 0 = 0
@[simp]
theorem
linear_map.rtensor_zero
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P] :
linear_map.rtensor M 0 = 0
@[simp]
theorem
linear_map.ltensor_smul
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(r : R)
(f : N →ₗ[R] P) :
linear_map.ltensor M (r • f) = r • linear_map.ltensor M f
@[simp]
theorem
linear_map.rtensor_smul
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(r : R)
(f : N →ₗ[R] P) :
linear_map.rtensor M (r • f) = r • linear_map.rtensor M f
theorem
linear_map.ltensor_comp
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(g : P →ₗ[R] Q)
(f : N →ₗ[R] P) :
linear_map.ltensor M (g.comp f) = (linear_map.ltensor M g).comp (linear_map.ltensor M f)
theorem
linear_map.rtensor_comp
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(g : P →ₗ[R] Q)
(f : N →ₗ[R] P) :
linear_map.rtensor M (g.comp f) = (linear_map.rtensor M g).comp (linear_map.rtensor M f)
theorem
linear_map.ltensor_mul
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f g : module.End R N) :
linear_map.ltensor M (f * g) = (linear_map.ltensor M f) * linear_map.ltensor M g
theorem
linear_map.rtensor_mul
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f g : module.End R N) :
linear_map.rtensor M (f * g) = (linear_map.rtensor M f) * linear_map.rtensor M g
@[simp]
theorem
linear_map.ltensor_id
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
@[simp]
theorem
linear_map.rtensor_id
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
(N : Type u_5)
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
@[simp]
theorem
linear_map.ltensor_comp_rtensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(linear_map.ltensor P g).comp (linear_map.rtensor N f) = tensor_product.map f g
@[simp]
theorem
linear_map.rtensor_comp_ltensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(linear_map.rtensor Q f).comp (linear_map.ltensor M g) = tensor_product.map f g
@[simp]
theorem
linear_map.map_comp_rtensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
{S : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[module R M]
[module R N]
[module R P]
[module R Q]
[module R S]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q)
(f' : S →ₗ[R] M) :
(tensor_product.map f g).comp (linear_map.rtensor N f') = tensor_product.map (f.comp f') g
@[simp]
theorem
linear_map.map_comp_ltensor
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
{S : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[module R M]
[module R N]
[module R P]
[module R Q]
[module R S]
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q)
(g' : S →ₗ[R] N) :
(tensor_product.map f g).comp (linear_map.ltensor M g') = tensor_product.map f (g.comp g')
@[simp]
theorem
linear_map.rtensor_comp_map
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
{S : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[module R M]
[module R N]
[module R P]
[module R Q]
[module R S]
(f' : P →ₗ[R] S)
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(linear_map.rtensor Q f').comp (tensor_product.map f g) = tensor_product.map (f'.comp f) g
@[simp]
theorem
linear_map.ltensor_comp_map
{R : Type u_1}
[comm_semiring R]
(M : Type u_4)
{N : Type u_5}
{P : Type u_6}
{Q : Type u_7}
{S : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[add_comm_monoid S]
[module R M]
[module R N]
[module R P]
[module R Q]
[module R S]
(g' : Q →ₗ[R] S)
(f : M →ₗ[R] P)
(g : N →ₗ[R] Q) :
(linear_map.ltensor P g').comp (tensor_product.map f g) = tensor_product.map f (g'.comp g)
@[simp]
theorem
linear_map.rtensor_pow
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f : M →ₗ[R] M)
(n : ℕ) :
linear_map.rtensor N f ^ n = linear_map.rtensor N (f ^ n)
@[simp]
theorem
linear_map.ltensor_pow
{R : Type u_1}
[comm_semiring R]
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f : N →ₗ[R] N)
(n : ℕ) :
linear_map.ltensor M f ^ n = linear_map.ltensor M (f ^ n)
def
tensor_product.neg.aux
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N] :
free_add_monoid (M × N) →+ 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]
[module R M]
[module R N]
(m : M)
(n : N) :
⇑(tensor_product.neg.aux R) (free_add_monoid.of (m, n)) = (-m) ⊗ₜ[R] n
@[protected, instance]
def
tensor_product.has_neg
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N] :
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)}
@[protected]
theorem
tensor_product.add_left_neg
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(x : M ⊗ N) :
@[protected, instance]
def
tensor_product.add_comm_group
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N] :
add_comm_group (M ⊗ N)
Equations
- tensor_product.add_comm_group = {add := add_comm_monoid.add tensor_product.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero tensor_product.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul tensor_product.add_comm_monoid, 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 := _, zsmul := λ (n : ℤ) (v : M ⊗ N), n • v, zsmul_zero' := _, zsmul_succ' := _, zsmul_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]
[module R M]
[module 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]
[module R M]
[module 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]
[module R M]
[module 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]
[module R M]
[module R N]
(m₁ m₂ : M)
(n : N) :
@[protected, instance]
def
tensor_product.compatible_smul.int
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
[module ℤ M]
[module ℤ N] :
While the tensor product will automatically inherit a ℤ-module structure from
add_comm_group.int_module, that structure won't be compatible with lemmas like tmul_smul unless
we use a ℤ-module instance provided by tensor_product.left_module.
When R is a ring we get the required tensor_product.compatible_smul instance through
is_scalar_tower, but when it is only a semiring we need to build it from scratch.
The instance diamond in compatible_smul doesn't matter because it's in Prop.
Equations
@[protected, instance]
def
tensor_product.compatible_smul.unit
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
{S : Type u_4}
[monoid S]
[distrib_mul_action S M]
[distrib_mul_action S N]
[tensor_product.compatible_smul R S M N] :
tensor_product.compatible_smul R Sˣ M N
Equations
@[simp]
theorem
linear_map.ltensor_sub
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[module R M]
[module R N]
[module R P]
(f g : N →ₗ[R] P) :
linear_map.ltensor M (f - g) = linear_map.ltensor M f - linear_map.ltensor M g
@[simp]
theorem
linear_map.rtensor_sub
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[module R M]
[module R N]
[module R P]
(f g : N →ₗ[R] P) :
linear_map.rtensor M (f - g) = linear_map.rtensor M f - linear_map.rtensor M g
@[simp]
theorem
linear_map.ltensor_neg
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[module R M]
[module R N]
[module R P]
(f : N →ₗ[R] P) :
linear_map.ltensor M (-f) = -linear_map.ltensor M f
@[simp]
theorem
linear_map.rtensor_neg
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[module R M]
[module R N]
[module R P]
(f : N →ₗ[R] P) :
linear_map.rtensor M (-f) = -linear_map.rtensor M f