Documentation

Mathlib.LinearAlgebra.TensorProduct.Basic

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 M → N → TensorProduct R M N.

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

We start by proving basic lemmas about bilinear maps.

Notations #

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

Tags #

bilinear, tensor, tensor product

inductive TensorProduct.Eqv (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [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.

Instances For
    noncomputable def TensorProduct (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
    Type (max u_4 u_5)

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

    Equations
    Instances For

      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.
      Instances For

        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.
        Instances For
          noncomputable instance TensorProduct.add {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
          Equations
          noncomputable instance TensorProduct.addZeroClass {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
          Equations
          noncomputable instance TensorProduct.addSemigroup {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
          Equations
          noncomputable instance TensorProduct.instInhabitedTensorProduct {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
          Equations
          noncomputable def TensorProduct.tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :

          The canonical function M → N → M ⊗ N. The localized notations are m ⊗ₜ n and m ⊗ₜ[R] n, accessed by open scoped TensorProduct.

          Equations
          Instances For

            The canonical function M → N → M ⊗ N.

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

              The canonical function M → N → M ⊗ N.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem TensorProduct.induction_on {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {motive : TensorProduct R M NProp} (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 xmotive ymotive (x + y)) :
                motive z
                noncomputable def TensorProduct.liftAddHom {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [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)) :

                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
                Instances For
                  @[simp]
                  theorem TensorProduct.liftAddHom_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [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) :
                  (TensorProduct.liftAddHom f hf) (m ⊗ₜ[R] n) = (f m) n
                  @[simp]
                  theorem TensorProduct.zero_tmul {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} [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_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m₁ : 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_4} (N : Type u_5) [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_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n₁ : N) (n₂ : N) :
                  m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂
                  noncomputable instance TensorProduct.uniqueLeft {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Subsingleton M] :
                  Equations
                  • TensorProduct.uniqueLeft = { toInhabited := { default := 0 }, uniq := }
                  noncomputable instance TensorProduct.uniqueRight {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Subsingleton N] :
                  Equations
                  • TensorProduct.uniqueRight = { toInhabited := { default := 0 }, uniq := }
                  class TensorProduct.CompatibleSMul (R : Type u_1) [CommSemiring R] (R' : Type u_2) [Monoid R'] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [DistribMulAction R' N] :

                  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.intModule, 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.

                  Instances
                    noncomputable instance TensorProduct.CompatibleSMul.isScalarTower {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMul R' R] [IsScalarTower R' R M] [DistribMulAction R' N] [IsScalarTower R' R N] :

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

                    Equations
                    • =
                    theorem TensorProduct.smul_tmul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [DistribMulAction R' N] [TensorProduct.CompatibleSMul R R' M N] (r : R') (m : M) (n : N) :
                    (r m) ⊗ₜ[R] n = m ⊗ₜ[R] (r n)

                    smul can be moved from one side of the product to the other .

                    noncomputable def TensorProduct.SMul.aux {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_10} [SMul R' M] (r : R') :

                    Auxiliary function to defining scalar multiplication on tensor product.

                    Equations
                    Instances For
                      theorem TensorProduct.SMul.aux_of {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_10} [SMul R' M] (r : R') (m : M) (n : N) :
                      noncomputable instance TensorProduct.leftHasSMul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] :
                      SMul R' (TensorProduct R M N)

                      Given two modules over a commutative semiring R, if one of the factors carries a (distributive) action of a second type of scalars R', which commutes with the action of R, then the tensor product (over R) carries an action of R'.

                      This instance defines this R' action in the case that it is the left module which has the R' action. Two natural ways in which this situation arises are:

                      • Extension of scalars
                      • A tensor product of a group representation with a module not carrying an action

                      Note that in the special case that R = R', since R is commutative, we just get the usual scalar action on a tensor product of two modules. This special case is important enough that, for performance reasons, we define it explicitly below.

                      Equations
                      noncomputable instance TensorProduct.instSMulTensorProduct {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                      Equations
                      • TensorProduct.instSMulTensorProduct = TensorProduct.leftHasSMul
                      theorem TensorProduct.smul_zero {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (r : R') :
                      r 0 = 0
                      theorem TensorProduct.smul_add {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (r : R') (x : TensorProduct R M N) (y : TensorProduct R M N) :
                      r (x + y) = r x + r y
                      theorem TensorProduct.zero_smul {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module R'' M] [SMulCommClass R R'' M] (x : TensorProduct R M N) :
                      0 x = 0
                      theorem TensorProduct.one_smul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (x : TensorProduct R M N) :
                      1 x = x
                      theorem TensorProduct.add_smul {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module R'' M] [SMulCommClass R R'' M] (r : R'') (s : R'') (x : TensorProduct R M N) :
                      (r + s) x = r x + s x
                      noncomputable instance TensorProduct.addMonoid {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                      Equations
                      noncomputable instance TensorProduct.addCommMonoid {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                      Equations
                      noncomputable instance TensorProduct.leftDistribMulAction {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] :
                      Equations
                      Equations
                      • TensorProduct.instDistribMulActionTensorProductToMonoidToMonoidWithZeroToSemiringAddMonoid = TensorProduct.leftDistribMulAction
                      theorem TensorProduct.smul_tmul' {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] (r : R') (m : M) (n : N) :
                      r m ⊗ₜ[R] n = (r m) ⊗ₜ[R] n
                      @[simp]
                      theorem TensorProduct.tmul_smul {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] [DistribMulAction R' N] [TensorProduct.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_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) (s : R) (m : M) (n : N) :
                      (r m) ⊗ₜ[R] (s n) = (r * s) m ⊗ₜ[R] n
                      noncomputable instance TensorProduct.leftModule {R : Type u_1} [CommSemiring R] {R'' : Type u_3} [Semiring R''] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module R'' M] [SMulCommClass R R'' M] :
                      Module R'' (TensorProduct R M N)
                      Equations
                      noncomputable instance TensorProduct.instModuleTensorProductToSemiringAddCommMonoid {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                      Equations
                      • TensorProduct.instModuleTensorProductToSemiringAddCommMonoid = TensorProduct.leftModule
                      noncomputable instance TensorProduct.smulCommClass_left {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] {R'₂ : Type u_10} [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)

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

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

                      Equations
                      • =
                      noncomputable instance TensorProduct.isScalarTower {R : Type u_1} [CommSemiring R] {R' : Type u_2} [Monoid R'] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DistribMulAction R' M] [SMulCommClass R R' M] [SMul R' R] [IsScalarTower R' R M] :

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

                      Equations
                      • =
                      noncomputable def TensorProduct.mk (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

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

                      Equations
                      Instances For
                        @[simp]
                        theorem TensorProduct.mk_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :
                        ((TensorProduct.mk R M N) m) n = m ⊗ₜ[R] n
                        theorem TensorProduct.ite_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [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_4} {N : Type u_5} [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.sum_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {α : Type u_10} (s : Finset α) (m : αM) (n : N) :
                        (Finset.sum s fun (a : α) => m a) ⊗ₜ[R] n = Finset.sum s fun (a : α) => m a ⊗ₜ[R] n
                        theorem TensorProduct.tmul_sum {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) {α : Type u_10} (s : Finset α) (n : αN) :
                        (m ⊗ₜ[R] Finset.sum s fun (a : α) => n a) = Finset.sum s fun (a : α) => m ⊗ₜ[R] n a
                        theorem TensorProduct.span_tmul_eq_top (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [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.

                        theorem TensorProduct.exists_eq_tmul_of_forall (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) (h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ (m : M) (n : N), m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n) :
                        ∃ (m : M) (n : N), x = m ⊗ₜ[R] n
                        noncomputable def TensorProduct.liftAux {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] 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
                        Instances For
                          theorem TensorProduct.liftAux_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
                          (TensorProduct.liftAux f) (m ⊗ₜ[R] n) = (f m) n
                          @[simp]
                          theorem TensorProduct.liftAux.smul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [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) :
                          noncomputable def TensorProduct.lift {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) :

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

                          Equations
                          Instances For
                            @[simp]
                            theorem TensorProduct.lift.tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :
                            (TensorProduct.lift f) (x ⊗ₜ[R] y) = (f x) y
                            @[simp]
                            theorem TensorProduct.lift.tmul' {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) :
                            (TensorProduct.lift f).toAddHom (x ⊗ₜ[R] y) = (f x) y
                            theorem TensorProduct.ext' {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g : TensorProduct R M N →ₗ[R] P} {h : TensorProduct R M N →ₗ[R] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) :
                            g = h
                            theorem TensorProduct.lift.unique {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} {g : TensorProduct R M N →ₗ[R] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f x) y) :
                            theorem TensorProduct.lift_mk {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                            theorem TensorProduct.lift_compr₂ {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                            theorem TensorProduct.ext {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g : TensorProduct R M N →ₗ[R] P} {h : TensorProduct R M N →ₗ[R] P} (H : LinearMap.compr₂ (TensorProduct.mk R M N) g = LinearMap.compr₂ (TensorProduct.mk R M N) h) :
                            g = h

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

                            See note [partially-applied ext lemmas].

                            noncomputable def TensorProduct.uncurry (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

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

                            Equations
                            Instances For
                              @[simp]
                              theorem TensorProduct.uncurry_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
                              ((TensorProduct.uncurry R M N P) f) (m ⊗ₜ[R] n) = (f m) n
                              noncomputable def TensorProduct.lift.equiv (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem TensorProduct.lift.equiv_apply (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
                                ((TensorProduct.lift.equiv R M N P) f) (m ⊗ₜ[R] n) = (f m) n
                                @[simp]
                                theorem TensorProduct.lift.equiv_symm_apply (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) :
                                (((LinearEquiv.symm (TensorProduct.lift.equiv R M N P)) f) m) n = f (m ⊗ₜ[R] n)
                                noncomputable def TensorProduct.lcurry (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

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

                                Equations
                                Instances For
                                  @[simp]
                                  theorem TensorProduct.lcurry_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) :
                                  (((TensorProduct.lcurry R M N P) f) m) n = f (m ⊗ₜ[R] n)
                                  noncomputable def TensorProduct.curry {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) :

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

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem TensorProduct.curry_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) :
                                    ((TensorProduct.curry f) m) n = f (m ⊗ₜ[R] n)
                                    theorem TensorProduct.curry_injective {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :
                                    Function.Injective TensorProduct.curry
                                    theorem TensorProduct.ext_threefold {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {g : TensorProduct R (TensorProduct R M N) P →ₗ[R] Q} {h : TensorProduct R (TensorProduct R M N) P →ₗ[R] Q} (H : ∀ (x : M) (y : N) (z : P), g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)) :
                                    g = h
                                    theorem TensorProduct.ext_fourfold {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] {g : TensorProduct R (TensorProduct R (TensorProduct R M N) P) Q →ₗ[R] S} {h : TensorProduct R (TensorProduct R (TensorProduct R M N) P) Q →ₗ[R] S} (H : ∀ (w : M) (x : N) (y : P) (z : Q), g (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = h (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)) :
                                    g = h
                                    theorem TensorProduct.ext_fourfold' {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] {φ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₗ[R] S} {ψ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₗ[R] S} (H : ∀ (w : M) (x : N) (y : P) (z : Q), φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)) :
                                    φ = ψ

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

                                    noncomputable def TensorProduct.lid (R : Type u_1) [CommSemiring R] (M : Type u_4) [AddCommMonoid M] [Module R M] :

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

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem TensorProduct.lid_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] (m : M) (r : R) :
                                      (TensorProduct.lid R M) (r ⊗ₜ[R] m) = r m
                                      @[simp]
                                      theorem TensorProduct.lid_symm_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] (m : M) :
                                      noncomputable def TensorProduct.comm (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

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

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem TensorProduct.comm_tmul (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :
                                        @[simp]
                                        theorem TensorProduct.comm_symm_tmul (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :
                                        theorem TensorProduct.lift_comp_comm_eq (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) :
                                        noncomputable def TensorProduct.rid (R : Type u_1) [CommSemiring R] (M : Type u_4) [AddCommMonoid M] [Module R M] :

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

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem TensorProduct.rid_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] (m : M) (r : R) :
                                          (TensorProduct.rid R M) (m ⊗ₜ[R] r) = r m
                                          @[simp]
                                          theorem TensorProduct.rid_symm_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] (m : M) :
                                          noncomputable def TensorProduct.assoc (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

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

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem TensorProduct.assoc_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) :
                                            (TensorProduct.assoc R M N P) ((m ⊗ₜ[R] n) ⊗ₜ[R] p) = m ⊗ₜ[R] n ⊗ₜ[R] p
                                            @[simp]
                                            theorem TensorProduct.assoc_symm_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) :
                                            noncomputable def TensorProduct.map {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :

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

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem TensorProduct.map_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) (m : M) (n : N) :
                                              (TensorProduct.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
                                              theorem TensorProduct.map_comp_comm_eq {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                              TensorProduct.map f g ∘ₗ (TensorProduct.comm R N M) = (TensorProduct.comm R Q P) ∘ₗ TensorProduct.map g f

                                              Given linear maps f : M → P, g : N → Q, if we identify M ⊗ N with N ⊗ M and P ⊗ Q with Q ⊗ P, then this lemma states that f ⊗ g = g ⊗ f.

                                              theorem TensorProduct.map_comm {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) (x : TensorProduct R N M) :
                                              theorem TensorProduct.map_map_comp_assoc_eq {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :

                                              Given linear maps f : M → Q, g : N → S, and h : P → T, if we identify (M ⊗ N) ⊗ P with M ⊗ (N ⊗ P) and (Q ⊗ S) ⊗ T with Q ⊗ (S ⊗ T), then this lemma states that f ⊗ (g ⊗ h) = (f ⊗ g) ⊗ h.

                                              theorem TensorProduct.map_map_assoc {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R (TensorProduct R M N) P) :
                                              theorem TensorProduct.map_map_comp_assoc_symm_eq {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :

                                              Given linear maps f : M → Q, g : N → S, and h : P → T, if we identify M ⊗ (N ⊗ P) with (M ⊗ N) ⊗ P and Q ⊗ (S ⊗ T) with (Q ⊗ S) ⊗ T, then this lemma states that (f ⊗ g) ⊗ h = f ⊗ (g ⊗ h).

                                              theorem TensorProduct.map_map_assoc_symm {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R M (TensorProduct R N P)) :
                                              theorem TensorProduct.map_range_eq_span_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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 (TensorProduct.map f g) = Submodule.span R {t : TensorProduct R P Q | ∃ (m : M) (n : N), f m ⊗ₜ[R] g n = t}
                                              noncomputable def TensorProduct.mapIncl {R : Type u_1} [CommSemiring R] {P : Type u_6} {Q : Type u_7} [AddCommMonoid P] [AddCommMonoid Q] [Module R P] [Module R Q] (p : Submodule R P) (q : Submodule R Q) :

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

                                              Equations
                                              Instances For
                                                theorem TensorProduct.map_comp {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {P' : Type u_10} {Q' : Type u_11} [AddCommMonoid P'] [Module R P'] [AddCommMonoid Q'] [Module R Q'] (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :
                                                TensorProduct.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = TensorProduct.map f₂ g₂ ∘ₗ TensorProduct.map f₁ g₁
                                                theorem TensorProduct.lift_comp_map {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {Q' : Type u_11} [AddCommMonoid Q'] [Module R Q'] (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
                                                @[simp]
                                                theorem TensorProduct.map_id {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                                                TensorProduct.map LinearMap.id LinearMap.id = LinearMap.id
                                                @[simp]
                                                theorem TensorProduct.map_one {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                                                theorem TensorProduct.map_mul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f₁ : M →ₗ[R] M) (f₂ : M →ₗ[R] M) (g₁ : N →ₗ[R] N) (g₂ : N →ₗ[R] N) :
                                                TensorProduct.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.map f₁ g₁ * TensorProduct.map f₂ g₂
                                                @[simp]
                                                theorem TensorProduct.map_pow {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ) :
                                                theorem TensorProduct.map_add_left {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f₁ : M →ₗ[R] P) (f₂ : M →ₗ[R] P) (g : N →ₗ[R] Q) :
                                                theorem TensorProduct.map_add_right {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) (g₂ : N →ₗ[R] Q) :
                                                theorem TensorProduct.map_smul_left {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
                                                theorem TensorProduct.map_smul_right {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
                                                noncomputable def TensorProduct.mapBilinear (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] :

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

                                                Equations
                                                Instances For
                                                  noncomputable def TensorProduct.lTensorHomToHomLTensor (R : Type u_1) [CommSemiring R] (M : Type u_4) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] :

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

                                                  Equations
                                                  Instances For
                                                    noncomputable def TensorProduct.rTensorHomToHomRTensor (R : Type u_1) [CommSemiring R] (M : Type u_4) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] :

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

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      noncomputable def TensorProduct.homTensorHomMap (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] :

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

                                                      Equations
                                                      Instances For
                                                        noncomputable def TensorProduct.map₂ {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) :

                                                        This is a binary version of TensorProduct.map: Given a bilinear map f : M ⟶ P ⟶ Q and a bilinear map g : N ⟶ S ⟶ T, if we think f and g as linear maps with two inputs, then map₂ f g is a bilinear map taking two inputs M ⊗ N → P ⊗ S → Q ⊗ S defined by map₂ f g (m ⊗ n) (p ⊗ s) = f m p ⊗ g n s.

                                                        Mathematically, TensorProduct.map₂ is defined as the composition M ⊗ N -map→ Hom(P, Q) ⊗ Hom(S, T) -homTensorHomMap→ Hom(P ⊗ S, Q ⊗ T).

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem TensorProduct.mapBilinear_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                                          @[simp]
                                                          theorem TensorProduct.lTensorHomToHomLTensor_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] (p : P) (f : M →ₗ[R] Q) (m : M) :
                                                          @[simp]
                                                          theorem TensorProduct.rTensorHomToHomRTensor_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] (f : M →ₗ[R] P) (q : Q) (m : M) :
                                                          @[simp]
                                                          theorem TensorProduct.homTensorHomMap_apply {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                                          @[simp]
                                                          theorem TensorProduct.map₂_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} {T : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T] (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) (m : M) (n : N) :
                                                          @[simp]
                                                          theorem TensorProduct.map_zero_left {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] Q) :
                                                          @[simp]
                                                          theorem TensorProduct.map_zero_right {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) :
                                                          noncomputable def TensorProduct.congr {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :

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

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem TensorProduct.congr_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) (m : M) (n : N) :
                                                            (TensorProduct.congr f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
                                                            @[simp]
                                                            theorem TensorProduct.congr_symm_tmul {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) (p : P) (q : Q) :
                                                            noncomputable def TensorProduct.leftComm (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

                                                            A tensor product analogue of mul_left_comm.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[simp]
                                                              theorem TensorProduct.leftComm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) :
                                                              @[simp]
                                                              theorem TensorProduct.leftComm_symm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (m : M) (n : N) (p : P) :
                                                              noncomputable def TensorProduct.tensorTensorTensorComm (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] :

                                                              This special case is worth defining explicitly since it is useful for defining multiplication on tensor products of modules carrying multiplications (e.g., associative rings, Lie rings, ...).

                                                              E.g., suppose M = P and N = Q and that M and N carry bilinear multiplications: M ⊗ M → M and N ⊗ N → N. Using map, we can define (M ⊗ M) ⊗ (N ⊗ N) → M ⊗ N which, when combined with this definition, yields a bilinear multiplication on M ⊗ N: (M ⊗ N) ⊗ (M ⊗ N) → M ⊗ N. In particular we could use this to define the multiplication in the TensorProduct.semiring instance (currently defined "by hand" using TensorProduct.mul).

                                                              See also mul_mul_mul_comm.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                theorem TensorProduct.tensorTensorTensorComm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (m : M) (n : N) (p : P) (q : Q) :
                                                                noncomputable def TensorProduct.tensorTensorTensorAssoc (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] :

                                                                This special case is useful for describing the interplay between dualTensorHomEquiv and composition of linear maps.

                                                                E.g., composition of linear maps gives a map (M → N) ⊗ (N → P) → (M → P), and applying dual_tensor_hom_equiv.symm to the three hom-modules gives a map (M.dual ⊗ N) ⊗ (N.dual ⊗ P) → (M.dual ⊗ P), which agrees with the application of contractRight on N ⊗ N.dual after the suitable rebracketting.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem TensorProduct.tensorTensorTensorAssoc_tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (m : M) (n : N) (p : P) (q : Q) :
                                                                  @[simp]
                                                                  theorem TensorProduct.tensorTensorTensorAssoc_symm_tmul (R : Type u_1) [CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (m : M) (n : N) (p : P) (q : Q) :
                                                                  noncomputable def LinearMap.lTensor {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) :

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

                                                                  Equations
                                                                  Instances For
                                                                    noncomputable def LinearMap.rTensor {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) :

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

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem LinearMap.lTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) (n : N) :
                                                                      (LinearMap.lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
                                                                      @[simp]
                                                                      theorem LinearMap.rTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) (n : N) :
                                                                      (LinearMap.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_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) :
                                                                      LinearMap.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_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) :
                                                                      theorem LinearMap.comm_comp_rTensor_comp_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] P) :
                                                                      (TensorProduct.comm R P Q) ∘ₗ LinearMap.rTensor Q g ∘ₗ (TensorProduct.comm R Q N) = LinearMap.lTensor Q g
                                                                      theorem LinearMap.comm_comp_lTensor_comp_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_5} {P : Type u_6} {Q : Type u_7} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] P) :
                                                                      (TensorProduct.comm R Q P) ∘ₗ LinearMap.lTensor Q g ∘ₗ (TensorProduct.comm R N Q) = LinearMap.rTensor Q g
                                                                      noncomputable def LinearMap.lTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

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

                                                                      Equations
                                                                      Instances For
                                                                        noncomputable def LinearMap.rTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :

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

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem LinearMap.coe_lTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :
                                                                          @[simp]
                                                                          theorem LinearMap.coe_rTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :
                                                                          @[simp]
                                                                          theorem LinearMap.lTensor_add {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (g : N →ₗ[R] P) :
                                                                          @[simp]
                                                                          theorem LinearMap.rTensor_add {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (g : N →ₗ[R] P) :
                                                                          @[simp]
                                                                          theorem LinearMap.lTensor_zero {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :
                                                                          @[simp]
                                                                          theorem LinearMap.rTensor_zero {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] :
                                                                          @[simp]
                                                                          theorem LinearMap.lTensor_smul {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (r : R) (f : N →ₗ[R] P) :
                                                                          @[simp]
                                                                          theorem LinearMap.rTensor_smul {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (r : R) (f : N →ₗ[R] P) :
                                                                          theorem LinearMap.lTensor_comp {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                                                          theorem LinearMap.lTensor_comp_apply {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                                                          (LinearMap.lTensor M (g ∘ₗ f)) x = (LinearMap.lTensor M g) ((LinearMap.lTensor M f) x)
                                                                          theorem LinearMap.rTensor_comp {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                                                          theorem LinearMap.rTensor_comp_apply {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                                                          (LinearMap.rTensor M (g ∘ₗ f)) x = (LinearMap.rTensor M g) ((LinearMap.rTensor M f) x)
                                                                          theorem LinearMap.lTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.End R N) (g : Module.End R N) :
                                                                          theorem LinearMap.rTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.End R N) (g : Module.End R N) :
                                                                          @[simp]
                                                                          theorem LinearMap.lTensor_id {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                                                                          LinearMap.lTensor M LinearMap.id = LinearMap.id
                                                                          theorem LinearMap.lTensor_id_apply {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) :
                                                                          (LinearMap.lTensor M LinearMap.id) x = x
                                                                          @[simp]
                                                                          theorem LinearMap.rTensor_id {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
                                                                          LinearMap.rTensor M LinearMap.id = LinearMap.id
                                                                          theorem LinearMap.rTensor_id_apply {R : Type u_1} [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R N M) :
                                                                          (LinearMap.rTensor M LinearMap.id) x = x
                                                                          theorem LinearMap.lid_comp_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N →ₗ[R] R) :
                                                                          @[simp]
                                                                          theorem LinearMap.lTensor_comp_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                                                          @[simp]
                                                                          theorem LinearMap.rTensor_comp_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} [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) :
                                                                          @[simp]
                                                                          theorem LinearMap.map_comp_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) :
                                                                          TensorProduct.map f g ∘ₗ LinearMap.rTensor N f' = TensorProduct.map (f ∘ₗ f') g
                                                                          @[simp]
                                                                          theorem LinearMap.map_comp_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) :
                                                                          TensorProduct.map f g ∘ₗ LinearMap.lTensor M g' = TensorProduct.map f (g ∘ₗ g')
                                                                          @[simp]
                                                                          theorem LinearMap.rTensor_comp_map {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
                                                                          LinearMap.rTensor Q f' ∘ₗ TensorProduct.map f g = TensorProduct.map (f' ∘ₗ f) g
                                                                          @[simp]
                                                                          theorem LinearMap.lTensor_comp_map {R : Type u_1} [CommSemiring R] (M : Type u_4) {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
                                                                          LinearMap.lTensor P g' ∘ₗ TensorProduct.map f g = TensorProduct.map f (g' ∘ₗ g)
                                                                          @[simp]
                                                                          theorem LinearMap.rTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] M) (n : ) :
                                                                          @[simp]
                                                                          theorem LinearMap.lTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N →ₗ[R] N) (n : ) :
                                                                          noncomputable def TensorProduct.Neg.aux (R : Type u_1) [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] :

                                                                          Auxiliary function to defining negation multiplication on tensor product.

                                                                          Equations
                                                                          Instances For
                                                                            noncomputable instance TensorProduct.neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] :
                                                                            Equations
                                                                            theorem TensorProduct.add_left_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (x : TensorProduct R M N) :
                                                                            -x + x = 0
                                                                            noncomputable instance TensorProduct.addCommGroup {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] :
                                                                            Equations
                                                                            • TensorProduct.addCommGroup = let __src := TensorProduct.addCommMonoid; AddCommGroup.mk
                                                                            theorem TensorProduct.neg_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m : M) (n : N) :
                                                                            (-m) ⊗ₜ[R] n = -m ⊗ₜ[R] n
                                                                            theorem TensorProduct.tmul_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m : M) (n : N) :
                                                                            m ⊗ₜ[R] (-n) = -m ⊗ₜ[R] n
                                                                            theorem TensorProduct.tmul_sub {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m : M) (n₁ : N) (n₂ : N) :
                                                                            m ⊗ₜ[R] (n₁ - n₂) = m ⊗ₜ[R] n₁ - m ⊗ₜ[R] n₂
                                                                            theorem TensorProduct.sub_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (m₁ : M) (m₂ : M) (n : N) :
                                                                            (m₁ - m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n
                                                                            noncomputable instance TensorProduct.CompatibleSMul.int {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] :

                                                                            While the tensor product will automatically inherit a ℤ-module structure from AddCommGroup.intModule, 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.

                                                                            Equations
                                                                            • =
                                                                            noncomputable instance TensorProduct.CompatibleSMul.unit {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {S : Type u_7} [Monoid S] [DistribMulAction S M] [DistribMulAction S N] [TensorProduct.CompatibleSMul R S M N] :
                                                                            Equations
                                                                            • =
                                                                            @[simp]
                                                                            theorem LinearMap.lTensor_sub {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (g : N →ₗ[R] P) :
                                                                            @[simp]
                                                                            theorem LinearMap.rTensor_sub {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (g : N →ₗ[R] P) :
                                                                            @[simp]
                                                                            theorem LinearMap.lTensor_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) :
                                                                            @[simp]
                                                                            theorem LinearMap.rTensor_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) :