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 →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂, there is a unique semilinear map TensorProduct.lift f : TensorProduct R M N →ₛₗ[σ₁₂] 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_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.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• m ⊗ₜ[R] n = (addConGen (TensorProduct.Eqv R M N)).mk' (FreeAddMonoid.of (m, n))

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

The canonical function M → N → M ⊗ N.

Equations

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

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

The canonical function M → N → M ⊗ N.

Equations

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

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

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

def TensorProduct.liftAddHom {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [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_7} {N : Type u_8} {P : Type u_9} [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_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)

Equations

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

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)

Equations

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

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.

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

Equations

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

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

Equations

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

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

Equations

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

theorem IsAddUnit.tmul_left (R : Type u_1) [CommSemiring R] {M : Type u_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)

Equations

• TensorProduct.leftDistribMulAction = { toSMul := TensorProduct.leftHasSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

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

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

theorem TensorProduct.tsmul_eq_smul_one_tuml {R : Type u_1} [CommSemiring R] {M : Type u_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

Alias of TensorProduct.tmul_eq_smul_one_tmul.

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)

Equations

• TensorProduct.leftModule = { toDistribMulAction := TensorProduct.leftDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

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)

Equations

• TensorProduct.instModule = TensorProduct.leftModule

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.

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

def TensorProduct.liftAux {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) : TensorProduct R M N →+ P₂

Auxiliary function to constructing a linear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations

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

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

@[simp]

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

theorem TensorProduct.liftAux.smul {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (r : R) (x : TensorProduct R M N) : (liftAux f) (r • x) = r • (liftAux f) x

def TensorProduct.lift {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) : TensorProduct R M N →ₛₗ[σ₁₂] P₂

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

This works for semilinear maps.

Equations

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

@[simp]

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

@[simp]

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

theorem TensorProduct.ext' {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) : g = h

theorem TensorProduct.lift.unique {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} {g : TensorProduct R M N →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f' x) y) : g = lift f'

theorem TensorProduct.lift_mk {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} {P₃ : Type u_18} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [AddCommMonoid P₃] [Module R M] [Module R N] [Module R₂ P₂] [Module R₃ P₃] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : P₂ →ₛₗ[σ₂₃] P₃) : lift (f'.compr₂ₛₗ h) = h ∘ₛₗ lift f'

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

theorem TensorProduct.lift_mk_compr₂ₛₗ {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (g : TensorProduct R M N →ₛₗ[σ₁₂] P₂) : lift ((mk R M N).compr₂ₛₗ g) = g

theorem TensorProduct.lift_mk_compr₂ {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂} (H : (mk R M N).compr₂ₛₗ g = (mk R M N).compr₂ₛₗ h) : g = h

This used to be an @[ext] lemma, but it fails very slowly when the ext tactic tries to apply it in some cases, notably when one wants to show equality of two linear maps. The @[ext] attribute is now added locally where it is needed. Using this as the @[ext] lemma instead of TensorProduct.ext' allows ext to apply lemmas specific to M →ₗ _ and N →ₗ _.

See note [partially-applied ext lemmas].

theorem TensorProduct.ext_iff {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂} : g = h ↔ (mk R M N).compr₂ₛₗ g = (mk R M N).compr₂ₛₗ h

def TensorProduct.uncurry {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] : (M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) →ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] P₂

Linearly constructing a semilinear 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 σ₁₂ M N P₂ = { toFun := TensorProduct.lift, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TensorProduct.uncurry_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) : ((uncurry σ₁₂ M N P₂) f) (m ⊗ₜ[R] n) = (f m) n

def TensorProduct.lift.equiv {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] : (M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) ≃ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] P₂

A linear equivalence constructing a semilinear 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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) : ((equiv σ₁₂ M N P₂) f) (m ⊗ₜ[R] n) = (f m) n

@[simp]

theorem TensorProduct.lift.equiv_symm_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) : (((equiv σ₁₂ M N P₂).symm f) m) n = f (m ⊗ₜ[R] n)

def TensorProduct.lcurry {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] : (TensorProduct R M N →ₛₗ[σ₁₂] P₂) →ₗ[R₂] M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂

Given a semilinear 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 σ₁₂ M N P₂ = ↑(TensorProduct.lift.equiv σ₁₂ M N P₂).symm

@[simp]

theorem TensorProduct.lcurry_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) : (((lcurry σ₁₂ M N P₂) f) m) n = f (m ⊗ₜ[R] n)

