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

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

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)

noncomputable 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))

def TensorProduct.«term_⊗_» : Lean.TrailingParserDescr

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.

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

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.

noncomputable 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))

noncomputable 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

• TensorProduct.addZeroClass M N = let __src := AddCon.addMonoid (addConGen (TensorProduct.Eqv R M N)); AddZeroClass.mk ⋯ ⋯

noncomputable 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

• TensorProduct.addSemigroup M N = let __src := AddCon.addMonoid (addConGen (TensorProduct.Eqv R M N)); AddSemigroup.mk ⋯

noncomputable 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 ⋯

noncomputable 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 }

noncomputable 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))

def TensorProduct.«term_⊗ₜ_» : Lean.TrailingParserDescr

The canonical function M → N → M ⊗ N.

Equations

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

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

The canonical function M → N → M ⊗ N.

Equations

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

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

noncomputable def TensorProduct.liftAddHom {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] (f : M →+ N →+ P) (hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)) : TensorProduct R M N →+ P

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 = AddCon.lift (addConGen (TensorProduct.Eqv R M N)) (FreeAddMonoid.lift fun (mn : M × N) => (f mn.1) mn.2) ⋯

@[simp]

theorem TensorProduct.liftAddHom_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] (f : M →+ N →+ P) (hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)) (m : M) (n : N) : (TensorProduct.liftAddHom f hf) (m ⊗ₜ[R] n) = (f m) n

@[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

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

@[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

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₂

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

Equations

• TensorProduct.uniqueLeft = { toInhabited := { default := 0 }, uniq := ⋯ }

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

Equations

• TensorProduct.uniqueRight = { toInhabited := { default := 0 }, uniq := ⋯ }

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

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.

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

noncomputable 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

• ⋯ = ⋯

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 .

noncomputable 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_10} [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 : M × N) => (r • p.1) ⊗ₜ[R] p.2

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_10} [SMul R' M] (r : R') (m : M) (n : N) : (TensorProduct.SMul.aux r) (FreeAddMonoid.of (m, n)) = (r • m) ⊗ₜ[R] n

noncomputable 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

• TensorProduct.leftHasSMul = { smul := fun (r : R') => ⇑(AddCon.lift (addConGen (TensorProduct.Eqv R M N)) (TensorProduct.SMul.aux r) ⋯) }

noncomputable 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

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

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

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

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

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

noncomputable instance 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

• TensorProduct.addMonoid = let __src := TensorProduct.addZeroClass M N; AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (v : TensorProduct R M N) => n • v) ⋯ ⋯

noncomputable 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; AddCommMonoid.mk ⋯

noncomputable 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

• TensorProduct.leftDistribMulAction = let_fun this := ⋯; DistribMulAction.mk ⋯ ⋯

noncomputable instance TensorProduct.instDistribMulActionTensorProductToMonoidToMonoidWithZeroToSemiringAddMonoid {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.instDistribMulActionTensorProductToMonoidToMonoidWithZeroToSemiringAddMonoid = TensorProduct.leftDistribMulAction

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

@[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

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

noncomputable 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 ⋯ ⋯

noncomputable 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

noncomputable instance TensorProduct.instIsCentralScalarTensorProductLeftHasSMulToMonoidToMonoidWithZeroToDistribMulActionMulOppositeMonoidInstSemiringOp_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

• ⋯ = ⋯

noncomputable 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_10} [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

• ⋯ = ⋯

noncomputable 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_10} [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

• ⋯ = ⋯

noncomputable 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_10} [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

• ⋯ = ⋯

noncomputable 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

• ⋯ = ⋯

noncomputable 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

• TensorProduct.mk R M N = LinearMap.mk₂ R (fun (x : M) (x_1 : N) => x ⊗ₜ[R] x_1) ⋯ ⋯ ⋯ ⋯

@[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

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

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

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_10} (s : Finset α) (m : α → M) (n : N) : (Finset.sum s fun (a : α) => m a) ⊗ₜ[R] n = Finset.sum s fun (a : α) => m a ⊗ₜ[R] n

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_10} (s : Finset α) (n : α → N) : (m ⊗ₜ[R] Finset.sum s fun (a : α) => n a) = Finset.sum s fun (a : α) => m ⊗ₜ[R] n a

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 : TensorProduct R M N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t} = ⊤

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

@[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) ⊤ ⊤ = ⊤

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 : M) (n : N), m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n) : ∃ (m : M) (n : N), x = m ⊗ₜ[R] n

