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
- 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.
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
- tensor_product R M N = (add_con_gen (tensor_product.eqv R M N)).quotient
Instances for tensor_product
- tensor_product.add_zero_class
- tensor_product.add_comm_semigroup
- tensor_product.inhabited
- tensor_product.left_has_smul
- tensor_product.has_smul
- tensor_product.add_comm_monoid
- tensor_product.left_distrib_mul_action
- tensor_product.distrib_mul_action
- tensor_product.left_module
- tensor_product.module
- tensor_product.is_central_scalar
- tensor_product.is_scalar_tower_left
- tensor_product.is_scalar_tower_right
- tensor_product.is_scalar_tower
- tensor_product.has_neg
- tensor_product.add_comm_group
- module.finite.base_change
- module.finite.tensor_product
- algebra.tensor_product.tensor_product.has_one
- algebra.tensor_product.tensor_product.add_monoid_with_one
- algebra.tensor_product.tensor_product.semiring
- algebra.tensor_product.left_algebra
- algebra.tensor_product.tensor_product.algebra
- algebra.tensor_product.tensor_product.is_scalar_tower
- algebra.tensor_product.tensor_product.ring
- algebra.tensor_product.tensor_product.comm_ring
- module.free.tensor
- tensor_product.lie_module.lie_ring_module
- tensor_product.lie_module.lie_module
- lie_algebra.extend_scalars.tensor_product.has_bracket
- lie_algebra.extend_scalars.tensor_product.lie_ring
- lie_algebra.extend_scalars.lie_algebra
- kaehler_differential.module_3
- kaehler_differential.is_scalar_tower
- algebra.formally_unramified.base_change
- algebra.formally_smooth.base_change
- algebra.formally_etale.base_change
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 := _}
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 := _}
Equations
- tensor_product.inhabited M N = {default := 0}
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))
A typeclass for has_smul
structures which can be moved across a tensor product.
This typeclass is generated automatically from a is_scalar_tower
instance, but exists so that
we can also add an instance for add_comm_group.int_module
, allowing z •
to be moved even if
R
does not support negation.
Note that module R' (M ⊗[R] N)
is available even without this typeclass on R'
; it's only
needed if tensor_product.smul_tmul
, tensor_product.smul_tmul'
, or tensor_product.tmul_smul
is
used.
Instances of this typeclass
Instances of other typeclasses for tensor_product.compatible_smul
- tensor_product.compatible_smul.has_sizeof_inst
Note that this provides the default compatible_smul R R M N
instance through
mul_action.is_scalar_tower.left
.
Equations
smul
can be moved from one side of the product to the other .
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)
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_smul = {smul := λ (r : R'), ⇑((add_con_gen (tensor_product.eqv R M N)).lift (tensor_product.smul.aux r) _)}
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 : tensor_product R M N), n • v, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
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_smul := {smul := has_smul.smul tensor_product.left_has_smul}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Equations
- tensor_product.left_module = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul tensor_product.left_has_smul}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
Equations
is_scalar_tower R'₂ R' M
implies is_scalar_tower R'₂ R' (M ⊗[R] N)
is_scalar_tower R'₂ R' N
implies is_scalar_tower R'₂ R' (M ⊗[R] N)
A short-cut instance for the common case, where the requirements for the compatible_smul
instances are sufficient.
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 _
The simple (aka pure) elements span the tensor product.
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)) _
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' := _}
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 →ₗ _
.
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
A linear equivalence constructing a linear map M ⊗ N → P
given a bilinear map M → N → P
with the property that its composition with the canonical bilinear map M → N → M ⊗ N
is
the given bilinear map M → N → P
.
Equations
- tensor_product.lift.equiv R M N P = {to_fun := (tensor_product.uncurry R M N P).to_fun, map_add' := _, map_smul' := _, inv_fun := λ (f : tensor_product R M N →ₗ[R] P), (tensor_product.mk R M N).compr₂ f, left_inv := _, right_inv := _}
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)
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
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) _ _
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) _ _
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)
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 (tensor_product R M (tensor_product R N P))).comp (tensor_product.mk R M (tensor_product R N P))))) (tensor_product.lift ((tensor_product.uncurry R N P (tensor_product R (tensor_product R M N) P)).comp (tensor_product.curry (tensor_product.mk R (tensor_product R M N) P)))) _ _
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)
Given submodules p ⊆ P
and q ⊆ Q
, this is the natural map: p ⊗ q → P ⊗ Q
.
Equations
The tensor product of a pair of linear maps between modules, bilinear in both maps.
The canonical linear map from P ⊗[R] (M →ₗ[R] Q)
to (M →ₗ[R] P ⊗[R] Q)
Equations
- tensor_product.ltensor_hom_to_hom_ltensor R M P Q = tensor_product.lift ((linear_map.llcomp R M Q (tensor_product R P Q)).comp (tensor_product.mk R P Q))
The canonical linear map from (M →ₗ[R] P) ⊗[R] Q
to (M →ₗ[R] P ⊗[R] Q)
Equations
- tensor_product.rtensor_hom_to_hom_rtensor R M P Q = tensor_product.lift ((linear_map.llcomp R M P (tensor_product R P Q)).comp (tensor_product.mk R P Q).flip).flip
The linear map from (M →ₗ P) ⊗ (N →ₗ Q)
to (M ⊗ N →ₗ P ⊗ Q)
sending f ⊗ₜ g
to
the tensor_product.map f g
, the tensor product of the two maps.
Equations
- tensor_product.hom_tensor_hom_map R M N P Q = tensor_product.lift (tensor_product.map_bilinear R M N P Q)
If M
and P
are linearly equivalent and N
and Q
are linearly equivalent
then M ⊗ N
and P ⊗ Q
are linearly equivalent.
Equations
- tensor_product.congr f g = linear_equiv.of_linear (tensor_product.map ↑f ↑g) (tensor_product.map ↑(f.symm) ↑(g.symm)) _ _
A tensor product analogue of mul_left_comm
.
Equations
- tensor_product.left_comm R M N P = let e₁ : tensor_product R M (tensor_product R N P) ≃ₗ[R] tensor_product R (tensor_product R M N) P := (tensor_product.assoc R M N P).symm, e₂ : tensor_product R (tensor_product R M N) P ≃ₗ[R] tensor_product R (tensor_product R N M) P := tensor_product.congr (tensor_product.comm R M N) 1, e₃ : tensor_product R (tensor_product R N M) P ≃ₗ[R] tensor_product R N (tensor_product R M P) := tensor_product.assoc R N M P in e₁.trans (e₂.trans e₃)
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₁ : tensor_product R (tensor_product R M N) (tensor_product R P Q) ≃ₗ[R] tensor_product R M (tensor_product R N (tensor_product R P Q)) := tensor_product.assoc R M N (tensor_product R P Q), e₂ : tensor_product R M (tensor_product R N (tensor_product R P Q)) ≃ₗ[R] tensor_product R M (tensor_product R P (tensor_product R N Q)) := tensor_product.congr 1 (tensor_product.left_comm R N P Q), e₃ : tensor_product R M (tensor_product R P (tensor_product R N Q)) ≃ₗ[R] tensor_product R (tensor_product R M P) (tensor_product R N Q) := (tensor_product.assoc R M P (tensor_product R N Q)).symm in e₁.trans (e₂.trans e₃)
This special case is useful for describing the interplay between dual_tensor_hom_equiv
and
composition of linear maps.
E.g., composition of linear maps gives a map (M → N) ⊗ (N → P) → (M → P)
, and applying
dual_tensor_hom_equiv.symm
to the three hom-modules gives a map
(M.dual ⊗ N) ⊗ (N.dual ⊗ P) → (M.dual ⊗ P)
, which agrees with the application of contract_right
on N ⊗ N.dual
after the suitable rebracketting.
Equations
- tensor_product.tensor_tensor_tensor_assoc R M N P Q = (tensor_product.assoc R (tensor_product R M N) P Q).symm.trans (tensor_product.congr (tensor_product.assoc R M N P) 1)
ltensor M f : M ⊗ N →ₗ M ⊗ P
is the natural linear map induced by f : N →ₗ P
.
Equations
rtensor f M : N₁ ⊗ M →ₗ N₂ ⊗ M
is the natural linear map induced by f : N₁ →ₗ N₂
.
Equations
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' := _}
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' := _}
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)
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)}
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 : tensor_product R M N), add_zero_class.add _x (-_x_1), sub_eq_add_neg := _, zsmul := λ (n : ℤ) (v : tensor_product R M N), n • v, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
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
.