def TensorProduct.curry {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂

Given a semilinear 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 σ₁₂ M N P₂) f

@[simp]

theorem TensorProduct.curry_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) : ((curry f) m) n = f (m ⊗ₜ[R] n)

theorem TensorProduct.curry_injective {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] {g h : TensorProduct R (TensorProduct R M N) P →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] y ⊗ₜ[R] z) = h (x ⊗ₜ[R] y ⊗ₜ[R] z)) : g = h

theorem TensorProduct.ext_threefold' {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] {g h : TensorProduct R M (TensorProduct R N P) →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] (y ⊗ₜ[R] z)) = h (x ⊗ₜ[R] (y ⊗ₜ[R] z))) : g = h

theorem TensorProduct.ext_fourfold {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] [Module R Q] {g h : TensorProduct R (TensorProduct R (TensorProduct R M N) P) Q →ₛₗ[σ₁₂] P₂} (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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] [Module R Q] {φ ψ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₛₗ[σ₁₂] P₂} (H : ∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) = ψ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z))) : φ = ψ

Two semilinear maps (M ⊗ N) ⊗ (P ⊗ Q) → P₂ which agree on all elements of the form (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) are equal.

theorem TensorProduct.ext_fourfold'' {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] [Module R Q] {φ ψ : TensorProduct R (TensorProduct R M (TensorProduct R N P)) Q →ₛₗ[σ₁₂] P₂} (H : ∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) = ψ (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z)) : φ = ψ

Two semilinear maps M ⊗ (N ⊗ P) ⊗ Q → P₂ which agree on all elements of the form m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q are equal.

def TensorProduct.comm (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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) {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} (M : Type u_7) (N : Type u_8) {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) : lift f ∘ₛₗ ↑(TensorProduct.comm R N M) = lift f.flip

def TensorProduct.mapOfCompatibleSMul (R : Type u_1) [CommSemiring R] (A : Type u_6) (M : Type u_7) (N : Type u_8) [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_6) (M : Type u_7) (N : Type u_8) [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_6) (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] : Function.Surjective ⇑(mapOfCompatibleSMul R A M N)

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

mapOfCompatibleSMul R A M N is also R-linear.

Equations

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

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

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

Equations

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

def TensorProduct.map {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

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

Equations

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

def RingTheory.LinearMap.«term_⊗ₘ_» : Lean.TrailingParserDescr

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

Equations

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

@[simp]

theorem TensorProduct.map_tmul {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (m : M) (n : N) : (map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R₂] g n

theorem TensorProduct.map_comp_comm_eq {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : map f g ∘ₛₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R₂ N₂ M₂) ∘ₛₗ map g f

Given semilinear 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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R N M) : (map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R₂ N₂ M₂) ((map g f) x)

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

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

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

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

Alias of TensorProduct.range_map_eq_span_tmul.

def TensorProduct.mapIncl {R : Type u_1} [CommSemiring R] {P : Type u_9} {Q : Type u_10} [AddCommMonoid P] [AddCommMonoid Q] [Module R P] [Module R Q] (p : Submodule R P) (q : Submodule R Q) : TensorProduct R ↥p ↥q →ₗ[R] TensorProduct R P Q

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

Equations

• TensorProduct.mapIncl p q = TensorProduct.map p.subtype q.subtype

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

theorem TensorProduct.map₂_eq_range_lift_comp_mapIncl {R : Type u_1} [CommSemiring R] {M : Type u_7} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] (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} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) : map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) = map f₂ g₂ ∘ₛₗ map f₁ g₁

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

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

theorem TensorProduct.range_mapIncl_mono {R : Type u_1} [CommSemiring R] {P : Type u_9} {Q : Type u_10} [AddCommMonoid P] [AddCommMonoid Q] [Module R P] [Module R Q] {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} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} {P₃ : Type u_18} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid P₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ P₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (i : M₂ →ₛₗ[σ₂₃] N₂ →ₛₗ[σ₂₃] P₃) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : lift i ∘ₛₗ map f g = lift ((i ∘ₛₗ f).compl₂ g)

@[simp]