noncomputable 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

• TensorProduct.liftAux f = TensorProduct.liftAddHom (AddMonoidHom.comp LinearMap.toAddMonoidHom' (LinearMap.toAddMonoidHom f)) ⋯

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

@[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

noncomputable 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

• TensorProduct.lift f = let __src := TensorProduct.liftAux f; { toAddHom := { toFun := __src.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

@[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

@[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

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

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

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

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) = g ∘ₗ TensorProduct.lift f

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

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].

noncomputable 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)))

@[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

noncomputable 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.

@[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

@[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)

noncomputable 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))

@[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)

noncomputable 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

@[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)

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

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

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

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.

noncomputable 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

• TensorProduct.lid R M = LinearEquiv.ofLinear (TensorProduct.lift (LinearMap.lsmul R M)) ((TensorProduct.mk R R M) 1) ⋯ ⋯

@[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

@[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

noncomputable 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

• TensorProduct.comm R M N = LinearEquiv.ofLinear (TensorProduct.lift (LinearMap.flip (TensorProduct.mk R N M))) (TensorProduct.lift (LinearMap.flip (TensorProduct.mk R M N))) ⋯ ⋯

@[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

@[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

theorem TensorProduct.lift_comp_comm_eq (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.lift f ∘ₗ ↑(TensorProduct.comm R N M) = TensorProduct.lift (LinearMap.flip f)

noncomputable 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)

@[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

@[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

theorem TensorProduct.lid_eq_rid (R : Type u_1) [CommSemiring R] : TensorProduct.lid R R = TensorProduct.rid R R

noncomputable 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.

@[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

@[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

noncomputable 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)

@[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

theorem TensorProduct.map_comp_comm_eq {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.map f g ∘ₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R Q P) ∘ₗ TensorProduct.map g f

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.

theorem TensorProduct.map_comm {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) (x : TensorProduct R N M) : (TensorProduct.map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R Q P) ((TensorProduct.map g f) x)

theorem TensorProduct.map_map_comp_assoc_eq {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} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) : TensorProduct.map f (TensorProduct.map g h) ∘ₗ ↑(TensorProduct.assoc R M N P) = ↑(TensorProduct.assoc R Q S T) ∘ₗ TensorProduct.map (TensorProduct.map 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.

theorem TensorProduct.map_map_assoc {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} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R (TensorProduct R M N) P) : (TensorProduct.map f (TensorProduct.map g h)) ((TensorProduct.assoc R M N P) x) = (TensorProduct.assoc R Q S T) ((TensorProduct.map (TensorProduct.map f g) h) x)

theorem TensorProduct.map_map_comp_assoc_symm_eq {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} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) : TensorProduct.map (TensorProduct.map f g) h ∘ₗ ↑(LinearEquiv.symm (TensorProduct.assoc R M N P)) = ↑(LinearEquiv.symm (TensorProduct.assoc R Q S T)) ∘ₗ TensorProduct.map f (TensorProduct.map 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).

theorem TensorProduct.map_map_assoc_symm {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} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R M (TensorProduct R N P)) : (TensorProduct.map (TensorProduct.map f g) h) ((LinearEquiv.symm (TensorProduct.assoc R M N P)) x) = (LinearEquiv.symm (TensorProduct.assoc R Q S T)) ((TensorProduct.map f (TensorProduct.map g h)) x)

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 : TensorProduct R P Q | ∃ (m : M) (n : N), f m ⊗ₜ[R] g n = t}

noncomputable 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 ↥p ↥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)

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_10} {Q' : Type u_11} [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 (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = TensorProduct.map f₂ g₂ ∘ₗ TensorProduct.map f₁ g₁

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_11} [AddCommMonoid Q'] [Module R Q'] (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct.lift i ∘ₗ TensorProduct.map f g = TensorProduct.lift (LinearMap.compl₂ (i ∘ₗ f) g)

@[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

@[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

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₂

@[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)

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

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₂

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

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

noncomputable 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

• TensorProduct.mapBilinear R M N P Q = LinearMap.mk₂ R TensorProduct.map ⋯ ⋯ ⋯ ⋯

noncomputable 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))

noncomputable 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.

noncomputable 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)

noncomputable 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} {S : Type u_8} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) : TensorProduct R M N →ₗ[R] TensorProduct R P S →ₗ[R] TensorProduct R Q T

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 = LinearMap.comp (TensorProduct.homTensorHomMap R P S Q T) (TensorProduct.map f g)

@[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

@[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

@[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

@[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

@[simp]

theorem TensorProduct.map₂_apply_tmul {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} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) (m : M) (n : N) : (TensorProduct.map₂ f g) (m ⊗ₜ[R] n) = TensorProduct.map (f m) (g n)

@[simp]

theorem TensorProduct.map_zero_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] (g : N →ₗ[R] Q) : TensorProduct.map 0 g = 0

@[simp]

theorem TensorProduct.map_zero_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) : TensorProduct.map f 0 = 0

noncomputable 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

• TensorProduct.congr f g = LinearEquiv.ofLinear (TensorProduct.map ↑f ↑g) (TensorProduct.map ↑(LinearEquiv.symm f) ↑(LinearEquiv.symm g)) ⋯ ⋯

@[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

@[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

noncomputable 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.

@[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

@[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

noncomputable 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).

See also mul_mul_mul_comm.

Equations

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

@[simp]

theorem TensorProduct.tensorTensorTensorComm_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] (m : M) (n : N) (p : P) (q : Q) : (TensorProduct.tensorTensorTensorComm R M N P Q) ((m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q) = (m ⊗ₜ[R] p) ⊗ₜ[R] n ⊗ₜ[R] q

@[simp]

theorem TensorProduct.tensorTensorTensorComm_symm (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] : LinearEquiv.symm (TensorProduct.tensorTensorTensorComm R M N P Q) = TensorProduct.tensorTensorTensorComm R M P N Q

noncomputable def TensorProduct.tensorTensorTensorAssoc (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 (TensorProduct R N P)) Q

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 = LinearEquiv.trans (LinearEquiv.symm (TensorProduct.assoc R (TensorProduct R M N) P Q)) (TensorProduct.congr (TensorProduct.assoc R M N P) 1)

@[simp]

theorem TensorProduct.tensorTensorTensorAssoc_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] (m : M) (n : N) (p : P) (q : Q) : (TensorProduct.tensorTensorTensorAssoc R M N P Q) ((m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q) = (m ⊗ₜ[R] n ⊗ₜ[R] p) ⊗ₜ[R] q

@[simp]

theorem TensorProduct.tensorTensorTensorAssoc_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] (m : M) (n : N) (p : P) (q : Q) : (LinearEquiv.symm (TensorProduct.tensorTensorTensorAssoc R M N P Q)) ((m ⊗ₜ[R] n ⊗ₜ[R] p) ⊗ₜ[R] q) = (m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q

noncomputable def LinearMap.lTensor {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 : N →ₗ[R] P) : TensorProduct R M N →ₗ[R] TensorProduct R M P

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

noncomputable def LinearMap.rTensor {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 : N →ₗ[R] P) : TensorProduct R N M →ₗ[R] TensorProduct R P M

rTensor f M : N₁ ⊗ M →ₗ N₂ ⊗ M is the natural linear map induced by f : N₁ →ₗ N₂.

Equations

• LinearMap.rTensor M f = TensorProduct.map f LinearMap.id

@[simp]

theorem LinearMap.lTensor_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 : N →ₗ[R] P) (m : M) (n : N) : (LinearMap.lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n

@[simp]

theorem LinearMap.rTensor_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 : N →ₗ[R] P) (m : M) (n : N) : (LinearMap.rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m

@[simp]

theorem LinearMap.lTensor_comp_mk {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 : N →ₗ[R] P) (m : M) : LinearMap.lTensor M f ∘ₗ (TensorProduct.mk R M N) m = (TensorProduct.mk R M P) m ∘ₗ f

@[simp]

theorem LinearMap.rTensor_comp_flip_mk {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 : N →ₗ[R] P) (m : M) : LinearMap.rTensor M f ∘ₗ (LinearMap.flip (TensorProduct.mk R N M)) m = (LinearMap.flip (TensorProduct.mk R P M)) m ∘ₗ f

theorem LinearMap.comm_comp_rTensor_comp_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] P) : ↑(TensorProduct.comm R P Q) ∘ₗ LinearMap.rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N) = LinearMap.lTensor Q g

theorem LinearMap.comm_comp_lTensor_comp_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] P) : ↑(TensorProduct.comm R Q P) ∘ₗ LinearMap.lTensor Q g ∘ₗ ↑(TensorProduct.comm R N Q) = LinearMap.rTensor Q g

