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
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.
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) _ _ _ _
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
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' := _}
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
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
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
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
Scalar multiplication as a bilinear map R → M → M
.
Equations
- linear_map.lsmul R M = linear_map.mk₂ R has_scalar.smul _ _ _ _
- 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.
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
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_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.
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)
Equations
- tensor_product.has_scalar' = {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 : M ⊗ N), n • v, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
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 := _}
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 _
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' := _}
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
.
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 (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)))) _ _
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)
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)) _ _
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_10, 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 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 := _}
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
.