theorem TensorProduct.map_id {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f₁ f₂ : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : map (f₁ + f₂) g = map f₁ g + map f₂ g

theorem TensorProduct.map_add_right {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g₁ g₂ : N →ₛₗ[σ₁₂] N₂) : map f (g₁ + g₂) = map f g₁ + map f g₂

theorem TensorProduct.map_smul_left {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (r : R₂) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : map (r • f) g = r • map f g

theorem TensorProduct.map_smul_right {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (r : R₂) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : map f (r • g) = r • map f g

def TensorProduct.mapBilinear {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (M₂ : Type u_12) (N₂ : Type u_14) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] : (M →ₛₗ[σ₁₂] M₂) →ₗ[R₂] (N →ₛₗ[σ₁₂] N₂) →ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

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

Equations

• TensorProduct.mapBilinear σ₁₂ M N M₂ N₂ = LinearMap.mk₂ R₂ TensorProduct.map ⋯ ⋯ ⋯ ⋯

def TensorProduct.lTensorHomToHomLTensor {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (P : Type u_9) (M₂ : Type u_12) (N₂ : Type u_14) [AddCommMonoid P] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] [Module R P] : TensorProduct R₂ M₂ (P →ₛₗ[σ₁₂] N₂) →ₗ[R₂] P →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

The canonical linear map from M₂ ⊗[R₂] (P →ₛₗ[σ₁₂] N₂) to P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂.

Equations

• TensorProduct.lTensorHomToHomLTensor σ₁₂ P M₂ N₂ = TensorProduct.lift (LinearMap.llcomp R₂ P N₂ (TensorProduct R₂ M₂ N₂) ∘ₗ TensorProduct.mk R₂ M₂ N₂)

def TensorProduct.rTensorHomToHomRTensor {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (P : Type u_9) (M₂ : Type u_12) (N₂ : Type u_14) [AddCommMonoid P] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] [Module R P] : TensorProduct R₂ (P →ₛₗ[σ₁₂] M₂) N₂ →ₗ[R₂] P →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

The canonical linear map from (P →ₛₗ[σ₁₂] M₂) ⊗[R₂] N₂ to P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂.

Equations

• TensorProduct.rTensorHomToHomRTensor σ₁₂ P M₂ N₂ = TensorProduct.lift (LinearMap.llcomp R₂ P M₂ (TensorProduct R₂ M₂ N₂) ∘ₗ (TensorProduct.mk R₂ M₂ N₂).flip).flip

def TensorProduct.homTensorHomMap {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (M₂ : Type u_12) (N₂ : Type u_14) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] : TensorProduct R₂ (M →ₛₗ[σ₁₂] M₂) (N →ₛₗ[σ₁₂] N₂) →ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

The linear map from (M →ₛₗ[σ₁₂] M₂) ⊗ (N →ₛₗ[σ₁₂] N₂) to M ⊗ N →ₛₗ[σ₁₂] M₂ ⊗ N₂ sending f ⊗ₜ g to TensorProduct.map f g, the tensor product of the two maps.

Equations

• TensorProduct.homTensorHomMap σ₁₂ M N M₂ N₂ = TensorProduct.lift (TensorProduct.mapBilinear σ₁₂ M N M₂ N₂)

def TensorProduct.map₂ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] (f : M →ₛₗ[σ₁₃] M₂ →ₛₗ[σ₂₃] M₃) (g : N →ₛₗ[σ₁₃] N₂ →ₛₗ[σ₂₃] N₃) : TensorProduct R M N →ₛₗ[σ₁₃] TensorProduct R₂ M₂ N₂ →ₛₗ[σ₂₃] TensorProduct R₃ M₃ N₃

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 semilinear 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 σ₂₃ M₂ N₂ M₃ N₃ ∘ₛₗ TensorProduct.map f g

@[simp]

theorem TensorProduct.mapBilinear_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : ((mapBilinear σ₁₂ M N M₂ N₂) f) g = map f g

@[simp]

theorem TensorProduct.lTensorHomToHomLTensor_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {P : Type u_9} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid P] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] [Module R P] (m₂ : M₂) (f : P →ₛₗ[σ₁₂] N₂) (p : P) : ((lTensorHomToHomLTensor σ₁₂ P M₂ N₂) (m₂ ⊗ₜ[R₂] f)) p = m₂ ⊗ₜ[R₂] f p

@[simp]

theorem TensorProduct.rTensorHomToHomRTensor_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {P : Type u_9} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid P] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] [Module R P] (f : P →ₛₗ[σ₁₂] M₂) (n₂ : N₂) (p : P) : ((rTensorHomToHomRTensor σ₁₂ P M₂ N₂) (f ⊗ₜ[R₂] n₂)) p = f p ⊗ₜ[R₂] n₂

@[simp]

theorem TensorProduct.homTensorHomMap_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : (homTensorHomMap σ₁₂ M N M₂ N₂) (f ⊗ₜ[R₂] g) = map f g

