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)

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

noncomputable 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

noncomputable 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

noncomputable 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 = AddZeroClass.mk ⋯ ⋯

noncomputable 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 = AddSemigroup.mk ⋯

noncomputable 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 = AddCommSemigroup.mk ⋯

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

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

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

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

noncomputable 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 := ⋯ }

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

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

noncomputable instance TensorProduct.leftHasSMul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_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) ⋯) }

noncomputable 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

noncomputable 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

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

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

noncomputable 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 = DistribMulAction.mk ⋯ ⋯

noncomputable 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

noncomputable 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 = Module.mk ⋯ ⋯

noncomputable 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_11} [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_11} [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_11} [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.

noncomputable 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_11} [DecidableEq ι] {M : ι → Type u_12} [(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_11} [DecidableEq ι] {M : ι → Type u_12} [(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_11} (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_11} (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

noncomputable def TensorProduct.liftAux {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) : 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} {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) : (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} {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

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

Constructing a linear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations

• TensorProduct.lift f = { 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} {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} (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} {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} (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} {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 : ∀ (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} {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} {g : TensorProduct R M N →ₗ[R] 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].

noncomputable 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 = (TensorProduct.lift (LinearMap.lflip ∘ₗ LinearMap.id.flip)).flip

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

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

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

noncomputable 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

@[deprecated TensorProduct.ext_threefold (since := "2024-10-18")]

theorem TensorProduct.ext₃ {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

Alias of TensorProduct.ext_threefold.

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.

noncomputable 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

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

noncomputable 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' := ⋯ }

noncomputable 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 := ⋯ }

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

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

Equations

• TensorProduct.map f g = TensorProduct.lift ((TensorProduct.mk R P Q).compl₂ g ∘ₗ f)

@[simp]

theorem TensorProduct.map_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) : (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.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}

noncomputable 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.span R (Set.image2 (fun (x1 : P) (x2 : Q) => x1 ⊗ₜ[R] x2) ↑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} {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] {P' : Type u_11} {Q' : Type u_12} [AddCommMonoid P'] [Module R P'] [AddCommMonoid Q'] [Module R Q'] (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) : map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = map f₂ g₂ ∘ₗ map f₁ g₁

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_12} [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

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

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

noncomputable 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

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

noncomputable 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

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

noncomputable 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

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

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

Equations

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

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

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

noncomputable 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

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

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

Auxiliary function to defining negation multiplication on tensor product.

Equations

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

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

Equations

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

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

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

Equations

• TensorProduct.addCommGroup = AddCommGroup.mk ⋯

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

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

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

theorem TensorProduct.sub_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m₁ m₂ : M) (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} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] : CompatibleSMul R ℤ M N

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] [AddCommGroup 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] [AddCommGroup 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] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : rTensor M (f - g) = rTensor M f - rTensor M g

@[simp]

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

@[simp]

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