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
TensorProduct R M N
. It is also a module over R
.
It comes with a canonical bilinear map
TensorProduct.mk R M N : M →ₗ[R] N →ₗ[R] TensorProduct R M N
.
Given any bilinear map f : M →ₗ[R] N →ₗ[R] P
, there is a unique linear map
TensorProduct.lift f : TensorProduct R M N →ₗ[R] P
whose composition with the canonical bilinear
map TensorProduct.mk
is the given bilinear map f
. Uniqueness is shown in the theorem
TensorProduct.lift.unique
.
Notation #
- This file introduces the notation
M ⊗ N
andM ⊗[R] N
for the tensor product spaceTensorProduct R M N
. - It introduces the notation
m ⊗ₜ n
andm ⊗ₜ[R] n
for the tensor product of two elements, otherwise written asTensorProduct.tmul R m n
.
Tags #
bilinear, tensor, tensor product
The relation on FreeAddMonoid (M × N)
that generates a congruence whose quotient is
the tensor product.
- of_zero_left: ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (n : N), TensorProduct.Eqv R M N (FreeAddMonoid.of (0, n)) 0
- of_zero_right: ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M), TensorProduct.Eqv R M N (FreeAddMonoid.of (m, 0)) 0
- of_add_left: ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m₁ m₂ : M) (n : N), TensorProduct.Eqv R M N (FreeAddMonoid.of (m₁, n) + FreeAddMonoid.of (m₂, n)) (FreeAddMonoid.of (m₁ + m₂, n))
- of_add_right: ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) (n₁ n₂ : N), TensorProduct.Eqv R M N (FreeAddMonoid.of (m, n₁) + FreeAddMonoid.of (m, n₂)) (FreeAddMonoid.of (m, n₁ + n₂))
- of_smul: ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (r : R) (m : M) (n : N), TensorProduct.Eqv R M N (FreeAddMonoid.of (r • m, n)) (FreeAddMonoid.of (m, r • n))
- add_comm: ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x y : FreeAddMonoid (M × N)), TensorProduct.Eqv R M N (x + y) (y + x)
Instances For
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 scoped TensorProduct
.
Equations
- TensorProduct R M N = (addConGen (TensorProduct.Eqv R M N)).Quotient
Instances For
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 scoped TensorProduct
.
Equations
- TensorProduct.«term_⊗_» = Lean.ParserDescr.trailingNode `TensorProduct.term_⊗_ 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 101))
Instances For
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 scoped TensorProduct
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- TensorProduct.add M N = (addConGen (TensorProduct.Eqv R M N)).hasAdd
Equations
Equations
Equations
Equations
- TensorProduct.instInhabited M N = { default := 0 }
The canonical function M → N → M ⊗ N
. The localized notations are m ⊗ₜ n
and m ⊗ₜ[R] n
,
accessed by open scoped TensorProduct
.
Equations
- m ⊗ₜ[R] n = (addConGen (TensorProduct.Eqv R M N)).mk' (FreeAddMonoid.of (m, n))
Instances For
The canonical function M → N → M ⊗ N
.
Equations
- TensorProduct.«term_⊗ₜ_» = Lean.ParserDescr.trailingNode `TensorProduct.term_⊗ₜ_ 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₜ ") (Lean.ParserDescr.cat `term 101))
Instances For
The canonical function M → N → M ⊗ N
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lift an R
-balanced map to the tensor product.
A map f : M →+ N →+ P
additive in both components is R
-balanced, or middle linear with respect
to R
, if scalar multiplication in either argument is equivalent, f (r • m) n = f m (r • n)
.
Note that strictly the first action should be a right-action by R
, but for now R
is commutative
so it doesn't matter.
Equations
- TensorProduct.liftAddHom f hf = (addConGen (TensorProduct.Eqv R M N)).lift (FreeAddMonoid.lift fun (mn : M × N) => (f mn.1) mn.2) ⋯
Instances For
Equations
- TensorProduct.uniqueLeft = { default := 0, uniq := ⋯ }
Equations
- TensorProduct.uniqueRight = { default := 0, uniq := ⋯ }
A typeclass for SMul
structures which can be moved across a tensor product.
This typeclass is generated automatically from an IsScalarTower
instance, but exists so that
we can also add an instance for AddCommGroup.toIntModule
, 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 TensorProduct.smul_tmul
, TensorProduct.smul_tmul'
, or TensorProduct.tmul_smul
is
used.
Instances
Note that this provides the default CompatibleSMul R R M N
instance through
IsScalarTower.left
.
Equations
- ⋯ = ⋯
smul
can be moved from one side of the product to the other .
Auxiliary function to defining scalar multiplication on tensor product.
Instances For
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
- TensorProduct.leftHasSMul = { smul := fun (r : R') => ⇑((addConGen (TensorProduct.Eqv R M N)).lift (TensorProduct.SMul.aux r) ⋯) }
Equations
- TensorProduct.instSMul = TensorProduct.leftHasSMul
Equations
- TensorProduct.addMonoid = AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (v : TensorProduct R M N) => n • v) ⋯ ⋯
Equations
- TensorProduct.addCommMonoid = AddCommMonoid.mk ⋯
Equations
- TensorProduct.leftDistribMulAction = DistribMulAction.mk ⋯ ⋯
Equations
- TensorProduct.instDistribMulAction = TensorProduct.leftDistribMulAction
Equations
- TensorProduct.instModule = TensorProduct.leftModule
Equations
- ⋯ = ⋯
SMulCommClass R' R'₂ M
implies SMulCommClass R' R'₂ (M ⊗[R] N)
Equations
- ⋯ = ⋯
IsScalarTower R'₂ R' M
implies IsScalarTower R'₂ R' (M ⊗[R] N)
Equations
- ⋯ = ⋯
IsScalarTower R'₂ R' N
implies IsScalarTower R'₂ R' (M ⊗[R] N)
Equations
- ⋯ = ⋯
A short-cut instance for the common case, where the requirements for the compatible_smul
instances are sufficient.
Equations
- ⋯ = ⋯
The canonical bilinear map M → N → M ⊗[R] N
.
Equations
- TensorProduct.mk R M N = LinearMap.mk₂ R (fun (x1 : M) (x2 : N) => x1 ⊗ₜ[R] x2) ⋯ ⋯ ⋯ ⋯
Instances For
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
- TensorProduct.liftAux f = TensorProduct.liftAddHom (LinearMap.toAddMonoidHom'.comp f.toAddMonoidHom) ⋯
Instances For
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
- TensorProduct.lift f = { toFun := (↑(TensorProduct.liftAux f)).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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
TensorProduct.ext'
allows ext
to apply lemmas specific to M →ₗ _
and N →ₗ _
.
See note [partially-applied ext lemmas].
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
- TensorProduct.uncurry R M N P = (TensorProduct.lift (LinearMap.lflip ∘ₗ LinearMap.id.flip)).flip
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
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
- TensorProduct.lcurry R M N P = ↑(TensorProduct.lift.equiv R M N P).symm
Instances For
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
- TensorProduct.curry f = (TensorProduct.lcurry R M N P) f
Instances For
Two linear maps (M ⊗ N) ⊗ (P ⊗ Q) → S which agree on all elements of the form (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) are equal.
The base ring is a left identity for the tensor product of modules, up to linear equivalence.
Equations
- TensorProduct.lid R M = LinearEquiv.ofLinear (TensorProduct.lift (LinearMap.lsmul R M)) ((TensorProduct.mk R R M) 1) ⋯ ⋯
Instances For
The tensor product of modules is commutative, up to linear equivalence.
Equations
- TensorProduct.comm R M N = LinearEquiv.ofLinear (TensorProduct.lift (TensorProduct.mk R N M).flip) (TensorProduct.lift (TensorProduct.mk R M N).flip) ⋯ ⋯
Instances For
The base ring is a right identity for the tensor product of modules, up to linear equivalence.
Equations
- TensorProduct.rid R M = (TensorProduct.comm R M R).trans (TensorProduct.lid R M)
Instances For
The associator for tensor product of R-modules, as a linear equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tensor product of a pair of linear maps between modules.
Equations
- TensorProduct.map f g = TensorProduct.lift ((TensorProduct.mk R P Q).compl₂ g ∘ₗ f)
Instances For
Given linear maps f : M → P
, g : N → Q
, if we identify M ⊗ N
with N ⊗ M
and P ⊗ Q
with Q ⊗ P
, then this lemma states that f ⊗ g = g ⊗ f
.
Given linear maps f : M → Q
, g : N → S
, and h : P → T
, if we identify (M ⊗ N) ⊗ P
with M ⊗ (N ⊗ P)
and (Q ⊗ S) ⊗ T
with Q ⊗ (S ⊗ T)
, then this lemma states that
f ⊗ (g ⊗ h) = (f ⊗ g) ⊗ h
.
Given linear maps f : M → Q
, g : N → S
, and h : P → T
, if we identify M ⊗ (N ⊗ P)
with (M ⊗ N) ⊗ P
and Q ⊗ (S ⊗ T)
with (Q ⊗ S) ⊗ T
, then this lemma states that
(f ⊗ g) ⊗ h = f ⊗ (g ⊗ h)
.
Given submodules p ⊆ P
and q ⊆ Q
, this is the natural map: p ⊗ q → P ⊗ Q
.
Equations
- TensorProduct.mapIncl p q = TensorProduct.map p.subtype q.subtype
Instances For
The tensor product of a pair of linear maps between modules, bilinear in both maps.
Equations
- TensorProduct.mapBilinear R M N P Q = LinearMap.mk₂ R TensorProduct.map ⋯ ⋯ ⋯ ⋯
Instances For
The canonical linear map from P ⊗[R] (M →ₗ[R] Q)
to (M →ₗ[R] P ⊗[R] Q)
Equations
- TensorProduct.lTensorHomToHomLTensor R M P Q = TensorProduct.lift (LinearMap.llcomp R M Q (TensorProduct R P Q) ∘ₗ TensorProduct.mk R P Q)
Instances For
The canonical linear map from (M →ₗ[R] P) ⊗[R] Q
to (M →ₗ[R] P ⊗[R] Q)
Equations
- TensorProduct.rTensorHomToHomRTensor R M P Q = TensorProduct.lift (LinearMap.llcomp R M P (TensorProduct R P Q) ∘ₗ (TensorProduct.mk R P Q).flip).flip
Instances For
The linear map from (M →ₗ P) ⊗ (N →ₗ Q)
to (M ⊗ N →ₗ P ⊗ Q)
sending f ⊗ₜ g
to
the TensorProduct.map f g
, the tensor product of the two maps.
Equations
- TensorProduct.homTensorHomMap R M N P Q = TensorProduct.lift (TensorProduct.mapBilinear R M N P Q)
Instances For
This is a binary version of TensorProduct.map
: Given a bilinear map f : M ⟶ P ⟶ Q
and a
bilinear map g : N ⟶ S ⟶ T
, if we think f
and g
as linear maps with two inputs, then
map₂ f g
is a bilinear map taking two inputs M ⊗ N → P ⊗ S → Q ⊗ S
defined by
map₂ f g (m ⊗ n) (p ⊗ s) = f m p ⊗ g n s
.
Mathematically, TensorProduct.map₂
is defined as the composition
M ⊗ N -map→ Hom(P, Q) ⊗ Hom(S, T) -homTensorHomMap→ Hom(P ⊗ S, Q ⊗ T)
.
Equations
- TensorProduct.map₂ f g = TensorProduct.homTensorHomMap R P S Q T ∘ₗ TensorProduct.map f g
Instances For
If M
and P
are linearly equivalent and N
and Q
are linearly equivalent
then M ⊗ N
and P ⊗ Q
are linearly equivalent.
Equations
- TensorProduct.congr f g = LinearEquiv.ofLinear (TensorProduct.map ↑f ↑g) (TensorProduct.map ↑f.symm ↑g.symm) ⋯ ⋯
Instances For
A tensor product analogue of mul_left_comm
.
Equations
- TensorProduct.leftComm R M N P = (TensorProduct.assoc R M N P).symm.trans ((TensorProduct.congr (TensorProduct.comm R M N) 1).trans (TensorProduct.assoc R N M P))
Instances For
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 TensorProduct.semiring
instance (currently defined "by hand" using TensorProduct.mul
).
See also mul_mul_mul_comm
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This special case is useful for describing the interplay between dualTensorHomEquiv
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 contractRight
on N ⊗ N.dual
after the suitable rebracketting.
Equations
- TensorProduct.tensorTensorTensorAssoc R M N P Q = (TensorProduct.assoc R (TensorProduct R M N) P Q).symm.trans (TensorProduct.congr (TensorProduct.assoc R M N P) 1)
Instances For
LinearMap.lTensor M f : M ⊗ N →ₗ M ⊗ P
is the natural linear map
induced by f : N →ₗ P
.
Equations
- LinearMap.lTensor M f = TensorProduct.map LinearMap.id f
Instances For
LinearMap.rTensor M f : N₁ ⊗ M →ₗ N₂ ⊗ M
is the natural linear map
induced by f : N₁ →ₗ N₂
.
Equations
- LinearMap.rTensor M f = TensorProduct.map f LinearMap.id
Instances For
Given a linear map f : N → P
, f ⊗ M
is injective if and only if M ⊗ f
is injective.
Given a linear map f : N → P
, f ⊗ M
is surjective if and only if M ⊗ f
is surjective.
Given a linear map f : N → P
, f ⊗ M
is bijective if and only if M ⊗ f
is bijective.
lTensorHom M
is the natural linear map that sends a linear map f : N →ₗ P
to M ⊗ f
.
Equations
- LinearMap.lTensorHom M = { toFun := LinearMap.lTensor M, map_add' := ⋯, map_smul' := ⋯ }
Instances For
rTensorHom M
is the natural linear map that sends a linear map f : N →ₗ P
to f ⊗ M
.
Equations
- LinearMap.rTensorHom M = { toFun := fun (f : N →ₗ[R] P) => LinearMap.rTensor M f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
LinearEquiv.lTensor M f : M ⊗ N ≃ₗ M ⊗ P
is the natural linear equivalence
induced by f : N ≃ₗ P
.
Equations
- LinearEquiv.lTensor M f = TensorProduct.congr (LinearEquiv.refl R M) f
Instances For
LinearEquiv.rTensor M f : N₁ ⊗ M ≃ₗ N₂ ⊗ M
is the natural linear equivalence
induced by f : N₁ ≃ₗ N₂
.
Equations
- LinearEquiv.rTensor M f = TensorProduct.congr f (LinearEquiv.refl R M)
Instances For
Auxiliary function to defining negation multiplication on tensor product.
Equations
- TensorProduct.Neg.aux R = TensorProduct.lift (TensorProduct.mk R M N ∘ₗ (-LinearMap.id))
Instances For
Equations
- TensorProduct.neg = { neg := ⇑(TensorProduct.Neg.aux R) }
Equations
- TensorProduct.addCommGroup = AddCommGroup.mk ⋯
While the tensor product will automatically inherit a ℤ-module structure from
AddCommGroup.toIntModule
, that structure won't be compatible with lemmas like tmul_smul
unless
we use a ℤ-Module
instance provided by TensorProduct.left_module
.
When R
is a Ring
we get the required TensorProduct.compatible_smul
instance through
IsScalarTower
, 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
- ⋯ = ⋯
Equations
- ⋯ = ⋯