@[simp]

theorem TensorProduct.map₂_apply_tmul {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] (f : M →ₛₗ[σ₁₃] M₂ →ₛₗ[σ₂₃] M₃) (g : N →ₛₗ[σ₁₃] N₂ →ₛₗ[σ₂₃] N₃) (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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (g : N →ₛₗ[σ₁₂] N₂) : map 0 g = 0

@[simp]

theorem TensorProduct.map_zero_right {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) : map f 0 = 0

def TensorProduct.congr {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : TensorProduct R M N ≃ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

If M and P are semilinearly equivalent and N and Q are semilinearly equivalent then M ⊗ N and P ⊗ Q are semilinearly equivalent.

Equations

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

@[simp]

theorem TensorProduct.toLinearMap_congr {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : ↑(congr f g) = map ↑f ↑g

@[simp]

theorem TensorProduct.congr_tmul {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) (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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) (p : M₂) (q : N₂) : (congr f g).symm (p ⊗ₜ[R₂] q) = f.symm p ⊗ₜ[R] g.symm q

theorem TensorProduct.congr_symm {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : (congr f g).symm = congr f.symm g.symm

@[simp]

theorem TensorProduct.congr_refl_refl {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₃₁ : R₃ →+* R} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂) (g₁ : N ≃ₛₗ[σ₁₂] N₂) : congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂)

theorem TensorProduct.congr_congr {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₃₁ : R₃ →+* R} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂) (g₁ : N ≃ₛₗ[σ₁₂] N₂) (x : TensorProduct R M N) : (congr f₂ g₂) ((congr f₁ g₁) x) = (congr (f₁.trans f₂) (g₁.trans g₂)) x

theorem TensorProduct.congr_mul {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℤ) : congr f g ^ n = congr (f ^ n) (g ^ n)

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

instance TensorProduct.instSmall {R : Type u_22} {M : Type u_23} {N : Type u_24} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Small.{u, u_23} M] [Small.{u, u_24} N] : Small.{u, max u_24 u_23} (TensorProduct R M N)

def LinearMap.lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : TensorProduct R M N →ₗ[R] TensorProduct R M P

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

Equations

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

def LinearMap.rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [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 →ₗ P ⊗ M is the natural linear map induced by f : N →ₗ P.

Equations

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

theorem LinearMap.lTensor_def {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (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_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Bijective ⇑(lTensor M f) ↔ Function.Bijective ⇑(rTensor M f)

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

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

def LinearMap.lTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (N →ₗ[R] P) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M P

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

See also Module.End.lTensorAlgHom.

Equations

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

def LinearMap.rTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (N →ₗ[R] P) →ₗ[R] TensorProduct R N M →ₗ[R] TensorProduct R P M

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

See also Module.End.rTensorAlgHom.

Equations

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

@[simp]

theorem LinearMap.coe_lTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : lTensor M (g ∘ₗ f) = lTensor M g ∘ₗ lTensor M f

theorem LinearMap.lTensor_comp_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R M N) : (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : rTensor M (g ∘ₗ f) = rTensor M g ∘ₗ rTensor M f

theorem LinearMap.rTensor_comp_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R N M) : (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_7) {N : Type u_8} [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_7) {N : Type u_8} [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : 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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : 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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) : TensorProduct.map f g ∘ₗ rTensor N f' = TensorProduct.map (f ∘ₗ f') g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LinearMap.rTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N →ₗ[R] N) (n : ℕ) : lTensor M f ^ n = lTensor M (f ^ n)

def LinearEquiv.lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : TensorProduct R M N ≃ₗ[R] TensorProduct R M P

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

Equations

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

def LinearEquiv.rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (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_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) : lTensor M (f ≪≫ₗ g) = lTensor M f ≪≫ₗ lTensor M g

theorem LinearEquiv.lTensor_trans_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (x : TensorProduct R M N) : (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) : rTensor M (f ≪≫ₗ g) = rTensor M f ≪≫ₗ rTensor M g

theorem LinearEquiv.rTensor_trans_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (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_7) {N : Type u_8} [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_7) {N : Type u_8} [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) (N : Type u_8) [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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : 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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : 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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [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_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N ≃ₗ[R] N) (n : ℤ) : lTensor M f ^ n = lTensor M (f ^ n)

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

Auxiliary function to defining negation multiplication on tensor product.

Equations

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

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

Equations

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

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

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

Equations

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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