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.

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_7) (N : Type u_8) [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : Type (max u_7 u_8)

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.

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.

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.

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

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

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

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

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

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

def TensorProduct.tmul (R : Type u_1) [CommSemiring R] {M : Type u_7} {N : Type u_8} [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.

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

The canonical function M → N → M ⊗ N.

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

The canonical function M → N → M ⊗ N.

unsafe instance TensorProduct.instRepr {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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₀ + ....

theorem TensorProduct.induction_on {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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

@[simp]

theorem TensorProduct.zero_tmul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} [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_7} {N : Type u_8} [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_7} (N : Type u_8) [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_7} {N : Type u_8} [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_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Subsingleton M] : Unique (TensorProduct R M N)

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

class TensorProduct.CompatibleSMul (R : Type u_1) (R' : Type u_4) [CommSemiring R] [Monoid R'] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [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} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [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} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [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_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_22} [SMul R' M] (r : R') : FreeAddMonoid (M × N) →+ TensorProduct R M N

Auxiliary function to defining scalar multiplication on tensor product.

theorem TensorProduct.SMul.aux_of {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_22} [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} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [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.

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

theorem TensorProduct.smul_zero {R : Type u_1} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [SMulCommClass R R' M] (r : R') : r • 0 = 0

theorem TensorProduct.smul_add {R : Type u_1} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [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} {R'' : Type u_5} [CommSemiring R] [Semiring R''] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R'' M] [Module R M] [Module R N] [SMulCommClass R R'' M] (x : TensorProduct R M N) : 0 • x = 0

theorem TensorProduct.one_smul {R : Type u_1} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [SMulCommClass R R' M] (x : TensorProduct R M N) : 1 • x = x

theorem TensorProduct.add_smul {R : Type u_1} {R'' : Type u_5} [CommSemiring R] [Semiring R''] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R'' M] [Module R M] [Module R N] [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_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : AddMonoid (TensorProduct R M N)

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

theorem IsAddUnit.tmul_left (R : Type u_1) [CommSemiring R] {M : Type u_7} {N : Type u_8} [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_7} {N : Type u_8} [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} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [SMulCommClass R R' M] : DistribMulAction R' (TensorProduct R M N)

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

theorem TensorProduct.smul_tmul' {R : Type u_1} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [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} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [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_7} {N : Type u_8} [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_7} [AddCommMonoid M] [Module R M] {S : Type u_22} [Semiring S] [Module R S] [SMulCommClass R S S] (s : S) (m : M) : s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

instance TensorProduct.leftModule {R : Type u_1} {R'' : Type u_5} [CommSemiring R] [Semiring R''] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R'' M] [Module R M] [Module R N] [SMulCommClass R R'' M] : Module R'' (TensorProduct R M N)

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

instance TensorProduct.instIsCentralScalar {R : Type u_1} {R'' : Type u_5} [CommSemiring R] [Semiring R''] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R'' M] [Module R M] [Module R N] [SMulCommClass R R'' M] [Module R''ᵐᵒᵖ M] [IsCentralScalar R'' M] : IsCentralScalar R'' (TensorProduct R M N)

instance TensorProduct.smulCommClass_left {R : Type u_1} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [SMulCommClass R R' M] {R'₂ : Type u_22} [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} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [SMulCommClass R R' M] {R'₂ : Type u_22} [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} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [SMulCommClass R R' M] {R'₂ : Type u_22} [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} {R' : Type u_4} [CommSemiring R] [Monoid R'] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R' M] [Module R M] [Module R N] [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_7) (N : Type u_8) [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.

@[simp]

theorem TensorProduct.mk_apply {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_8} [AddCommMonoid N] [Module R N] {ι : Type u_22} [DecidableEq ι] {M : ι → Type u_23} [(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_8} [AddCommMonoid N] [Module R N] {ι : Type u_22} [DecidableEq ι] {M : ι → Type u_23} [(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_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {α : Type u_22} (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_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) {α : Type u_22} (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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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