noncomputable def LinearMap.lTensorHom {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] : (N →ₗ[R] P) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M P

lTensorHom M is the natural linear map that sends a linear map f : N →ₗ P to M ⊗ f.

Equations

• LinearMap.lTensorHom M = { toAddHom := { toFun := LinearMap.lTensor M, map_add' := ⋯ }, map_smul' := ⋯ }

noncomputable def LinearMap.rTensorHom {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] : (N →ₗ[R] P) →ₗ[R] TensorProduct R N M →ₗ[R] TensorProduct R P M

rTensorHom M is the natural linear map that sends a linear map f : N →ₗ P to M ⊗ f.

Equations

• LinearMap.rTensorHom M = { toAddHom := { toFun := fun (f : N →ₗ[R] P) => LinearMap.rTensor M f, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem LinearMap.coe_lTensorHom {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] : ⇑(LinearMap.lTensorHom M) = LinearMap.lTensor M

@[simp]

theorem LinearMap.coe_rTensorHom {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] : ⇑(LinearMap.rTensorHom M) = LinearMap.rTensor M

@[simp]

theorem LinearMap.lTensor_add {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 : N →ₗ[R] P) (g : N →ₗ[R] P) : LinearMap.lTensor M (f + g) = LinearMap.lTensor M f + LinearMap.lTensor M g

@[simp]

theorem LinearMap.rTensor_add {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 : N →ₗ[R] P) (g : N →ₗ[R] P) : LinearMap.rTensor M (f + g) = LinearMap.rTensor M f + LinearMap.rTensor M g

@[simp]

theorem LinearMap.lTensor_zero {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] : LinearMap.lTensor M 0 = 0

@[simp]

theorem LinearMap.rTensor_zero {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] : LinearMap.rTensor M 0 = 0

@[simp]

theorem LinearMap.lTensor_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] (r : R) (f : N →ₗ[R] P) : LinearMap.lTensor M (r • f) = r • LinearMap.lTensor M f

@[simp]

theorem LinearMap.rTensor_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] (r : R) (f : N →ₗ[R] P) : LinearMap.rTensor M (r • f) = r • LinearMap.rTensor M f

theorem LinearMap.lTensor_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] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : LinearMap.lTensor M (g ∘ₗ f) = LinearMap.lTensor M g ∘ₗ LinearMap.lTensor M f

