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 M → N → TensorProduct R M N.

Given any bilinear map M → N → P, there is a unique linear map TensorProduct R M N → P whose composition with the canonical bilinear map M → N → TensorProduct 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 TensorProduct R M N, as well as m ⊗ₜ n and m ⊗ₜ[R] n for TensorProduct.tmul R m n.

Tags #

bilinear, tensor, tensor product

source

inductive TensorProduct.Eqv (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

FreeAddMonoid (M × N) → FreeAddMonoid (M × N) → Prop

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)

The relation on FreeAddMonoid (M × N) that generates a congruence whose quotient is the tensor product.

Instances For

source

def TensorProduct (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid 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 scoped TensorProduct.

Equations

TensorProduct R M N = AddCon.Quotient (addConGen (TensorProduct.Eqv R M N))

Instances For

source

def TensorProduct.«term_⊗_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def TensorProduct.«term_⊗[_]_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def TensorProduct.addMonoid {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

AddMonoid (TensorProduct R M N)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance TensorProduct.add {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

Add (TensorProduct R M N)

Equations

TensorProduct.add M N = AddCon.hasAdd (addConGen (TensorProduct.Eqv R M N))

source

instance TensorProduct.addZeroClass {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

AddZeroClass (TensorProduct R M N)

Equations

One or more equations did not get rendered due to their size.

source

instance TensorProduct.addSemigroup {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

AddSemigroup (TensorProduct R M N)

Equations

One or more equations did not get rendered due to their size.

source

instance TensorProduct.addCommSemigroup {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

AddCommSemigroup (TensorProduct R M N)

Equations

TensorProduct.addCommSemigroup M N = let src := AddCon.addMonoid (addConGen (TensorProduct.Eqv R M N)); AddCommSemigroup.mk (_ : ∀ (x y : TensorProduct R M N), x + y = y + x)

source

instance TensorProduct.instInhabitedTensorProduct {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

Inhabited (TensorProduct R M N)

Equations

TensorProduct.instInhabitedTensorProduct M N = { default := 0 }

source

def TensorProduct.tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :

TensorProduct R M N

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 = ↑(AddCon.mk' (addConGen (TensorProduct.Eqv R M N))) (FreeAddMonoid.of (m, n))

Instances For

source

def TensorProduct.«term_⊗ₜ_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def TensorProduct.«term_⊗ₜ[_]_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem TensorProduct.induction_on {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {motive : TensorProduct R M N → Prop} (z : TensorProduct R M N) (zero : motive 0) (tmul : (x : M) → (y : N) → motive (x ⊗ₜ[R] y)) (add : (x y : TensorProduct R M N) → motive x → motive y → motive (x + y)) :

motive z

source

@[simp]

theorem TensorProduct.zero_tmul {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (n : N) :

0 ⊗ₜ[R] n = 0

source

theorem TensorProduct.add_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m₁ : M) (m₂ : M) (n : N) :

(m₁ + m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n + m₂ ⊗ₜ[R] n

source

@[simp]

theorem TensorProduct.tmul_zero {R : Type u_1} [CommSemiring R] {M : Type u_4} (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) :

m ⊗ₜ[R] 0 = 0

source

theorem TensorProduct.tmul_add {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n₁ : N) (n₂ : N) :

m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂

source

class TensorProduct.CompatibleSMul (R : Type u_1) [CommSemiring R] (R' : Type u_2) [Monoid R'] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [DistribMulAction R' N] :

Prop

smul_tmul : ∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)

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.intModule, 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

source

instance TensorProduct.CompatibleSMul.isScalarTower {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMul R' R] [IsScalarTower R' R M] [DistribMulAction R' N] [IsScalarTower R' R N] :

TensorProduct.CompatibleSMul R R' M N

Note that this provides the default compatible_smul R R M N instance through IsScalarTower.left.

Equations

@TensorProduct.CompatibleSMul.isScalarTower = @TensorProduct.CompatibleSMul.isScalarTower.proof_1

source

theorem TensorProduct.smul_tmul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [DistribMulAction R' N] [TensorProduct.CompatibleSMul R R' M N] (r : R') (m : M) (n : N) :

(r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)

smul can be moved from one side of the product to the other .

source

def TensorProduct.SMul.aux {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_9} [SMul R' M] (r : R') :

FreeAddMonoid (M × N) →+ TensorProduct R M N

Auxiliary function to defining scalar multiplication on tensor product.

Equations

TensorProduct.SMul.aux r = ↑FreeAddMonoid.lift fun p => (r • p.fst) ⊗ₜ[R] p.snd

Instances For

source

theorem TensorProduct.SMul.aux_of {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_9} [SMul R' M] (r : R') (m : M) (n : N) :

↑(TensorProduct.SMul.aux r) (FreeAddMonoid.of (m, n)) = (r • m) ⊗ₜ[R] n

source

instance TensorProduct.leftHasSMul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] :

SMul R' (TensorProduct 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

One or more equations did not get rendered due to their size.

source

instance TensorProduct.instSMulTensorProduct {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

SMul R (TensorProduct R M N)

Equations

TensorProduct.instSMulTensorProduct = TensorProduct.leftHasSMul

source

theorem TensorProduct.smul_zero {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (r : R') :

r • 0 = 0

source

theorem TensorProduct.smul_add {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (r : R') (x : TensorProduct R M N) (y : TensorProduct R M N) :

r • (x + y) = r • x + r • y

source

theorem TensorProduct.zero_smul {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module R'' M] [SMulCommClass R R'' M] (x : TensorProduct R M N) :

0 • x = 0

source

theorem TensorProduct.one_smul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (x : TensorProduct R M N) :

1 • x = x

source

theorem TensorProduct.add_smul {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module R'' M] [SMulCommClass R R'' M] (r : R'') (s : R'') (x : TensorProduct R M N) :

(r + s) • x = r • x + s • x

source

instance TensorProduct.addCommMonoid {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

AddCommMonoid (TensorProduct R M N)

Equations

TensorProduct.addCommMonoid = let src := TensorProduct.addCommSemigroup M N; let src := TensorProduct.addZeroClass M N; AddCommMonoid.mk (_ : ∀ (a b : TensorProduct R M N), a + b = b + a)

source

instance TensorProduct.leftDistribMulAction {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] :

DistribMulAction R' (TensorProduct R M N)

Equations

One or more equations did not get rendered due to their size.

source

instance TensorProduct.instDistribMulActionTensorProductToMonoidToMonoidWithZeroToSemiringToAddMonoidAddCommMonoid {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

DistribMulAction R (TensorProduct R M N)

Equations

TensorProduct.instDistribMulActionTensorProductToMonoidToMonoidWithZeroToSemiringToAddMonoidAddCommMonoid = TensorProduct.leftDistribMulAction

source

theorem TensorProduct.smul_tmul' {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (r : R') (m : M) (n : N) :

r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n

source

@[simp]

theorem TensorProduct.tmul_smul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] [DistribMulAction R' N] [TensorProduct.CompatibleSMul R R' M N] (r : R') (x : M) (y : N) :

x ⊗ₜ[R] (r • y) = r • x ⊗ₜ[R] y

source

theorem TensorProduct.smul_tmul_smul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) (s : R) (m : M) (n : N) :

(r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n

source

instance TensorProduct.leftModule {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module R'' M] [SMulCommClass R R'' M] :

Module R'' (TensorProduct R M N)

Equations

TensorProduct.leftModule = Module.mk (_ : ∀ (r s : R'') (x : TensorProduct R M N), (r + s) • x = r • x + s • x) (_ : ∀ (x : TensorProduct R M N), 0 • x = 0)

source

instance TensorProduct.instModuleTensorProductToSemiringAddCommMonoid {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

Module R (TensorProduct R M N)

Equations

TensorProduct.instModuleTensorProductToSemiringAddCommMonoid = TensorProduct.leftModule

source

instance TensorProduct.instIsCentralScalarTensorProductLeftHasSMulToMonoidToMonoidWithZeroToDistribMulActionMulOppositeMonoidSemiringOp_rightToSMulToZeroToAddMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZeroToSMulToSMulZeroClassToZeroToSMulWithZeroToMulActionWithZeroToSMulZeroClassToAddZeroClassToDistribSMul {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module R'' M] [SMulCommClass R R'' M] [Module R''ᵐᵒᵖ M] [IsCentralScalar R'' M] :

IsCentralScalar R'' (TensorProduct R M N)

Equations

One or more equations did not get rendered due to their size.

source

instance TensorProduct.smulCommClass_left {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] {R'₂ : Type u_9} [Monoid R'₂] [DistribMulAction R'₂ M] [SMulCommClass R R'₂ M] [SMulCommClass R' R'₂ M] :

SMulCommClass R' R'₂ (TensorProduct R M N)

SMulCommClass R' R'₂ M implies SMulCommClass R' R'₂ (M ⊗[R] N)

Equations

@TensorProduct.smulCommClass_left = @TensorProduct.smulCommClass_left.proof_1

source

instance TensorProduct.isScalarTower_left {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] {R'₂ : Type u_9} [Monoid R'₂] [DistribMulAction R'₂ M] [SMulCommClass R R'₂ M] [SMul R'₂ R'] [IsScalarTower R'₂ R' M] :

IsScalarTower R'₂ R' (TensorProduct R M N)

IsScalarTower R'₂ R' M implies IsScalarTower R'₂ R' (M ⊗[R] N)

Equations

@TensorProduct.isScalarTower_left = @TensorProduct.isScalarTower_left.proof_1

source

instance TensorProduct.isScalarTower_right {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] {R'₂ : Type u_9} [Monoid R'₂] [DistribMulAction R'₂ M] [SMulCommClass R R'₂ M] [SMul R'₂ R'] [DistribMulAction R'₂ N] [DistribMulAction R' N] [TensorProduct.CompatibleSMul R R'₂ M N] [TensorProduct.CompatibleSMul R R' M N] [IsScalarTower R'₂ R' N] :

IsScalarTower R'₂ R' (TensorProduct R M N)

IsScalarTower R'₂ R' N implies IsScalarTower R'₂ R' (M ⊗[R] N)

Equations

@TensorProduct.isScalarTower_right = @TensorProduct.isScalarTower_right.proof_1

source

instance TensorProduct.isScalarTower {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] [SMul R' R] [IsScalarTower R' R M] :

IsScalarTower R' R (TensorProduct R M N)

A short-cut instance for the common case, where the requirements for the compatible_smul instances are sufficient.

Equations

@TensorProduct.isScalarTower = @TensorProduct.isScalarTower.proof_1

source

def TensorProduct.mk (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

M →ₗ[R] N →ₗ[R] TensorProduct R M N

The canonical bilinear map M → N → M ⊗[R] N.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TensorProduct.mk_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :

↑(↑(TensorProduct.mk R M N) m) n = m ⊗ₜ[R] n

source

theorem TensorProduct.ite_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] :

(if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ[R] x₂ else 0

source

theorem TensorProduct.tmul_ite {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] :

(x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ[R] x₂ else 0

source

theorem TensorProduct.sum_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {α : Type u_9} (s : Finset α) (m : α → M) (n : N) :

(Finset.sum s fun a => m a) ⊗ₜ[R] n = Finset.sum s fun a => m a ⊗ₜ[R] n

source

theorem TensorProduct.tmul_sum {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) {α : Type u_9} (s : Finset α) (n : α → N) :

(m ⊗ₜ[R] Finset.sum s fun a => n a) = Finset.sum s fun a => m ⊗ₜ[R] n a

source

theorem TensorProduct.span_tmul_eq_top (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} = ⊤

The simple (aka pure) elements span the tensor product.

source

@[simp]

theorem TensorProduct.map₂_mk_top_top_eq_top (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

Submodule.map₂ (TensorProduct.mk R M N) ⊤ ⊤ = ⊤

source

theorem TensorProduct.exists_eq_tmul_of_forall (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) (h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n) :

∃ m n, x = m ⊗ₜ[R] n

source

def TensorProduct.liftAux {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) :

TensorProduct R M N →+ 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

One or more equations did not get rendered due to their size.

Instances For

source

theorem TensorProduct.liftAux_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :

↑(TensorProduct.liftAux f) (m ⊗ₜ[R] n) = ↑(↑f m) n

source

@[simp]

theorem TensorProduct.liftAux.smul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (r : R) (x : TensorProduct R M N) :

↑(TensorProduct.liftAux f) (r • x) = r • ↑(TensorProduct.liftAux f) x

source

def TensorProduct.lift {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) :

TensorProduct R M 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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TensorProduct.lift.tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :

↑(TensorProduct.lift f) (x ⊗ₜ[R] y) = ↑(↑f x) y

source

@[simp]

theorem TensorProduct.lift.tmul' {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :

↑(TensorProduct.lift f).toAddHom (x ⊗ₜ[R] y) = ↑(↑f x) y

source

theorem TensorProduct.ext' {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g : TensorProduct R M N →ₗ[R] P} {h : TensorProduct R M N →ₗ[R] P} (H : ∀ (x : M) (y : N), ↑g (x ⊗ₜ[R] y) = ↑h (x ⊗ₜ[R] y)) :

g = h

source

theorem TensorProduct.lift.unique {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} {g : TensorProduct R M N →ₗ[R] P} (H : ∀ (x : M) (y : N), ↑g (x ⊗ₜ[R] y) = ↑(↑f x) y) :

g = TensorProduct.lift f

source

theorem TensorProduct.lift_mk {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

TensorProduct.lift (TensorProduct.mk R M N) = LinearMap.id

source

theorem TensorProduct.lift_compr₂ {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {f : M →ₗ[R] N →ₗ[R] P} (g : P →ₗ[R] Q) :

TensorProduct.lift (LinearMap.compr₂ f g) = LinearMap.comp g (TensorProduct.lift f)

source

theorem TensorProduct.lift_mk_compr₂ {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) :

TensorProduct.lift (LinearMap.compr₂ (TensorProduct.mk R M N) f) = f

source

theorem TensorProduct.ext {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g : TensorProduct R M N →ₗ[R] P} {h : TensorProduct R M N →ₗ[R] P} (H : LinearMap.compr₂ (TensorProduct.mk R M N) g = LinearMap.compr₂ (TensorProduct.mk R M N) 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 TensorProduct.ext' allows ext to apply lemmas specific to M →ₗ _ and N →ₗ _.

See note [partially-applied ext lemmas].

source

def TensorProduct.uncurry (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

(M →ₗ[R] N →ₗ[R] P) →ₗ[R] TensorProduct R M N →ₗ[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

TensorProduct.uncurry R M N P = LinearMap.flip (TensorProduct.lift (LinearMap.comp LinearMap.lflip (LinearMap.flip LinearMap.id)))

Instances For

source

@[simp]

theorem TensorProduct.uncurry_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :

↑(↑(TensorProduct.uncurry R M N P) f) (m ⊗ₜ[R] n) = ↑(↑f m) n

source

def TensorProduct.lift.equiv (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

(M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] TensorProduct R M N →ₗ[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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TensorProduct.lift.equiv_apply (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :

↑(↑(TensorProduct.lift.equiv R M N P) f) (m ⊗ₜ[R] n) = ↑(↑f m) n

source

@[simp]

theorem TensorProduct.lift.equiv_symm_apply (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) :

↑(↑(↑(LinearEquiv.symm (TensorProduct.lift.equiv R M N P)) f) m) n = ↑f (m ⊗ₜ[R] n)

source

def TensorProduct.lcurry (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

(TensorProduct R M N →ₗ[R] P) →ₗ[R] M →ₗ[R] 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

TensorProduct.lcurry R M N P = ↑(LinearEquiv.symm (TensorProduct.lift.equiv R M N P))

Instances For

source

@[simp]

theorem TensorProduct.lcurry_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) :

↑(↑(↑(TensorProduct.lcurry R M N P) f) m) n = ↑f (m ⊗ₜ[R] n)

source

def TensorProduct.curry {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) :

M →ₗ[R] 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

TensorProduct.curry f = ↑(TensorProduct.lcurry R M N P) f

Instances For

source

@[simp]

theorem TensorProduct.curry_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) :

↑(↑(TensorProduct.curry f) m) n = ↑f (m ⊗ₜ[R] n)

source

theorem TensorProduct.curry_injective {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

Function.Injective TensorProduct.curry

source

theorem TensorProduct.ext_threefold {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {g : TensorProduct R (TensorProduct R M N) P →ₗ[R] Q} {h : TensorProduct R (TensorProduct R 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

source

theorem TensorProduct.ext_fourfold {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] {g : TensorProduct R (TensorProduct R (TensorProduct R M N) P) Q →ₗ[R] S} {h : TensorProduct R (TensorProduct R (TensorProduct R 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

source

theorem TensorProduct.ext_fourfold' {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] {φ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₗ[R] S} {ψ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₗ[R] S} (H : ∀ (w : M) (x : N) (y : P) (z : Q), ↑φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ↑ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)) :

φ = ψ

Two linear maps (M ⊗ N) ⊗ (P ⊗ Q) → S which agree on all elements of the form (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) are equal.

source

def TensorProduct.lid (R : Type u_1) [CommSemiring R] (M : Type u_4) [AddCommMonoid M] [Module R M] :

TensorProduct R R M ≃ₗ[R] M

The base ring is a left identity for the tensor product of modules, up to linear equivalence.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TensorProduct.lid_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] (m : M) (r : R) :

↑(TensorProduct.lid R M) (r ⊗ₜ[R] m) = r • m

source

@[simp]

theorem TensorProduct.lid_symm_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] (m : M) :

↑(LinearEquiv.symm (TensorProduct.lid R M)) m = 1 ⊗ₜ[R] m

source

def TensorProduct.comm (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

TensorProduct R M N ≃ₗ[R] TensorProduct R N M

The tensor product of modules is commutative, up to linear equivalence.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TensorProduct.comm_tmul (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :

↑(TensorProduct.comm R M N) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m

source

@[simp]

theorem TensorProduct.comm_symm_tmul (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :

↑(LinearEquiv.symm (TensorProduct.comm R M N)) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n

source

def TensorProduct.rid (R : Type u_1) [CommSemiring R] (M : Type u_4) [AddCommMonoid M] [Module R M] :

TensorProduct R M R ≃ₗ[R] M

The base ring is a right identity for the tensor product of modules, up to linear equivalence.

Equations

TensorProduct.rid R M = LinearEquiv.trans (TensorProduct.comm R M R) (TensorProduct.lid R M)

Instances For

source

@[simp]

theorem TensorProduct.rid_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] (m : M) (r : R) :

↑(TensorProduct.rid R M) (m ⊗ₜ[R] r) = r • m

source

@[simp]

theorem TensorProduct.rid_symm_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] (m : M) :

↑(LinearEquiv.symm (TensorProduct.rid R M)) m = m ⊗ₜ[R] 1

source

def TensorProduct.assoc (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

TensorProduct R (TensorProduct R M N) P ≃ₗ[R] TensorProduct R M (TensorProduct R N P)

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

source

@[simp]

theorem TensorProduct.assoc_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) :

↑(TensorProduct.assoc R M N P) ((m ⊗ₜ[R] n) ⊗ₜ[R] p) = m ⊗ₜ[R] n ⊗ₜ[R] p

source

@[simp]

theorem TensorProduct.assoc_symm_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) :

↑(LinearEquiv.symm (TensorProduct.assoc R M N P)) (m ⊗ₜ[R] n ⊗ₜ[R] p) = (m ⊗ₜ[R] n) ⊗ₜ[R] p

source

def TensorProduct.map {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

TensorProduct R M N →ₗ[R] TensorProduct R P Q

The tensor product of a pair of linear maps between modules.

Equations

TensorProduct.map f g = TensorProduct.lift (LinearMap.comp (LinearMap.compl₂ (TensorProduct.mk R P Q) g) f)

Instances For

source

@[simp]

theorem TensorProduct.map_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid 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) :

↑(TensorProduct.map f g) (m ⊗ₜ[R] n) = ↑f m ⊗ₜ[R] ↑g n

source

theorem TensorProduct.map_range_eq_span_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

LinearMap.range (TensorProduct.map f g) = Submodule.span R {t | ∃ m n, ↑f m ⊗ₜ[R] ↑g n = t}

source

def TensorProduct.mapIncl {R : Type u_1} [CommSemiring R] {P : Type u_6} {Q : Type u_7} [AddCommMonoid P] [AddCommMonoid Q] [Module R P] [Module R Q] (p : Submodule R P) (q : Submodule R Q) :

TensorProduct R { x // x ∈ p } { x // x ∈ q } →ₗ[R] TensorProduct R P Q

Given submodules p ⊆ P and q ⊆ Q, this is the natural map: p ⊗ q → P ⊗ Q.

Equations

TensorProduct.mapIncl p q = TensorProduct.map (Submodule.subtype p) (Submodule.subtype q)

Instances For

source

theorem TensorProduct.map_comp {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {P' : Type u_9} {Q' : Type u_10} [AddCommMonoid P'] [Module R P'] [AddCommMonoid Q'] [Module R Q'] (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :

TensorProduct.map (LinearMap.comp f₂ f₁) (LinearMap.comp g₂ g₁) = LinearMap.comp (TensorProduct.map f₂ g₂) (TensorProduct.map f₁ g₁)

source

theorem TensorProduct.lift_comp_map {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {Q' : Type u_10} [AddCommMonoid Q'] [Module R Q'] (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

LinearMap.comp (TensorProduct.lift i) (TensorProduct.map f g) = TensorProduct.lift (LinearMap.compl₂ (LinearMap.comp i f) g)

source

@[simp]

theorem TensorProduct.map_id {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

TensorProduct.map LinearMap.id LinearMap.id = LinearMap.id

source

@[simp]

theorem TensorProduct.map_one {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

TensorProduct.map 1 1 = 1

source

theorem TensorProduct.map_mul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f₁ : M →ₗ[R] M) (f₂ : M →ₗ[R] M) (g₁ : N →ₗ[R] N) (g₂ : N →ₗ[R] N) :

TensorProduct.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.map f₁ g₁ * TensorProduct.map f₂ g₂

source

@[simp]

theorem TensorProduct.map_pow {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ) :

TensorProduct.map f g ^ n = TensorProduct.map (f ^ n) (g ^ n)

source

theorem TensorProduct.map_add_left {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f₁ : M →ₗ[R] P) (f₂ : M →ₗ[R] P) (g : N →ₗ[R] Q) :

TensorProduct.map (f₁ + f₂) g = TensorProduct.map f₁ g + TensorProduct.map f₂ g

source

theorem TensorProduct.map_add_right {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g₁ : N →ₗ[R] Q) (g₂ : N →ₗ[R] Q) :

TensorProduct.map f (g₁ + g₂) = TensorProduct.map f g₁ + TensorProduct.map f g₂

source

theorem TensorProduct.map_smul_left {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

TensorProduct.map (r • f) g = r • TensorProduct.map f g

source

theorem TensorProduct.map_smul_right {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

TensorProduct.map f (r • g) = r • TensorProduct.map f g

source

def TensorProduct.mapBilinear (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] :

(M →ₗ[R] P) →ₗ[R] (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R P Q

The tensor product of a pair of linear maps between modules, bilinear in both maps.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def TensorProduct.lTensorHomToHomLTensor (R : Type u_1) [CommSemiring R] (M : Type u_4) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] :

TensorProduct R P (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] TensorProduct R P Q

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.comp (LinearMap.llcomp R M Q (TensorProduct R P Q)) (TensorProduct.mk R P Q))

Instances For

source

def TensorProduct.rTensorHomToHomRTensor (R : Type u_1) [CommSemiring R] (M : Type u_4) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] :

TensorProduct R (M →ₗ[R] P) Q →ₗ[R] M →ₗ[R] TensorProduct R P Q

The canonical linear map from (M →ₗ[R] P) ⊗[R] Q to (M →ₗ[R] P ⊗[R] Q)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def TensorProduct.homTensorHomMap (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] :

TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R P Q

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

source

@[simp]

theorem TensorProduct.mapBilinear_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

↑(↑(TensorProduct.mapBilinear R M N P Q) f) g = TensorProduct.map f g

source

@[simp]

theorem TensorProduct.lTensorHomToHomLTensor_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] (p : P) (f : M →ₗ[R] Q) (m : M) :

↑(↑(TensorProduct.lTensorHomToHomLTensor R M P Q) (p ⊗ₜ[R] f)) m = p ⊗ₜ[R] ↑f m

source

@[simp]

theorem TensorProduct.rTensorHomToHomRTensor_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] (f : M →ₗ[R] P) (q : Q) (m : M) :

↑(↑(TensorProduct.rTensorHomToHomRTensor R M P Q) (f ⊗ₜ[R] q)) m = ↑f m ⊗ₜ[R] q

source

@[simp]

theorem TensorProduct.homTensorHomMap_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :

↑(TensorProduct.homTensorHomMap R M N P Q) (f ⊗ₜ[R] g) = TensorProduct.map f g

source

def TensorProduct.congr {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :

TensorProduct R M N ≃ₗ[R] TensorProduct R 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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TensorProduct.congr_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid 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) :

↑(TensorProduct.congr f g) (m ⊗ₜ[R] n) = ↑f m ⊗ₜ[R] ↑g n

source

@[simp]

theorem TensorProduct.congr_symm_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid 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) :

↑(LinearEquiv.symm (TensorProduct.congr f g)) (p ⊗ₜ[R] q) = ↑(LinearEquiv.symm f) p ⊗ₜ[R] ↑(LinearEquiv.symm g) q

source

def TensorProduct.leftComm (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

TensorProduct R M (TensorProduct R N P) ≃ₗ[R] TensorProduct R N (TensorProduct R M P)

A tensor product analogue of mul_left_comm.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TensorProduct.leftComm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) :

↑(TensorProduct.leftComm R M N P) (m ⊗ₜ[R] n ⊗ₜ[R] p) = n ⊗ₜ[R] m ⊗ₜ[R] p

source

@[simp]

theorem TensorProduct.leftComm_symm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) :

↑(LinearEquiv.symm (TensorProduct.leftComm R M N P)) (n ⊗ₜ[R] m ⊗ₜ[R] p) = m ⊗ₜ[R] n ⊗ₜ[R] p

source

def TensorProduct.tensorTensorTensorComm (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] :

TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) ≃ₗ[R] TensorProduct R (TensorProduct R M P) (TensorProduct R N 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 TensorProduct.semiring instance (currently defined "by hand" using TensorProduct.mul).