mathlib3documentation

linear_algebra.tensor_product

Tensor product of modules over commutative semirings. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 `tensor_product R M N`. It is also a module over `R`.

It comes with a canonical bilinear map `M → N → tensor_product R M N`.

Given any bilinear map `M → N → P`, there is a unique linear map `tensor_product R M N → P` whose composition with the canonical bilinear map `M → N → tensor_product R M N` is the given bilinear map `M → N → P`.

We start by proving basic lemmas about bilinear maps.

Notations #

This file uses the localized notation `M ⊗ N` and `M ⊗[R] N` for `tensor_product R M N`, as well as `m ⊗ₜ n` and `m ⊗ₜ[R] n` for `tensor_product.tmul R m n`.

Tags #

bilinear, tensor, tensor product

inductive tensor_product.eqv (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] :

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

def tensor_product (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ 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_locale tensor_product`.

Equations
Instances for `tensor_product`
@[protected, instance]
def tensor_product.add_zero_class {R : Type u_1} (M : Type u_4) (N : Type u_5) [ M] [ N] :
Equations
@[protected, instance]
def tensor_product.add_comm_semigroup {R : Type u_1} (M : Type u_4) (N : Type u_5) [ M] [ N] :
Equations
@[protected, instance]
def tensor_product.inhabited {R : Type u_1} (M : Type u_4) (N : Type u_5) [ M] [ N] :
Equations
def tensor_product.tmul (R : Type u_1) {M : Type u_4} {N : Type u_5} [ M] [ N] (m : M) (n : N) :
N

The canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`, accessed by `open_locale tensor_product`.

Equations
@[protected]
theorem tensor_product.induction_on {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] {C : N Prop} (z : N) (C0 : C 0) (C1 : {x : M} {y : N}, C (x ⊗ₜ[R] y)) (Cp : {x y : N}, C x C y C (x + y)) :
C z
@[simp]
theorem tensor_product.zero_tmul {R : Type u_1} (M : Type u_4) {N : Type u_5} [ M] [ N] (n : N) :
0 ⊗ₜ[R] n = 0
theorem tensor_product.add_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (m₁ m₂ : M) (n : N) :
(m₁ + m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n + m₂ ⊗ₜ[R] n
@[simp]
theorem tensor_product.tmul_zero {R : Type u_1} {M : Type u_4} (N : Type u_5) [ M] [ N] (m : M) :
m ⊗ₜ[R] 0 = 0
theorem tensor_product.tmul_add {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (m : M) (n₁ n₂ : N) :
m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂
@[class]
structure tensor_product.compatible_smul (R : Type u_1) (R' : Type u_2) [monoid R'] (M : Type u_4) (N : Type u_5) [ M] [ N] [ M] [ N] :

A typeclass for `has_smul` structures which can be moved across a tensor product.

This typeclass is generated automatically from a `is_scalar_tower` instance, but exists so that we can also add an instance for `add_comm_group.int_module`, allowing `z •` to be moved even if `R` does not support negation.

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

Instances of this typeclass
Instances of other typeclasses for `tensor_product.compatible_smul`
• tensor_product.compatible_smul.has_sizeof_inst
@[protected, instance]
def tensor_product.compatible_smul.is_scalar_tower {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [has_smul R' R] [ R M] [ N] [ R N] :
N

Note that this provides the default `compatible_smul R R M N` instance through `mul_action.is_scalar_tower.left`.

Equations
theorem tensor_product.smul_tmul {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ N] [ 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 tensor_product.smul.aux {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] {R' : Type u_2} [has_smul R' M] (r : R') :

Auxiliary function to defining scalar multiplication on tensor product.

Equations
theorem tensor_product.smul.aux_of {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] {R' : Type u_2} [has_smul R' M] (r : R') (m : M) (n : N) :
(free_add_monoid.of (m, n)) = (r m) ⊗ₜ[R] n
@[protected, instance]
def tensor_product.left_has_smul {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] :
has_smul 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
@[protected, instance]
def tensor_product.has_smul {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] :
M N)
Equations
@[protected]
theorem tensor_product.smul_zero {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] (r : R') :
r 0 = 0
@[protected]
theorem tensor_product.smul_add {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] (r : R') (x y : N) :
r (x + y) = r x + r y
@[protected]
theorem tensor_product.zero_smul {R : Type u_1} {R'' : Type u_3} [semiring R''] {M : Type u_4} {N : Type u_5} [ M] [ N] [module R'' M] [ R'' M] (x : N) :
0 x = 0
@[protected]
theorem tensor_product.one_smul {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] (x : N) :
1 x = x
@[protected]
theorem tensor_product.add_smul {R : Type u_1} {R'' : Type u_3} [semiring R''] {M : Type u_4} {N : Type u_5} [ M] [ N] [module R'' M] [ R'' M] (r s : R'') (x : N) :
(r + s) x = r x + s x
@[protected, instance]
def tensor_product.add_comm_monoid {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] :
Equations
@[protected, instance]
def tensor_product.left_distrib_mul_action {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] :
M N)
Equations
@[protected, instance]
def tensor_product.distrib_mul_action {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] :
M N)
Equations
theorem tensor_product.smul_tmul' {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] (r : R') (m : M) (n : N) :
r m ⊗ₜ[R] n = (r m) ⊗ₜ[R] n
@[simp]
theorem tensor_product.tmul_smul {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] [ N] [ N] (r : R') (x : M) (y : N) :
x ⊗ₜ[R] (r y) = r x ⊗ₜ[R] y
theorem tensor_product.smul_tmul_smul {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (r s : R) (m : M) (n : N) :
(r m) ⊗ₜ[R] (s n) = (r * s) m ⊗ₜ[R] n
@[protected, instance]
def tensor_product.left_module {R : Type u_1} {R'' : Type u_3} [semiring R''] {M : Type u_4} {N : Type u_5} [ M] [ N] [module R'' M] [ R'' M] :
module R'' M N)
Equations
@[protected, instance]
def tensor_product.module {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] :
M N)
Equations
@[protected, instance]
def tensor_product.is_central_scalar {R : Type u_1} {R'' : Type u_3} [semiring R''] {M : Type u_4} {N : Type u_5} [ M] [ N] [module R'' M] [ R'' M] [module R''ᵐᵒᵖ M] [ M] :
M N)
@[protected, instance]
def tensor_product.smul_comm_class_left {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] {R'₂ : Type u_9} [monoid R'₂] [ M] [ R'₂ M] [ R'₂ M] :
R'₂ M N)

`smul_comm_class R' R'₂ M` implies `smul_comm_class R' R'₂ (M ⊗[R] N)`

@[protected, instance]
def tensor_product.is_scalar_tower_left {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] {R'₂ : Type u_9} [monoid R'₂] [ M] [ R'₂ M] [has_smul R'₂ R'] [ R' M] :
R' M N)

`is_scalar_tower R'₂ R' M` implies `is_scalar_tower R'₂ R' (M ⊗[R] N)`

@[protected, instance]
def tensor_product.is_scalar_tower_right {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] {R'₂ : Type u_9} [monoid R'₂] [ M] [ R'₂ M] [has_smul R'₂ R'] [ N] [ N] [ N] [ N] [ R' N] :
R' M N)

`is_scalar_tower R'₂ R' N` implies `is_scalar_tower R'₂ R' (M ⊗[R] N)`

@[protected, instance]
def tensor_product.is_scalar_tower {R : Type u_1} {R' : Type u_2} [monoid R'] {M : Type u_4} {N : Type u_5} [ M] [ N] [ M] [ R' M] [has_smul R' R] [ R M] :
R M N)

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

def tensor_product.mk (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] :

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

Equations
@[simp]
theorem tensor_product.mk_apply {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (m : M) (n : N) :
( N) m) n = m ⊗ₜ[R] n
theorem tensor_product.ite_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (x₁ : M) (x₂ : N) (P : Prop) [decidable P] :
ite P x₁ 0 ⊗ₜ[R] x₂ = ite P (x₁ ⊗ₜ[R] x₂) 0
theorem tensor_product.tmul_ite {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (x₁ : M) (x₂ : N) (P : Prop) [decidable P] :
x₁ ⊗ₜ[R] ite P x₂ 0 = ite P (x₁ ⊗ₜ[R] x₂) 0
theorem tensor_product.sum_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] {α : Type u_2} (s : finset α) (m : α M) (n : N) :
s.sum (λ (a : α), m a) ⊗ₜ[R] n = s.sum (λ (a : α), m a ⊗ₜ[R] n)
theorem tensor_product.tmul_sum {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (m : M) {α : Type u_2} (s : finset α) (n : α N) :
m ⊗ₜ[R] s.sum (λ (a : α), n a) = s.sum (λ (a : α), m ⊗ₜ[R] n a)
theorem tensor_product.span_tmul_eq_top (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] :
{t : N | (m : M) (n : N), m ⊗ₜ[R] n = t} =

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

@[simp]
theorem tensor_product.map₂_mk_top_top_eq_top (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] :
def tensor_product.lift_aux {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) :
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
theorem tensor_product.lift_aux_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
(m ⊗ₜ[R] n) = (f m) n
@[simp]
theorem tensor_product.lift_aux.smul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] {f : M →ₗ[R] N →ₗ[R] P} (r : R) (x : N) :
(r x) = r
def tensor_product.lift {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) :
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
@[simp]
theorem tensor_product.lift.tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :
(x ⊗ₜ[R] y) = (f x) y
@[simp]
theorem tensor_product.lift.tmul' {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :
(x ⊗ₜ[R] y) = (f x) y
theorem tensor_product.ext' {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] {g h : N →ₗ[R] P} (H : (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) :
g = h
theorem tensor_product.lift.unique {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] {f : M →ₗ[R] N →ₗ[R] P} {g : N →ₗ[R] P} (H : (x : M) (y : N), g (x ⊗ₜ[R] y) = (f x) y) :
theorem tensor_product.lift_mk {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] :
theorem tensor_product.lift_compr₂ {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] {f : M →ₗ[R] N →ₗ[R] P} (g : P →ₗ[R] Q) :
= g.comp
theorem tensor_product.lift_mk_compr₂ {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : N →ₗ[R] P) :
theorem tensor_product.ext {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] {g h : N →ₗ[R] P} (H : N).compr₂ g = 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 `tensor_product.ext'` allows `ext` to apply lemmas specific to `M →ₗ _` and `N →ₗ _`.

def tensor_product.uncurry (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) [ M] [ N] [ 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
@[simp]
theorem tensor_product.uncurry_apply {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
( N P) f) (m ⊗ₜ[R] n) = (f m) n
def tensor_product.lift.equiv (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) [ M] [ N] [ 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
@[simp]
theorem tensor_product.lift.equiv_apply (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
( P) f) (m ⊗ₜ[R] n) = (f m) n
@[simp]
theorem tensor_product.lift.equiv_symm_apply (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) [ M] [ N] [ P] (f : N →ₗ[R] P) (m : M) (n : N) :
(( N P).symm) f) m) n = f (m ⊗ₜ[R] n)
def tensor_product.lcurry (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) [ M] [ N] [ P] :

Given a linear map `M ⊗ N → P`, compose it with the canonical bilinear map `M → N → M ⊗ N` to form a bilinear map `M → N → P`.

Equations
@[simp]
theorem tensor_product.lcurry_apply {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : N →ₗ[R] P) (m : M) (n : N) :
(( N P) f) m) n = f (m ⊗ₜ[R] n)
def tensor_product.curry {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : 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
@[simp]
theorem tensor_product.curry_apply {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : N →ₗ[R] P) (m : M) (n : N) :
m) n = f (m ⊗ₜ[R] n)
theorem tensor_product.curry_injective {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] :
theorem tensor_product.ext_threefold {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] {g h : 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 tensor_product.ext_fourfold {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [ M] [ N] [ P] [ Q] [ S] {g h : 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 tensor_product.ext_fourfold' {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [ M] [ N] [ P] [ Q] [ S] {φ ψ : M N) 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.

@[protected]
def tensor_product.lid (R : Type u_1) (M : Type u_4) [ M] :
M ≃ₗ[R] M

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

Equations
@[simp]
theorem tensor_product.lid_tmul {R : Type u_1} {M : Type u_4} [ M] (m : M) (r : R) :
M) (r ⊗ₜ[R] m) = r m
@[simp]
theorem tensor_product.lid_symm_apply {R : Type u_1} {M : Type u_4} [ M] (m : M) :
M).symm) m = 1 ⊗ₜ[R] m
@[protected]
def tensor_product.comm (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] :
N ≃ₗ[R] M

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

Equations
• N = _ _
@[simp]
theorem tensor_product.comm_tmul (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] (m : M) (n : N) :
N) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
@[simp]
theorem tensor_product.comm_symm_tmul (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] (m : M) (n : N) :
M N).symm) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
@[protected]
def tensor_product.rid (R : Type u_1) (M : Type u_4) [ M] :
R ≃ₗ[R] M

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