theorem LinearMap.lTensor_comp_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] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R M N) : (LinearMap.lTensor M (g ∘ₗ f)) x = (LinearMap.lTensor M g) ((LinearMap.lTensor M f) x)

theorem LinearMap.rTensor_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] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : LinearMap.rTensor M (g ∘ₗ f) = LinearMap.rTensor M g ∘ₗ LinearMap.rTensor M f

theorem LinearMap.rTensor_comp_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] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R N M) : (LinearMap.rTensor M (g ∘ₗ f)) x = (LinearMap.rTensor M g) ((LinearMap.rTensor M f) x)

theorem LinearMap.lTensor_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 : Module.End R N) (g : Module.End R N) : LinearMap.lTensor M (f * g) = LinearMap.lTensor M f * LinearMap.lTensor M g

theorem LinearMap.rTensor_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 : Module.End R N) (g : Module.End R N) : LinearMap.rTensor M (f * g) = LinearMap.rTensor M f * LinearMap.rTensor M g

@[simp]

theorem LinearMap.lTensor_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] : LinearMap.lTensor M LinearMap.id = LinearMap.id

theorem LinearMap.lTensor_id_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] (x : TensorProduct R M N) : (LinearMap.lTensor M LinearMap.id) x = x

@[simp]

theorem LinearMap.rTensor_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] : LinearMap.rTensor M LinearMap.id = LinearMap.id

theorem LinearMap.rTensor_id_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] (x : TensorProduct R N M) : (LinearMap.rTensor M LinearMap.id) x = x

theorem LinearMap.lid_comp_rTensor {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 : N →ₗ[R] R) : ↑(TensorProduct.lid R M) ∘ₗ LinearMap.rTensor M f = TensorProduct.lift (LinearMap.lsmul R M ∘ₗ f)

