Tensor product of modules over commutative semirings.

This file constructs the tensor product of modules over commutative semirings. Given a semiring R and modules over it M and N, the standard construction of the tensor product is TensorProduct R M N. It is also a module over R.

It comes with a canonical bilinear map TensorProduct.mk R M N : M →ₗ[R] N →ₗ[R] TensorProduct R M N.

Given any bilinear map f : M →ₗ[R] N →ₗ[R] P, there is a unique linear map TensorProduct.lift f : TensorProduct R M N →ₗ[R] P whose composition with the canonical bilinear map TensorProduct.mk is the given bilinear map f. Uniqueness is shown in the theorem TensorProduct.lift.unique.

Notation

• This file introduces the notation M ⊗ N and M ⊗[R] N for the tensor product space TensorProduct R M N.
• It introduces the notation m ⊗ₜ n and m ⊗ₜ[R] n for the tensor product of two elements, otherwise written as TensorProduct.tmul R m n.

Tags

bilinear, tensor, tensor product

inductive TensorProduct.Eqv (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) [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} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (n : N) : Eqv R M N (FreeAddMonoid.of (0, n)) 0
• of_zero_right {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) : Eqv R M N (FreeAddMonoid.of (m, 0)) 0
• of_add_left {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m₁ m₂ : M) (n : N) : Eqv R M N (FreeAddMonoid.of (m₁, n) + FreeAddMonoid.of (m₂, n)) (FreeAddMonoid.of (m₁ + m₂, n))
• of_add_right {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n₁ n₂ : N) : Eqv R M N (FreeAddMonoid.of (m, n₁) + FreeAddMonoid.of (m, n₂)) (FreeAddMonoid.of (m, n₁ + n₂))
• of_smul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) (m : M) (n : N) : Eqv R M N (FreeAddMonoid.of (r • m, n)) (FreeAddMonoid.of (m, r • n))
• add_comm {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x y : FreeAddMonoid (M × N)) : Eqv R M N (x + y) (y + x)

def TensorProduct (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_5 u_6)

The tensor product of two modules M and N over the same commutative semiring R. The localized notations are M ⊗ N and M ⊗[R] N, accessed by open scoped TensorProduct.

Equations

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

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

• TensorProduct.«term_⊗_» = Lean.ParserDescr.trailingNode `TensorProduct.«term_⊗_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 101))

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.

instance TensorProduct.zero {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : Zero (TensorProduct R M N)

Equations

• TensorProduct.zero M N = (addConGen (TensorProduct.Eqv R M N)).zero

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

Equations

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

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

Equations

• TensorProduct.addZeroClass M N = { toZero := TensorProduct.zero M N, toAdd := TensorProduct.add M N, zero_add := ⋯, add_zero := ⋯ }

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

Equations

• TensorProduct.addSemigroup M N = { toAdd := TensorProduct.add M N, add_assoc := ⋯ }

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

Equations

• TensorProduct.addCommSemigroup M N = { toAddSemigroup := TensorProduct.addSemigroup M N, add_comm := ⋯ }

instance TensorProduct.instInhabited {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : Inhabited (TensorProduct R M N)

Equations

• TensorProduct.instInhabited M N = { default := 0 }

def TensorProduct.tmul (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} [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 = (addConGen (TensorProduct.Eqv R M N)).mk' (FreeAddMonoid.of (m, n))

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

The canonical function M → N → M ⊗ N.

Equations

• TensorProduct.«term_⊗ₜ_» = Lean.ParserDescr.trailingNode `TensorProduct.«term_⊗ₜ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₜ ") (Lean.ParserDescr.cat `term 101))

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.

unsafe instance TensorProduct.instRepr {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Repr M] [Repr N] : Repr (TensorProduct R M N)