Equations
@[simp]
theorem tensor_product.rid_tmul {R : Type u_1} {M : Type u_4} [ M] (m : M) (r : R) :
M) (m ⊗ₜ[R] r) = r m
@[simp]
theorem tensor_product.rid_symm_apply {R : Type u_1} {M : Type u_4} [ M] (m : M) :
M).symm) m = m ⊗ₜ[R] 1
@[protected]
def tensor_product.assoc (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) [ M] [ N] [ P] :
M N) P ≃ₗ[R] N P)

The associator for tensor product of R-modules, as a linear equivalence.

Equations
@[simp]
theorem tensor_product.assoc_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (m : M) (n : N) (p : P) :
N P) (m ⊗ₜ[R] n ⊗ₜ[R] p) = m ⊗ₜ[R] (n ⊗ₜ[R] p)
@[simp]
theorem tensor_product.assoc_symm_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (m : M) (n : N) (p : P) :
M N P).symm) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = m ⊗ₜ[R] n ⊗ₜ[R] p
def tensor_product.map {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
N →ₗ[R] Q

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

Equations
@[simp]
theorem tensor_product.map_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (m : M) (n : N) :
g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
theorem tensor_product.map_range_eq_span_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
= {t : Q | (m : M) (n : N), f m ⊗ₜ[R] g n = t}
@[simp]
def tensor_product.map_incl {R : Type u_1} {P : Type u_6} {Q : Type u_7} [ P] [ Q] (p : P) (q : Q) :

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

Equations
theorem tensor_product.map_comp {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] {P' : Type u_9} {Q' : Type u_10} [add_comm_monoid P'] [ P'] [add_comm_monoid Q'] [ Q'] (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :
tensor_product.map (f₂.comp f₁) (g₂.comp g₁) = g₂).comp g₁)
theorem tensor_product.lift_comp_map {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] {Q' : Type u_10} [add_comm_monoid Q'] [ Q'] (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
@[simp]
theorem tensor_product.map_id {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] :
@[simp]
theorem tensor_product.map_one {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] :
= 1
theorem tensor_product.map_mul {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (f₁ f₂ : M →ₗ[R] M) (g₁ g₂ : N →ₗ[R] N) :
tensor_product.map (f₁ * f₂) (g₁ * g₂) = g₁ * g₂
@[protected, simp]
theorem tensor_product.map_pow {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ) :
^ n = tensor_product.map (f ^ n) (g ^ n)
theorem tensor_product.map_add_left {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f₁ f₂ : M →ₗ[R] P) (g : N →ₗ[R] Q) :
tensor_product.map (f₁ + f₂) g = +
theorem tensor_product.map_add_right {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] P) (g₁ g₂ : N →ₗ[R] Q) :
(g₁ + g₂) = +
theorem tensor_product.map_smul_left {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
theorem tensor_product.map_smul_right {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
(r g) = r
def tensor_product.map_bilinear (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [ M] [ N] [ P] [ Q] :

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

Equations
def tensor_product.ltensor_hom_to_hom_ltensor (R : Type u_1) (M : Type u_4) (P : Type u_6) (Q : Type u_7) [ M] [ P] [ Q] :
(M →ₗ[R] Q) →ₗ[R] M →ₗ[R] Q

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

Equations
def tensor_product.rtensor_hom_to_hom_rtensor (R : Type u_1) (M : Type u_4) (P : Type u_6) (Q : Type u_7) [ M] [ P] [ Q] :
(M →ₗ[R] P) Q →ₗ[R] M →ₗ[R] Q

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

Equations
def tensor_product.hom_tensor_hom_map (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [ M] [ N] [ P] [ Q] :
(M →ₗ[R] P) (N →ₗ[R] Q) →ₗ[R] N →ₗ[R] Q

The linear map from `(M →ₗ P) ⊗ (N →ₗ Q)` to `(M ⊗ N →ₗ P ⊗ Q)` sending `f ⊗ₜ g` to the `tensor_product.map f g`, the tensor product of the two maps.

Equations
@[simp]
theorem tensor_product.map_bilinear_apply {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
( P Q) f) g =
@[simp]
theorem tensor_product.ltensor_hom_to_hom_ltensor_apply {R : Type u_1} {M : Type u_4} {P : Type u_6} {Q : Type u_7} [ M] [ P] [ Q] (p : P) (f : M →ₗ[R] Q) (m : M) :
( (p ⊗ₜ[R] f)) m = p ⊗ₜ[R] f m
@[simp]
theorem tensor_product.rtensor_hom_to_hom_rtensor_apply {R : Type u_1} {M : Type u_4} {P : Type u_6} {Q : Type u_7} [ M] [ P] [ Q] (f : M →ₗ[R] P) (q : Q) (m : M) :
( (f ⊗ₜ[R] q)) m = f m ⊗ₜ[R] q
@[simp]
theorem tensor_product.hom_tensor_hom_map_apply {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
Q) (f ⊗ₜ[R] g) =
def tensor_product.congr {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
N ≃ₗ[R] 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
@[simp]
theorem tensor_product.congr_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) :
g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
@[simp]
theorem tensor_product.congr_symm_tmul {R : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) :
g).symm) (p ⊗ₜ[R] q) = (f.symm) p ⊗ₜ[R] (g.symm) q
def tensor_product.left_comm (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) [ M] [ N] [ P] :
N P) ≃ₗ[R] M P)

A tensor product analogue of `mul_left_comm`.

Equations
@[simp]
theorem tensor_product.left_comm_tmul (R : Type u_1) {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (m : M) (n : N) (p : P) :
N P) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = n ⊗ₜ[R] (m ⊗ₜ[R] p)
@[simp]
theorem tensor_product.left_comm_symm_tmul (R : Type u_1) {M : Type u_4} {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (m : M) (n : N) (p : P) :
N P).symm) (n ⊗ₜ[R] (m ⊗ₜ[R] p)) = m ⊗ₜ[R] (n ⊗ₜ[R] p)
def tensor_product.tensor_tensor_tensor_comm (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [ M] [ N] [ P] [ Q] :
M N) P Q) ≃ₗ[R] M P) 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 `tensor_product.semiring` instance (currently defined "by hand" using `tensor_product.mul`).