@[simp]

theorem LinearMap.lTensor_comp_rTensor {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.lTensor P g ∘ₗ LinearMap.rTensor N f = TensorProduct.map f g

@[simp]

theorem LinearMap.rTensor_comp_lTensor {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.rTensor Q f ∘ₗ LinearMap.lTensor M g = TensorProduct.map f g

@[simp]

theorem LinearMap.map_comp_rTensor {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] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) : TensorProduct.map f g ∘ₗ LinearMap.rTensor N f' = TensorProduct.map (f ∘ₗ f') g

@[simp]

theorem LinearMap.map_comp_lTensor {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] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) : TensorProduct.map f g ∘ₗ LinearMap.lTensor M g' = TensorProduct.map f (g ∘ₗ g')

@[simp]

theorem LinearMap.rTensor_comp_map {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] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.rTensor Q f' ∘ₗ TensorProduct.map f g = TensorProduct.map (f' ∘ₗ f) g

@[simp]

theorem LinearMap.lTensor_comp_map {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' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.lTensor P g' ∘ₗ TensorProduct.map f g = TensorProduct.map f (g' ∘ₗ g)

@[simp]

theorem LinearMap.rTensor_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) (n : ℕ) : LinearMap.rTensor N f ^ n = LinearMap.rTensor N (f ^ n)

@[simp]

theorem LinearMap.lTensor_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 : N →ₗ[R] N) (n : ℕ) : LinearMap.lTensor M f ^ n = LinearMap.lTensor M (f ^ n)

noncomputable def TensorProduct.Neg.aux (R : Type u_1) [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] : TensorProduct R M N →ₗ[R] TensorProduct R M N

Auxiliary function to defining negation multiplication on tensor product.

Equations

• TensorProduct.Neg.aux R = TensorProduct.lift (LinearMap.comp (TensorProduct.mk R M N) (-LinearMap.id))

noncomputable instance TensorProduct.neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] : Neg (TensorProduct R M N)

Equations

• TensorProduct.neg = { neg := ⇑(TensorProduct.Neg.aux R) }

theorem TensorProduct.add_left_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (x : TensorProduct R M N) : -x + x = 0

noncomputable instance TensorProduct.addCommGroup {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] : AddCommGroup (TensorProduct R M N)

Equations

• TensorProduct.addCommGroup = let __src := TensorProduct.addCommMonoid; AddCommGroup.mk ⋯

theorem TensorProduct.neg_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m : M) (n : N) : (-m) ⊗ₜ[R] n = -m ⊗ₜ[R] n

theorem TensorProduct.tmul_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m : M) (n : N) : m ⊗ₜ[R] (-n) = -m ⊗ₜ[R] n

theorem TensorProduct.tmul_sub {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m : M) (n₁ : N) (n₂ : N) : m ⊗ₜ[R] (n₁ - n₂) = m ⊗ₜ[R] n₁ - m ⊗ₜ[R] n₂

theorem TensorProduct.sub_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m₁ : M) (m₂ : M) (n : N) : (m₁ - m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n

noncomputable instance TensorProduct.CompatibleSMul.int {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] : TensorProduct.CompatibleSMul R ℤ M N

While the tensor product will automatically inherit a ℤ-module structure from AddCommGroup.intModule, 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

• ⋯ = ⋯

noncomputable instance TensorProduct.CompatibleSMul.unit {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {S : Type u_7} [Monoid S] [DistribMulAction S M] [DistribMulAction S N] [TensorProduct.CompatibleSMul R S M N] : TensorProduct.CompatibleSMul R Sˣ M N

Equations

• ⋯ = ⋯

@[simp]

theorem LinearMap.lTensor_sub {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (g : N →ₗ[R] P) : LinearMap.lTensor M (f - g) = LinearMap.lTensor M f - LinearMap.lTensor M g

@[simp]

theorem LinearMap.rTensor_sub {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (g : N →ₗ[R] P) : LinearMap.rTensor M (f - g) = LinearMap.rTensor M f - LinearMap.rTensor M g

@[simp]

theorem LinearMap.lTensor_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : LinearMap.lTensor M (-f) = -LinearMap.lTensor M f

@[simp]

theorem LinearMap.rTensor_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : LinearMap.rTensor M (-f) = -LinearMap.rTensor M f