Produces an arbitrary representation of the form 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_5} {N : Type u_6} [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

def TensorProduct.liftAddHom {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [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 = (addConGen (TensorProduct.Eqv R M N)).lift (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_5} {N : Type u_6} {P : Type u_7} [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) : (liftAddHom f hf) (m ⊗ₜ[R] n) = (f m) n

@[simp]

theorem TensorProduct.zero_tmul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [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_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (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_5} (N : Type u_6) [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_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n₁ n₂ : N) : m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂

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

Equations

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

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

Equations

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

class TensorProduct.CompatibleSMul (R : Type u_1) [CommSemiring R] (R' : Type u_2) [Monoid R'] (M : Type u_5) (N : Type u_6) [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.toIntModule, allowing z • to be moved even if R does not support negation.

Note that Module R' (M ⊗[R] N) is available even without this typeclass on R'; it's only needed if TensorProduct.smul_tmul, TensorProduct.smul_tmul', or TensorProduct.tmul_smul is used.

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

@[instance 100]

instance TensorProduct.CompatibleSMul.isScalarTower {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [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] : CompatibleSMul R R' M N

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

theorem TensorProduct.smul_tmul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [DistribMulAction R' N] [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 .

def TensorProduct.SMul.aux {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_18} [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_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_18} [SMul R' M] (r : R') (m : M) (n : N) : (aux r) (FreeAddMonoid.of (m, n)) = (r • m) ⊗ₜ[R] n

instance TensorProduct.leftHasSMul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [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') => ⇑((addConGen (TensorProduct.Eqv R M N)).lift (TensorProduct.SMul.aux r) ⋯) }

instance TensorProduct.instSMul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : SMul R (TensorProduct R M N)

Equations

• TensorProduct.instSMul = TensorProduct.leftHasSMul

theorem TensorProduct.smul_zero {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [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_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (r : R') (x 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_5} {N : Type u_6} [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_5} {N : Type u_6} [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_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module R'' M] [SMulCommClass R R'' M] (r s : R'') (x : TensorProduct R M N) : (r + s) • x = r • x + s • x

instance TensorProduct.addMonoid {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [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.

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

Equations

• TensorProduct.addCommMonoid = { toAddMonoid := TensorProduct.addMonoid, add_comm := ⋯ }

theorem IsAddUnit.tmul_left (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : N} (hn : IsAddUnit n) (m : M) : IsAddUnit (m ⊗ₜ[R] n)

theorem IsAddUnit.tmul_right (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {m : M} (hm : IsAddUnit m) (n : N) : IsAddUnit (m ⊗ₜ[R] n)

instance TensorProduct.leftDistribMulAction {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [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 = { toSMul := TensorProduct.leftHasSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

instance TensorProduct.instDistribMulAction {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : DistribMulAction R (TensorProduct R M N)

Equations

• TensorProduct.instDistribMulAction = TensorProduct.leftDistribMulAction

theorem TensorProduct.smul_tmul' {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [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_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] [DistribMulAction R' N] [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_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r s : R) (m : M) (n : N) : (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n

theorem TensorProduct.tmul_eq_smul_one_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] {S : Type u_18} [Semiring S] [Module R S] [SMulCommClass R S S] (s : S) (m : M) : s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

@[deprecated TensorProduct.tmul_eq_smul_one_tmul (since := "2025-07-08")]

theorem TensorProduct.tsmul_eq_smul_one_tuml {R : Type u_1} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] {S : Type u_18} [Semiring S] [Module R S] [SMulCommClass R S S] (s : S) (m : M) : s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

Alias of TensorProduct.tmul_eq_smul_one_tmul.

instance TensorProduct.leftModule {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_5} {N : Type u_6} [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 = { toDistribMulAction := TensorProduct.leftDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

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

Equations

• TensorProduct.instModule = TensorProduct.leftModule

instance TensorProduct.instIsCentralScalar {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_5} {N : Type u_6} [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)

instance TensorProduct.smulCommClass_left {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] {R'₂ : Type u_18} [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)

instance TensorProduct.isScalarTower_left {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] {R'₂ : Type u_18} [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)

instance TensorProduct.isScalarTower_right {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] {R'₂ : Type u_18} [Monoid R'₂] [DistribMulAction R'₂ M] [SMulCommClass R R'₂ M] [SMul R'₂ R'] [DistribMulAction R'₂ N] [DistribMulAction R' N] [CompatibleSMul R R'₂ M N] [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)

instance TensorProduct.isScalarTower {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_5} {N : Type u_6} [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.

def TensorProduct.mk (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) [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 (x1 : M) (x2 : N) => x1 ⊗ₜ[R] x2) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TensorProduct.mk_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) : ((mk R M N) m) n = m ⊗ₜ[R] n

theorem TensorProduct.ite_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [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_5} {N : Type u_6} [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.tmul_single {R : Type u_1} [CommSemiring R] {N : Type u_6} [AddCommMonoid N] [Module R N] {ι : Type u_18} [DecidableEq ι] {M : ι → Type u_19} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (x : N) (m : M i) (j : ι) : x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

theorem TensorProduct.single_tmul {R : Type u_1} [CommSemiring R] {N : Type u_6} [AddCommMonoid N] [Module R N] {ι : Type u_18} [DecidableEq ι] {M : ι → Type u_19} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (x : N) (m : M i) (j : ι) : Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

theorem TensorProduct.sum_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {α : Type u_18} (s : Finset α) (m : α → M) (n : N) : (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n

theorem TensorProduct.tmul_sum {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) {α : Type u_18} (s : Finset α) (n : α → N) : m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a

theorem TensorProduct.span_tmul_eq_top (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) [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_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤

theorem TensorProduct.exists_eq_tmul_of_forall (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) [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

def TensorProduct.liftAux {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {P₂ : Type u_17} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid P₂] [Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] 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 (LinearMap.toAddMonoidHom'.comp f'.toAddMonoidHom) ⋯

theorem TensorProduct.liftAux_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {P₂ : Type u_17} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid P₂] [Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) : (liftAux f') (m ⊗ₜ[R] n) = (f' m) n

@[simp]

theorem TensorProduct.liftAux.smulₛₗ {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {P₂ : Type u_17} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid P₂] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (r : R) (x : TensorProduct R M N) : (liftAux f') (r • x) = σ₁₂ r • (liftAux f') x

theorem TensorProduct.liftAux.smul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [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) : (liftAux f) (r • x) = r • (liftAux f) x

def TensorProduct.lift {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {P₂ : Type u_17} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid P₂] [Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) : TensorProduct R M N →ₛₗ[σ₁₂] 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.

This works for semilinear maps.

Equations

• TensorProduct.lift f' = { toFun := (↑(TensorProduct.liftAux f')).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TensorProduct.lift.tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {P₂ : Type u_17} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid P₂] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (x : M) (y : N) : (lift f') (x ⊗ₜ[R] y) = (f' x) y

@[simp]

theorem TensorProduct.lift.tmul' {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {P₂ : Type u_17} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid P₂] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (x : M) (y : N) : (lift f').toAddHom (x ⊗ₜ[R] y) = (f' x) y

theorem TensorProduct.ext' {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {P₂ : Type u_17} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid P₂] [Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] 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_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {P₂ : Type u_17} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid P₂] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} {g : TensorProduct R M N →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f' x) y) : g = lift f'

theorem TensorProduct.lift_mk {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : lift (mk R M N) = LinearMap.id

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

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

theorem TensorProduct.ext {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g h : TensorProduct R M N →ₗ[R] P} (H : (mk R M N).compr₂ g = (mk R M N).compr₂ 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].

theorem TensorProduct.ext_iff {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g h : TensorProduct R M N →ₗ[R] P} : g = h ↔ (mk R M N).compr₂ g = (mk R M N).compr₂ h

def TensorProduct.uncurry (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [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 = { toFun := TensorProduct.lift, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TensorProduct.uncurry_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [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) : ((uncurry R M N P) f) (m ⊗ₜ[R] n) = (f m) n

def TensorProduct.lift.equiv (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [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_5) (N : Type u_6) (P : Type u_7) [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) : ((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_5) (N : Type u_6) (P : Type u_7) [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) : (((equiv R M N P).symm f) m) n = f (m ⊗ₜ[R] n)

def TensorProduct.lcurry (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [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 = ↑(TensorProduct.lift.equiv R M N P).symm

@[simp]

theorem TensorProduct.lcurry_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [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) : (((lcurry R M N P) f) m) n = f (m ⊗ₜ[R] n)

def TensorProduct.curry {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [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_5} {N : Type u_6} {P : Type u_7} [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) : ((curry f) m) n = f (m ⊗ₜ[R] n)

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

theorem TensorProduct.ext_threefold {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] {g 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_threefold' {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] {g h : TensorProduct R M (TensorProduct R 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_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] {g 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_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] {φ ψ : 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.

def TensorProduct.comm (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) [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 (TensorProduct.mk R N M).flip) (TensorProduct.lift (TensorProduct.mk R M N).flip) ⋯ ⋯

@[simp]

theorem TensorProduct.comm_tmul (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) [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_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) : (TensorProduct.comm R M N).symm (n ⊗ₜ[R] m) = m ⊗ₜ[R] n

theorem TensorProduct.lift_comp_comm_eq (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) : lift f ∘ₗ ↑(TensorProduct.comm R N M) = lift f.flip

def TensorProduct.mapOfCompatibleSMul (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] : TensorProduct A M N →ₗ[A] TensorProduct R M N

If M and N are both R- and A-modules and their actions on them commute, and if the A-action on M ⊗[R] N can switch between the two factors, then there is a canonical A-linear map from M ⊗[A] N to M ⊗[R] N.

Equations

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

@[simp]

theorem TensorProduct.mapOfCompatibleSMul_tmul (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] (m : M) (n : N) : (mapOfCompatibleSMul R A M N) (m ⊗ₜ[A] n) = m ⊗ₜ[R] n

theorem TensorProduct.mapOfCompatibleSMul_surjective (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] : Function.Surjective ⇑(mapOfCompatibleSMul R A M N)

def TensorProduct.mapOfCompatibleSMul' (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] : TensorProduct A M N →ₗ[R] TensorProduct R M N

mapOfCompatibleSMul R A M N is also R-linear.

Equations

• TensorProduct.mapOfCompatibleSMul' R A M N = { toAddHom := (TensorProduct.mapOfCompatibleSMul R A M N).toAddHom, map_smul' := ⋯ }

def TensorProduct.equivOfCompatibleSMul (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] [CompatibleSMul A R M N] : TensorProduct A M N ≃ₗ[A] TensorProduct R M N

If the R- and A-actions on M and N satisfy CompatibleSMul both ways, then M ⊗[A] N is canonically isomorphic to M ⊗[R] N.

Equations

• TensorProduct.equivOfCompatibleSMul R A M N = { toLinearMap := TensorProduct.mapOfCompatibleSMul R A M N, invFun := ⇑(TensorProduct.mapOfCompatibleSMul A R M N), left_inv := ⋯, right_inv := ⋯ }

def TensorProduct.map {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {M₂ : Type u_13} {N₂ : Type u_15} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

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

Equations

• TensorProduct.map f g = TensorProduct.lift ((TensorProduct.mk R₂ M₂ N₂).compl₂ g ∘ₛₗ f)

@[simp]

theorem TensorProduct.map_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {M₂ : Type u_13} {N₂ : Type u_15} [CommSemiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (m : M) (n : N) : (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_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map f g ∘ₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R Q P) ∘ₗ 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_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R N M) : (map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R Q P) ((map g f) x)

theorem TensorProduct.range_map {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.range (map f g) = Submodule.map₂ (mk R P Q) (LinearMap.range f) (LinearMap.range g)

theorem TensorProduct.range_map_eq_span_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.range (map f g) = Submodule.span R {t : TensorProduct R P Q | ∃ (m : M) (n : N), f m ⊗ₜ[R] g n = t}

@[deprecated TensorProduct.range_map_eq_span_tmul (since := "2025-09-07")]

theorem TensorProduct.map_range_eq_span_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.range (map f g) = Submodule.span R {t : TensorProduct R P Q | ∃ (m : M) (n : N), f m ⊗ₜ[R] g n = t}

Alias of TensorProduct.range_map_eq_span_tmul.

def TensorProduct.mapIncl {R : Type u_1} [CommSemiring R] {P : Type u_7} {Q : Type u_8} [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] (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 p.subtype q.subtype

theorem TensorProduct.range_mapIncl {R : Type u_1} [CommSemiring R] {P : Type u_7} {Q : Type u_8} [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] (p : Submodule R P) (q : Submodule R Q) : LinearMap.range (mapIncl p q) = Submodule.map₂ (mk R P Q) p q

theorem TensorProduct.map₂_eq_range_lift_comp_mapIncl {R : Type u_1} [CommSemiring R] {M : Type u_5} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] (f : P →ₗ[R] Q →ₗ[R] M) (p : Submodule R P) (q : Submodule R Q) : Submodule.map₂ f p q = LinearMap.range (lift f ∘ₗ mapIncl p q)

theorem TensorProduct.map_comp {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {R₃ : Type u_12} {M₂ : Type u_13} {M₃ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R₂ M₂] [Module R₃ M₃] [Module R₂ N₂] [Module R₃ N₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) : map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) = map f₂ g₂ ∘ₛₗ map f₁ g₁

theorem TensorProduct.map_map {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R₂ : Type u_11} {R₃ : Type u_12} {M₂ : Type u_13} {M₃ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R₂ M₂] [Module R₃ M₃] [Module R₂ N₂] [Module R₃ N₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R M N) : (map f₂ g₂) ((map f₁ g₁) x) = (map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁)) x

theorem TensorProduct.range_map_mono {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₂ : Type u_13} {M₃ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R M₂] [Module R M₃] [Module R N₂] [Module R N₃] {a : M →ₗ[R] M₂} {b : M₃ →ₗ[R] M₂} {c : N →ₗ[R] N₂} {d : N₃ →ₗ[R] N₂} (hab : LinearMap.range a ≤ LinearMap.range b) (hcd : LinearMap.range c ≤ LinearMap.range d) : LinearMap.range (map a c) ≤ LinearMap.range (map b d)

theorem TensorProduct.range_mapIncl_mono {R : Type u_1} [CommSemiring R] {P : Type u_7} {Q : Type u_8} [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] {p p' : Submodule R P} {q q' : Submodule R Q} (hp : p ≤ p') (hq : q ≤ q') : LinearMap.range (mapIncl p q) ≤ LinearMap.range (mapIncl p' q')

theorem TensorProduct.lift_comp_map {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] {Q' : Type u_19} [AddCommMonoid Q'] [Module R Q'] (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : lift i ∘ₗ map f g = lift ((i ∘ₗ f).compl₂ g)

@[simp]

theorem TensorProduct.map_id {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : map LinearMap.id LinearMap.id = LinearMap.id

@[simp]

theorem TensorProduct.map_one {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : map 1 1 = 1

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

@[simp]

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

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

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

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

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

def TensorProduct.mapBilinear (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] : (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 ⋯ ⋯ ⋯ ⋯

def TensorProduct.lTensorHomToHomLTensor (R : Type u_1) [CommSemiring R] (M : Type u_5) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] : 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.llcomp R M Q (TensorProduct R P Q) ∘ₗ TensorProduct.mk R P Q)

def TensorProduct.rTensorHomToHomRTensor (R : Type u_1) [CommSemiring R] (M : Type u_5) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] : 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

• TensorProduct.rTensorHomToHomRTensor R M P Q = TensorProduct.lift (LinearMap.llcomp R M P (TensorProduct R P Q) ∘ₗ (TensorProduct.mk R P Q).flip).flip

def TensorProduct.homTensorHomMap (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] : 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)

def TensorProduct.map₂ {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (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 = 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_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : ((mapBilinear R M N P Q) f) g = map f g

@[simp]

theorem TensorProduct.lTensorHomToHomLTensor_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] (p : P) (f : M →ₗ[R] Q) (m : M) : ((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_5} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] (f : M →ₗ[R] P) (q : Q) (m : M) : ((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_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (homTensorHomMap R M N P Q) (f ⊗ₜ[R] g) = map f g

@[simp]

theorem TensorProduct.map₂_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) (m : M) (n : N) : (map₂ f g) (m ⊗ₜ[R] n) = map (f m) (g n)

@[simp]

theorem TensorProduct.map_zero_left {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : N →ₗ[R] Q) : map 0 g = 0

@[simp]

theorem TensorProduct.map_zero_right {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) : map f 0 = 0

def TensorProduct.congr {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (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 ↑f.symm ↑g.symm) ⋯ ⋯

@[simp]

theorem TensorProduct.toLinearMap_congr {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : ↑(congr f g) = map ↑f ↑g

@[simp]

theorem TensorProduct.congr_tmul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) : (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_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) : (congr f g).symm (p ⊗ₜ[R] q) = f.symm p ⊗ₜ[R] g.symm q

theorem TensorProduct.congr_symm {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : (congr f g).symm = congr f.symm g.symm

@[simp]

theorem TensorProduct.congr_refl_refl {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : congr (LinearEquiv.refl R M) (LinearEquiv.refl R N) = LinearEquiv.refl R (TensorProduct R M N)

theorem TensorProduct.congr_trans {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : P ≃ₗ[R] S) (g' : Q ≃ₗ[R] T) : congr (f ≪≫ₗ f') (g ≪≫ₗ g') = congr f g ≪≫ₗ congr f' g'

theorem TensorProduct.congr_mul {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (f' : M ≃ₗ[R] M) (g' : N ≃ₗ[R] N) : congr (f * f') (g * g') = congr f g * congr f' g'

@[simp]

theorem TensorProduct.congr_pow {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℕ) : congr f g ^ n = congr (f ^ n) (g ^ n)

@[simp]

theorem TensorProduct.congr_zpow {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℤ) : congr f g ^ n = congr (f ^ n) (g ^ n)

theorem TensorProduct.map_bijective {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] {f : M →ₗ[R] N} {g : P →ₗ[R] Q} (hf : Function.Bijective ⇑f) (hg : Function.Bijective ⇑g) : Function.Bijective ⇑(map f g)

def LinearMap.lTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [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

LinearMap.lTensor M f : M ⊗ N →ₗ M ⊗ P is the natural linear map induced by f : N →ₗ P.

Equations

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

def LinearMap.rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [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

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

Equations

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

theorem LinearMap.lTensor_def {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : lTensor M f = TensorProduct.map id f

theorem LinearMap.rTensor_def {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : rTensor M f = TensorProduct.map f id

@[simp]

theorem LinearMap.lTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) (n : N) : (lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n

@[simp]

theorem LinearMap.rTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) (n : N) : (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_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) : 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_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) : rTensor M f ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f

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

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

theorem LinearMap.lTensor_inj_iff_rTensor_inj {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Injective ⇑(lTensor M f) ↔ Function.Injective ⇑(rTensor M f)

Given a linear map f : N → P, f ⊗ M is injective if and only if M ⊗ f is injective.

theorem LinearMap.lTensor_surj_iff_rTensor_surj {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Surjective ⇑(lTensor M f) ↔ Function.Surjective ⇑(rTensor M f)

Given a linear map f : N → P, f ⊗ M is surjective if and only if M ⊗ f is surjective.

theorem LinearMap.lTensor_bij_iff_rTensor_bij {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Bijective ⇑(lTensor M f) ↔ Function.Bijective ⇑(rTensor M f)

Given a linear map f : N → P, f ⊗ M is bijective if and only if M ⊗ f is bijective.

theorem LinearMap.smul_lTensor {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) {S : Type u_18} [CommSemiring S] [SMul R S] [Module S M] [IsScalarTower R S M] [SMulCommClass R S M] (s : S) (m : TensorProduct R M N) : s • (lTensor M f) m = (lTensor M f) (s • m)

def LinearMap.lTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [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.

See also Module.End.lTensorAlgHom.

Equations

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

def LinearMap.rTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [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 f ⊗ M.

See also Module.End.rTensorAlgHom.

Equations

• LinearMap.rTensorHom M = { 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_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : ⇑(lTensorHom M) = lTensor M

@[simp]

theorem LinearMap.coe_rTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : ⇑(rTensorHom M) = rTensor M

@[simp]

theorem LinearMap.lTensor_add {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : lTensor M (f + g) = lTensor M f + lTensor M g

@[simp]

theorem LinearMap.rTensor_add {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : rTensor M (f + g) = rTensor M f + rTensor M g

@[simp]

theorem LinearMap.lTensor_zero {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : lTensor M 0 = 0

@[simp]

theorem LinearMap.rTensor_zero {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : rTensor M 0 = 0

@[simp]

theorem LinearMap.lTensor_smul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (r : R) (f : N →ₗ[R] P) : lTensor M (r • f) = r • lTensor M f

@[simp]

theorem LinearMap.rTensor_smul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (r : R) (f : N →ₗ[R] P) : rTensor M (r • f) = r • rTensor M f

theorem LinearMap.lTensor_comp {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : lTensor M (g ∘ₗ f) = lTensor M g ∘ₗ lTensor M f

theorem LinearMap.lTensor_comp_apply {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R M N) : (lTensor M (g ∘ₗ f)) x = (lTensor M g) ((lTensor M f) x)

theorem LinearMap.rTensor_comp {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : rTensor M (g ∘ₗ f) = rTensor M g ∘ₗ rTensor M f

theorem LinearMap.rTensor_comp_apply {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R N M) : (rTensor M (g ∘ₗ f)) x = (rTensor M g) ((rTensor M f) x)

theorem LinearMap.lTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : Module.End R N) : lTensor M (f * g) = lTensor M f * lTensor M g

theorem LinearMap.rTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : Module.End R N) : rTensor M (f * g) = rTensor M f * rTensor M g

@[simp]

theorem LinearMap.lTensor_id {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : lTensor M id = id

theorem LinearMap.lTensor_id_apply {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : (lTensor M id) x = x

@[simp]

theorem LinearMap.rTensor_id {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : rTensor M id = id

theorem LinearMap.rTensor_id_apply {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R N M) : (rTensor M id) x = x

@[simp]

theorem LinearMap.lTensor_smul_action {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) : lTensor M (DistribMulAction.toLinearMap R N r) = DistribMulAction.toLinearMap R (TensorProduct R M N) r

@[simp]

theorem LinearMap.rTensor_smul_action {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) : rTensor M (DistribMulAction.toLinearMap R N r) = DistribMulAction.toLinearMap R (TensorProduct R N M) r

@[simp]

theorem LinearMap.lTensor_comp_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : lTensor P g ∘ₗ rTensor N f = TensorProduct.map f g

@[simp]

theorem LinearMap.rTensor_comp_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : rTensor Q f ∘ₗ lTensor M g = TensorProduct.map f g

@[simp]

theorem LinearMap.map_comp_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) : TensorProduct.map f g ∘ₗ rTensor N f' = TensorProduct.map (f ∘ₗ f') g

@[simp]

theorem LinearMap.map_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) (x : TensorProduct R S N) : (TensorProduct.map f g) ((rTensor N f') x) = (TensorProduct.map (f ∘ₗ f') g) x

@[simp]

theorem LinearMap.map_comp_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) : TensorProduct.map f g ∘ₗ lTensor M g' = TensorProduct.map f (g ∘ₗ g')

@[simp]

theorem LinearMap.map_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) (x : TensorProduct R M S) : (TensorProduct.map f g) ((lTensor M g') x) = (TensorProduct.map f (g ∘ₗ g')) x

@[simp]

theorem LinearMap.rTensor_comp_map {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : rTensor Q f' ∘ₗ TensorProduct.map f g = TensorProduct.map (f' ∘ₗ f) g

@[simp]

theorem LinearMap.rTensor_map {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R M N) : (rTensor Q f') ((TensorProduct.map f g) x) = (TensorProduct.map (f' ∘ₗ f) g) x

@[simp]

theorem LinearMap.lTensor_comp_map {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : lTensor P g' ∘ₗ TensorProduct.map f g = TensorProduct.map f (g' ∘ₗ g)

@[simp]

theorem LinearMap.lTensor_map {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R M N) : (lTensor P g') ((TensorProduct.map f g) x) = (TensorProduct.map f (g' ∘ₗ g)) x

@[simp]

theorem LinearMap.rTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] M) (n : ℕ) : rTensor N f ^ n = rTensor N (f ^ n)

@[simp]

theorem LinearMap.lTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N →ₗ[R] N) (n : ℕ) : lTensor M f ^ n = lTensor M (f ^ n)

def LinearEquiv.lTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [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

LinearEquiv.lTensor M f : M ⊗ N ≃ₗ M ⊗ P is the natural linear equivalence induced by f : N ≃ₗ P.

Equations

• LinearEquiv.lTensor M f = TensorProduct.congr (LinearEquiv.refl R M) f

def LinearEquiv.rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [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

LinearEquiv.rTensor M f : N₁ ⊗ M ≃ₗ N₂ ⊗ M is the natural linear equivalence induced by f : N₁ ≃ₗ N₂.

Equations

• LinearEquiv.rTensor M f = TensorProduct.congr f (LinearEquiv.refl R M)

@[simp]

theorem LinearEquiv.coe_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(lTensor M f) = LinearMap.lTensor M ↑f

@[simp]

theorem LinearEquiv.coe_lTensor_symm {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(lTensor M f).symm = LinearMap.lTensor M ↑f.symm

@[simp]

theorem LinearEquiv.coe_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(rTensor M f) = LinearMap.rTensor M ↑f

@[simp]

theorem LinearEquiv.coe_rTensor_symm {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(rTensor M f).symm = LinearMap.rTensor M ↑f.symm

@[simp]

theorem LinearEquiv.lTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) (m : M) (n : N) : (lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n

@[simp]

theorem LinearEquiv.lTensor_symm_tmul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) (m : M) (p : P) : (lTensor M f).symm (m ⊗ₜ[R] p) = m ⊗ₜ[R] f.symm p

@[simp]

theorem LinearEquiv.rTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) (m : M) (n : N) : (rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m

@[simp]

theorem LinearEquiv.rTensor_symm_tmul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) (m : M) (p : P) : (rTensor M f).symm (p ⊗ₜ[R] m) = f.symm p ⊗ₜ[R] m

theorem LinearEquiv.comm_trans_rTensor_trans_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R Q] [Module R P] (g : N ≃ₗ[R] P) : TensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = lTensor Q g

theorem LinearEquiv.comm_trans_lTensor_trans_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R Q] [Module R P] (g : N ≃ₗ[R] P) : TensorProduct.comm R N Q ≪≫ₗ lTensor Q g ≪≫ₗ TensorProduct.comm R Q P = rTensor Q g

theorem LinearEquiv.lTensor_trans {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) : lTensor M (f ≪≫ₗ g) = lTensor M f ≪≫ₗ lTensor M g

theorem LinearEquiv.lTensor_trans_apply {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (x : TensorProduct R M N) : (lTensor M (f ≪≫ₗ g)) x = (lTensor M g) ((lTensor M f) x)

theorem LinearEquiv.rTensor_trans {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) : rTensor M (f ≪≫ₗ g) = rTensor M f ≪≫ₗ rTensor M g

theorem LinearEquiv.rTensor_trans_apply {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (y : TensorProduct R N M) : (rTensor M (f ≪≫ₗ g)) y = (rTensor M g) ((rTensor M f) y)

theorem LinearEquiv.lTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : N ≃ₗ[R] N) : lTensor M (f * g) = lTensor M f * lTensor M g

theorem LinearEquiv.rTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : N ≃ₗ[R] N) : rTensor M (f * g) = rTensor M f * rTensor M g

@[simp]

theorem LinearEquiv.lTensor_refl {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : lTensor M (refl R N) = refl R (TensorProduct R M N)

theorem LinearEquiv.lTensor_refl_apply {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : (lTensor M (refl R N)) x = x

@[simp]

theorem LinearEquiv.rTensor_refl {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : rTensor M (refl R N) = refl R (TensorProduct R N M)

theorem LinearEquiv.rTensor_refl_apply {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (y : TensorProduct R N M) : (rTensor M (refl R N)) y = y

@[simp]

theorem LinearEquiv.rTensor_trans_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : rTensor N f ≪≫ₗ lTensor P g = TensorProduct.congr f g

@[simp]

theorem LinearEquiv.lTensor_trans_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : lTensor M g ≪≫ₗ rTensor Q f = TensorProduct.congr f g

@[simp]

theorem LinearEquiv.rTensor_trans_congr {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : S ≃ₗ[R] M) : rTensor N f' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr (f' ≪≫ₗ f) g

@[simp]

theorem LinearEquiv.lTensor_trans_congr {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (g' : S ≃ₗ[R] N) : lTensor M g' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g)

@[simp]

theorem LinearEquiv.congr_trans_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f' : P ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : TensorProduct.congr f g ≪≫ₗ rTensor Q f' = TensorProduct.congr (f ≪≫ₗ f') g

@[simp]

theorem LinearEquiv.congr_trans_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (g' : Q ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : TensorProduct.congr f g ≪≫ₗ lTensor P g' = TensorProduct.congr f (g ≪≫ₗ g')

@[simp]

theorem LinearEquiv.rTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (n : ℕ) : rTensor N f ^ n = rTensor N (f ^ n)

@[simp]

theorem LinearEquiv.rTensor_zpow {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (n : ℤ) : rTensor N f ^ n = rTensor N (f ^ n)

@[simp]

theorem LinearEquiv.lTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N ≃ₗ[R] N) (n : ℕ) : lTensor M f ^ n = lTensor M (f ^ n)

@[simp]

theorem LinearEquiv.lTensor_zpow {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N ≃ₗ[R] N) (n : ℤ) : lTensor M f ^ n = lTensor M (f ^ n)

def TensorProduct.Neg.aux (R : Type u_1) [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid 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 (TensorProduct.mk R M N ∘ₗ (-LinearMap.id))

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

Equations

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

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

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

Equations

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

theorem TensorProduct.neg_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid 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} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (m : M) (p : P) : m ⊗ₜ[R] (-p) = -m ⊗ₜ[R] p

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

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

instance TensorProduct.CompatibleSMul.int {R : Type u_1} [CommSemiring R] {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] : CompatibleSMul R ℤ M P

While the tensor product will automatically inherit a ℤ-module structure from AddCommGroup.toIntModule, that structure won't be compatible with lemmas like tmul_smul unless we use a ℤ-Module instance provided by TensorProduct.left_module.

When R is a Ring we get the required TensorProduct.compatible_smul instance through IsScalarTower, but when it is only a Semiring we need to build it from scratch. The instance diamond in compatible_smul doesn't matter because it's in Prop.

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

@[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] [AddCommMonoid N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : lTensor M (f - g) = lTensor M f - lTensor M g

@[simp]

theorem LinearMap.rTensor_sub {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [AddCommMonoid N] [AddCommGroup P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (f g : N →ₗ[R] P) : rTensor Q (f - g) = rTensor Q f - rTensor Q 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] [AddCommMonoid N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : lTensor M (-f) = -lTensor M f

@[simp]

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