See also `mul_mul_mul_comm`.

Equations
@[simp]
theorem tensor_product.tensor_tensor_tensor_comm_tmul (R : Type u_1) {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (m : M) (n : N) (p : P) (q : Q) :
Q) (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)) = m ⊗ₜ[R] p ⊗ₜ[R] (n ⊗ₜ[R] q)
@[simp]
theorem tensor_product.tensor_tensor_tensor_comm_symm (R : Type u_1) {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] :
Q).symm =
def tensor_product.tensor_tensor_tensor_assoc (R : Type u_1) (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [ M] [ N] [ P] [ Q] :
M N) P Q) ≃ₗ[R] M N P)) Q

This special case is useful for describing the interplay between `dual_tensor_hom_equiv` 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 `contract_right` on `N ⊗ N.dual` after the suitable rebracketting.

Equations
@[simp]
theorem tensor_product.tensor_tensor_tensor_assoc_tmul (R : Type u_1) {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (m : M) (n : N) (p : P) (q : Q) :
Q) (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)) = m ⊗ₜ[R] (n ⊗ₜ[R] p) ⊗ₜ[R] q
@[simp]
theorem tensor_product.tensor_tensor_tensor_assoc_symm_tmul (R : Type u_1) {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (m : M) (n : N) (p : P) (q : Q) :
Q).symm) (m ⊗ₜ[R] (n ⊗ₜ[R] p) ⊗ₜ[R] q) = m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)
def linear_map.ltensor {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : N →ₗ[R] P) :
N →ₗ[R] P

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

Equations
def linear_map.rtensor {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : N →ₗ[R] P) :
M →ₗ[R] M

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

Equations
@[simp]
theorem linear_map.ltensor_tmul {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : N →ₗ[R] P) (m : M) (n : N) :
f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
@[simp]
theorem linear_map.rtensor_tmul {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f : N →ₗ[R] P) (m : M) (n : N) :
f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m
def linear_map.ltensor_hom {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] :

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

Equations
def linear_map.rtensor_hom {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] :

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

Equations
@[simp]
theorem linear_map.coe_ltensor_hom {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] :
@[simp]
theorem linear_map.coe_rtensor_hom {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] :
@[simp]
theorem linear_map.ltensor_add {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f g : N →ₗ[R] P) :
(f + g) =
@[simp]
theorem linear_map.rtensor_add {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (f g : N →ₗ[R] P) :
(f + g) =
@[simp]
theorem linear_map.ltensor_zero {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] :
= 0
@[simp]
theorem linear_map.rtensor_zero {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] :
= 0
@[simp]
theorem linear_map.ltensor_smul {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (r : R) (f : N →ₗ[R] P) :
(r f) = r
@[simp]
theorem linear_map.rtensor_smul {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} [ M] [ N] [ P] (r : R) (f : N →ₗ[R] P) :
(r f) = r
theorem linear_map.ltensor_comp {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) :
(g.comp f) = g).comp f)
theorem linear_map.ltensor_comp_apply {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : N) :
(g.comp f)) x = g) ( f) x)
theorem linear_map.rtensor_comp {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) :
(g.comp f) = g).comp f)
theorem linear_map.rtensor_comp_apply {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : M) :
(g.comp f)) x = g) ( f) x)
theorem linear_map.ltensor_mul {R : Type u_1} (M : Type u_4) {N : Type u_5} [ M] [ N] (f g : N) :
(f * g) =
theorem linear_map.rtensor_mul {R : Type u_1} (M : Type u_4) {N : Type u_5} [ M] [ N] (f g : N) :
(f * g) =
@[simp]
theorem linear_map.ltensor_id {R : Type u_1} (M : Type u_4) (N : Type u_5) [ M] [ N] :
theorem linear_map.ltensor_id_apply {R : Type u_1} (M : Type u_4) (N : Type u_5) [ M] [ N] (x : N) :
@[simp]
theorem linear_map.rtensor_id {R : Type u_1} (M : Type u_4) (N : Type u_5) [ M] [ N] :
theorem linear_map.rtensor_id_apply {R : Type u_1} (M : Type u_4) (N : Type u_5) [ M] [ N] (x : M) :
@[simp]
theorem linear_map.ltensor_comp_rtensor {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
g).comp f) =
@[simp]
theorem linear_map.rtensor_comp_ltensor {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
f).comp g) =
@[simp]
theorem linear_map.map_comp_rtensor {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [ M] [ N] [ P] [ Q] [ S] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) :
g).comp f') = tensor_product.map (f.comp f') g
@[simp]
theorem linear_map.map_comp_ltensor {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [ M] [ N] [ P] [ Q] [ S] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) :
g).comp g') = (g.comp g')
@[simp]
theorem linear_map.rtensor_comp_map {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [ M] [ N] [ P] [ Q] [ S] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
f').comp g) = tensor_product.map (f'.comp f) g
@[simp]
theorem linear_map.ltensor_comp_map {R : Type u_1} (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [ M] [ N] [ P] [ Q] [ S] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
g').comp g) = (g'.comp g)
@[simp]
theorem linear_map.rtensor_pow {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (f : M →ₗ[R] M) (n : ) :
^ n = (f ^ n)
@[simp]
theorem linear_map.ltensor_pow {R : Type u_1} {M : Type u_4} {N : Type u_5} [ M] [ N] (f : N →ₗ[R] N) (n : ) :
^ n = (f ^ n)
def tensor_product.neg.aux (R : Type u_1) {M : Type u_2} {N : Type u_3} [ M] [ N] :

Auxiliary function to defining negation multiplication on tensor product.

Equations
theorem tensor_product.neg.aux_of {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (m : M) (n : N) :
(free_add_monoid.of (m, n)) = (-m) ⊗ₜ[R] n
@[protected, instance]
def tensor_product.has_neg {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] :
has_neg M N)
Equations
@[protected]
theorem tensor_product.add_left_neg {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (x : N) :
-x + x = 0
@[protected, instance]
def tensor_product.add_comm_group {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] :
Equations
theorem tensor_product.neg_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (m : M) (n : N) :
(-m) ⊗ₜ[R] n = -m ⊗ₜ[R] n
theorem tensor_product.tmul_neg {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (m : M) (n : N) :
theorem tensor_product.tmul_sub {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (m : M) (n₁ n₂ : N) :
m ⊗ₜ[R] (n₁ - n₂) = m ⊗ₜ[R] n₁ - m ⊗ₜ[R] n₂
theorem tensor_product.sub_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (m₁ m₂ : M) (n : N) :
(m₁ - m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n
@[protected, instance]
def tensor_product.compatible_smul.int {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] :

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

When `R` is a `ring` we get the required `tensor_product.compatible_smul` instance through `is_scalar_tower`, but when it is only a `semiring` we need to build it from scratch. The instance diamond in `compatible_smul` doesn't matter because it's in `Prop`.

Equations
@[protected, instance]
def tensor_product.compatible_smul.unit {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] {S : Type u_4} [monoid S] [ M] [ N] [ N] :
Equations
@[simp]
theorem linear_map.ltensor_sub {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f g : N →ₗ[R] P) :
(f - g) =
@[simp]
theorem linear_map.rtensor_sub {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f g : N →ₗ[R] P) :
(f - g) =
@[simp]
theorem linear_map.ltensor_neg {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : N →ₗ[R] P) :
(-f) =
@[simp]
theorem linear_map.rtensor_neg {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : N →ₗ[R] P) :
(-f) =