Documentation

Mathlib.LinearAlgebra.TensorProduct.Tower

The A-module structure on M ⊗[R] N #

When M is both an R-module and an A-module, and Algebra R A, then many of the morphisms preserve the actions by A.

The Module instance itself is provided elsewhere as TensorProduct.leftModule. This file provides more general versions of the definitions already in LinearAlgebra/TensorProduct.

In this file, we use the convention that M, N, P, Q are all R-modules, but only M and P are simultaneously A-modules.

Main definitions #

Implementation notes #

We could thus consider replacing the less general definitions with these ones. If we do this, we probably should still implement the less general ones as abbreviations to the more general ones with fewer type arguments.

source
theorem TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (a : A) (x : TensorProduct R M N) :
a • x = ↑(LinearMap.rTensor N (↑(Algebra.lsmul R R M) a)) x
source
@[simp]
theorem TensorProduct.AlgebraTensorModule.curry_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N →ₗ[A] P) (a : M) :
↑(TensorProduct.AlgebraTensorModule.curry f) a = ↑(TensorProduct.curry (↑R f)) a
source
def TensorProduct.AlgebraTensorModule.curry {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N →ₗ[A] P) :
M →ₗ[A] N →ₗ[R] P

Heterobasic version of TensorProduct.curry:

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

Instances For
    source
    theorem TensorProduct.AlgebraTensorModule.restrictScalars_curry {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N →ₗ[A] P) :
    ↑R (TensorProduct.AlgebraTensorModule.curry f) = TensorProduct.curry (↑R f)
    source
    theorem TensorProduct.AlgebraTensorModule.curry_injective {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] :
    Function.Injective TensorProduct.AlgebraTensorModule.curry

    Just as TensorProduct.ext is marked ext instead of TensorProduct.ext', this is a better ext lemma than TensorProduct.AlgebraTensorModule.ext below.

    See note [partially-applied ext lemmas].

    source
    theorem TensorProduct.AlgebraTensorModule.ext {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] {g : TensorProduct R M N →ₗ[A] P} {h : TensorProduct R M N →ₗ[A] P} (H : ∀ (x : M) (y : N), ↑g (x ⊗ₜ[R] y) = ↑h (x ⊗ₜ[R] y)) :
    g = h
    source
    def TensorProduct.AlgebraTensorModule.lift {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] N →ₗ[R] P) :
    TensorProduct R M N →ₗ[A] P

    Heterobasic version of TensorProduct.lift:

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

    Instances For
      source
      @[simp]
      theorem TensorProduct.AlgebraTensorModule.lift_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] N →ₗ[R] P) (a : TensorProduct R M N) :
      ↑(TensorProduct.AlgebraTensorModule.lift f) a = ↑(TensorProduct.lift (↑R f)) a
      source
      @[simp]
      theorem TensorProduct.AlgebraTensorModule.lift_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) :
      ↑(TensorProduct.AlgebraTensorModule.lift f) (x ⊗ₜ[R] y) = ↑(↑f x) y
      source
      @[simp]
      theorem TensorProduct.AlgebraTensorModule.uncurry_apply (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] N →ₗ[R] P) :
      ↑(TensorProduct.AlgebraTensorModule.uncurry R A B M N P) f = TensorProduct.AlgebraTensorModule.lift f
      source
      def TensorProduct.AlgebraTensorModule.uncurry (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] :
      (M →ₗ[A] N →ₗ[R] P) →ₗ[B] TensorProduct R M N →ₗ[A] P

      Heterobasic version of TensorProduct.uncurry:

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

      Instances For
        source
        @[simp]
        theorem TensorProduct.AlgebraTensorModule.lcurry_apply (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] (f : TensorProduct R M N →ₗ[A] P) :
        ↑(TensorProduct.AlgebraTensorModule.lcurry R A B M N P) f = TensorProduct.AlgebraTensorModule.curry f
        source
        def TensorProduct.AlgebraTensorModule.lcurry (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] :
        (TensorProduct R M N →ₗ[A] P) →ₗ[B] M →ₗ[A] N →ₗ[R] P

        Heterobasic version of TensorProduct.lcurry:

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

        Instances For
          source
          def TensorProduct.AlgebraTensorModule.lift.equiv (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] :
          (M →ₗ[A] N →ₗ[R] P) ≃ₗ[B] TensorProduct R M N →ₗ[A] P

          Heterobasic version of TensorProduct.lift.equiv:

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

          Instances For
            source
            @[simp]
            theorem TensorProduct.AlgebraTensorModule.mk_apply (R : Type uR) (A : Type uA) (M : Type uM) (N : Type uN) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (m : M) :
            ↑(TensorProduct.AlgebraTensorModule.mk R A M N) m = { toAddHom := { toFun := fun x => m ⊗ₜ[R] x, map_add' := (_ : ∀ (n₁ n₂ : N), m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂) }, map_smul' := (_ : ∀ (c : R) (y : N), m ⊗ₜ[R] (c • y) = c • m ⊗ₜ[R] y) }
            source
            def TensorProduct.AlgebraTensorModule.mk (R : Type uR) (A : Type uA) (M : Type uM) (N : Type uN) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
            M →ₗ[A] N →ₗ[R] TensorProduct R M N

            Heterobasic version of TensorProduct.mk:

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

            Instances For
              source
              def TensorProduct.AlgebraTensorModule.map {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) :
              TensorProduct R M N →ₗ[A] TensorProduct R P Q

              Heterobasic version of TensorProduct.map

              Instances For
                source
                @[simp]
                theorem TensorProduct.AlgebraTensorModule.map_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) :
                ↑(TensorProduct.AlgebraTensorModule.map f g) (m ⊗ₜ[R] n) = ↑f m ⊗ₜ[R] ↑g n
                source
                @[simp]
                theorem TensorProduct.AlgebraTensorModule.map_id {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                TensorProduct.AlgebraTensorModule.map LinearMap.id LinearMap.id = LinearMap.id
                source
                theorem TensorProduct.AlgebraTensorModule.map_comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] [AddCommMonoid Q'] [Module R Q'] (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :
                TensorProduct.AlgebraTensorModule.map (LinearMap.comp f₂ f₁) (LinearMap.comp g₂ g₁) = LinearMap.comp (TensorProduct.AlgebraTensorModule.map f₂ g₂) (TensorProduct.AlgebraTensorModule.map f₁ g₁)
                source
                @[simp]
                theorem TensorProduct.AlgebraTensorModule.map_one {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                TensorProduct.AlgebraTensorModule.map 1 1 = 1
                source
                theorem TensorProduct.AlgebraTensorModule.map_mul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (f₁ : M →ₗ[A] M) (f₂ : M →ₗ[A] M) (g₁ : N →ₗ[R] N) (g₂ : N →ₗ[R] N) :
                TensorProduct.AlgebraTensorModule.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.AlgebraTensorModule.map f₁ g₁ * TensorProduct.AlgebraTensorModule.map f₂ g₂
                source
                theorem TensorProduct.AlgebraTensorModule.map_add_left {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f₁ : M →ₗ[A] P) (f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) :
                TensorProduct.AlgebraTensorModule.map (f₁ + f₂) g = TensorProduct.AlgebraTensorModule.map f₁ g + TensorProduct.AlgebraTensorModule.map f₂ g
                source
                theorem TensorProduct.AlgebraTensorModule.map_add_right {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g₁ : N →ₗ[R] Q) (g₂ : N →ₗ[R] Q) :
                TensorProduct.AlgebraTensorModule.map f (g₁ + g₂) = TensorProduct.AlgebraTensorModule.map f g₁ + TensorProduct.AlgebraTensorModule.map f g₂
                source
                theorem TensorProduct.AlgebraTensorModule.map_smul_right {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) :
                TensorProduct.AlgebraTensorModule.map f (r • g) = r • TensorProduct.AlgebraTensorModule.map f g
                source
                theorem TensorProduct.AlgebraTensorModule.map_smul_left {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] [AddCommMonoid Q] [Module R Q] (b : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) :
                TensorProduct.AlgebraTensorModule.map (b • f) g = b • TensorProduct.AlgebraTensorModule.map f g
                source
                def TensorProduct.AlgebraTensorModule.mapBilinear (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] [AddCommMonoid Q] [Module R Q] :
                (M →ₗ[A] P) →ₗ[B] (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R P Q

                Heterobasic version of TensorProduct.map_bilinear

                Instances For
                  source
                  @[simp]
                  theorem TensorProduct.AlgebraTensorModule.mapBilinear_apply {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) :
                  ↑(↑(TensorProduct.AlgebraTensorModule.mapBilinear R A B M N P Q) f) g = TensorProduct.AlgebraTensorModule.map f g
                  source
                  def TensorProduct.AlgebraTensorModule.homTensorHomMap (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] [AddCommMonoid Q] [Module R Q] :
                  TensorProduct R (M →ₗ[A] P) (N →ₗ[R] Q) →ₗ[B] TensorProduct R M N →ₗ[A] TensorProduct R P Q

                  Heterobasic version of TensorProduct.homTensorHomMap

                  Instances For
                    source
                    @[simp]
                    theorem TensorProduct.AlgebraTensorModule.homTensorHomMap_apply {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [Module B P] [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) :
                    ↑(TensorProduct.AlgebraTensorModule.homTensorHomMap R A B M N P Q) (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g
                    source
                    def TensorProduct.AlgebraTensorModule.congr {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) :
                    TensorProduct R M N ≃ₗ[A] TensorProduct R P Q

                    Heterobasic version of TensorProduct.congr

                    Instances For
                      source
                      @[simp]
                      theorem TensorProduct.AlgebraTensorModule.congr_refl {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                      TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl A M) (LinearEquiv.refl R N) = LinearEquiv.refl A (TensorProduct R M N)
                      source
                      theorem TensorProduct.AlgebraTensorModule.congr_trans {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] [AddCommMonoid Q'] [Module R Q'] (f₁ : M ≃ₗ[A] P) (f₂ : P ≃ₗ[A] P') (g₁ : N ≃ₗ[R] Q) (g₂ : Q ≃ₗ[R] Q') :
                      TensorProduct.AlgebraTensorModule.congr (LinearEquiv.trans f₁ f₂) (LinearEquiv.trans g₁ g₂) = LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr f₁ g₁) (TensorProduct.AlgebraTensorModule.congr f₂ g₂)
                      source
                      theorem TensorProduct.AlgebraTensorModule.congr_symm {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) :
                      TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm f) (LinearEquiv.symm g) = LinearEquiv.symm (TensorProduct.AlgebraTensorModule.congr f g)
                      source
                      @[simp]
                      theorem TensorProduct.AlgebraTensorModule.congr_one {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] :
                      TensorProduct.AlgebraTensorModule.congr 1 1 = 1
                      source
                      theorem TensorProduct.AlgebraTensorModule.congr_mul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (f₁ : M ≃ₗ[A] M) (f₂ : M ≃ₗ[A] M) (g₁ : N ≃ₗ[R] N) (g₂ : N ≃ₗ[R] N) :
                      TensorProduct.AlgebraTensorModule.congr (f₁ * f₂) (g₁ * g₂) = TensorProduct.AlgebraTensorModule.congr f₁ g₁ * TensorProduct.AlgebraTensorModule.congr f₂ g₂
                      source
                      @[simp]
                      theorem TensorProduct.AlgebraTensorModule.congr_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) :
                      ↑(TensorProduct.AlgebraTensorModule.congr f g) (m ⊗ₜ[R] n) = ↑f m ⊗ₜ[R] ↑g n
                      source
                      @[simp]
                      theorem TensorProduct.AlgebraTensorModule.congr_symm_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) :
                      ↑(LinearEquiv.symm (TensorProduct.AlgebraTensorModule.congr f g)) (p ⊗ₜ[R] q) = ↑(LinearEquiv.symm f) p ⊗ₜ[R] ↑(LinearEquiv.symm g) q
                      source
                      def TensorProduct.AlgebraTensorModule.rid (R : Type uR) (A : Type uA) (M : Type uM) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] :
                      TensorProduct R M R ≃ₗ[A] M

                      Heterobasic version of TensorProduct.rid.

                      Instances For
                        source
                        @[simp]
                        theorem TensorProduct.AlgebraTensorModule.rid_tmul {R : Type uR} (A : Type uA) {M : Type uM} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (r : R) (m : M) :
                        ↑(TensorProduct.AlgebraTensorModule.rid R A M) (m ⊗ₜ[R] r) = r • m
                        source
                        def TensorProduct.AlgebraTensorModule.assoc (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (P : Type uP) (Q : Type uQ) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Algebra A B] [IsScalarTower A B M] :
                        TensorProduct R (TensorProduct A M P) Q ≃ₗ[B] TensorProduct A M (TensorProduct R P Q)

                        Heterobasic version of TensorProduct.assoc:

                        Linear equivalence between (M ⊗[A] N) ⊗[R] P and M ⊗[A] (N ⊗[R] P).

                        Note this is especially useful with A = R (where it is a "more linear" version of TensorProduct.assoc), or with B = A.

                        Instances For
                          source
                          @[simp]
                          theorem TensorProduct.AlgebraTensorModule.assoc_tmul (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Algebra A B] [IsScalarTower A B M] (m : M) (p : P) (q : Q) :
                          ↑(TensorProduct.AlgebraTensorModule.assoc R A B M P Q) ((m ⊗ₜ[A] p) ⊗ₜ[R] q) = m ⊗ₜ[A] p ⊗ₜ[R] q
                          source
                          @[simp]
                          theorem TensorProduct.AlgebraTensorModule.assoc_symm_tmul (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Algebra A B] [IsScalarTower A B M] (m : M) (p : P) (q : Q) :
                          ↑(LinearEquiv.symm (TensorProduct.AlgebraTensorModule.assoc R A B M P Q)) (m ⊗ₜ[A] p ⊗ₜ[R] q) = (m ⊗ₜ[A] p) ⊗ₜ[R] q
                          source
                          def TensorProduct.AlgebraTensorModule.leftComm (R : Type uR) (A : Type uA) (M : Type uM) (P : Type uP) (Q : Type uQ) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] :
                          TensorProduct A M (TensorProduct R P Q) ≃ₗ[A] TensorProduct A P (TensorProduct R M Q)

                          Heterobasic version of TensorProduct.leftComm

                          Instances For
                            source
                            @[simp]
                            theorem TensorProduct.AlgebraTensorModule.leftComm_tmul (R : Type uR) (A : Type uA) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (m : M) (p : P) (q : Q) :
                            ↑(TensorProduct.AlgebraTensorModule.leftComm R A M P Q) (m ⊗ₜ[A] p ⊗ₜ[R] q) = p ⊗ₜ[A] m ⊗ₜ[R] q
                            source
                            @[simp]
                            theorem TensorProduct.AlgebraTensorModule.leftComm_symm_tmul (R : Type uR) (A : Type uA) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (m : M) (p : P) (q : Q) :
                            ↑(LinearEquiv.symm (TensorProduct.AlgebraTensorModule.leftComm R A M P Q)) (p ⊗ₜ[A] m ⊗ₜ[R] q) = m ⊗ₜ[A] p ⊗ₜ[R] q
                            source
                            def TensorProduct.AlgebraTensorModule.rightComm (R : Type uR) (A : Type uA) (M : Type uM) (P : Type uP) (Q : Type uQ) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] :
                            TensorProduct R (TensorProduct A M P) Q ≃ₗ[A] TensorProduct A (TensorProduct R M Q) P

                            A tensor product analogue of mul_right_comm.

                            Instances For
                              source
                              @[simp]
                              theorem TensorProduct.AlgebraTensorModule.rightComm_tmul (R : Type uR) (A : Type uA) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] (m : M) (p : P) (q : Q) :
                              ↑(TensorProduct.AlgebraTensorModule.rightComm R A M P Q) ((m ⊗ₜ[A] p) ⊗ₜ[R] q) = (m ⊗ₜ[R] q) ⊗ₜ[A] p
                              source
                              @[simp]
                              theorem TensorProduct.AlgebraTensorModule.rightComm_symm_tmul (R : Type uR) (A : Type uA) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] (m : M) (p : P) (q : Q) :
                              ↑(LinearEquiv.symm (TensorProduct.AlgebraTensorModule.rightComm R A M P Q)) ((m ⊗ₜ[R] q) ⊗ₜ[A] p) = (m ⊗ₜ[A] p) ⊗ₜ[R] q
                              source
                              def TensorProduct.AlgebraTensorModule.tensorTensorTensorComm (R : Type uR) (A : Type uA) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] :
                              TensorProduct A (TensorProduct R M N) (TensorProduct R P Q) ≃ₗ[A] TensorProduct R (TensorProduct A M P) (TensorProduct R N Q)

                              Heterobasic version of tensorTensorTensorComm.

                              Instances For
                                source
                                @[simp]
                                theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (m : M) (n : N) (p : P) (q : Q) :
                                ↑(TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M N P Q) ((m ⊗ₜ[R] n) ⊗ₜ[A] p ⊗ₜ[R] q) = (m ⊗ₜ[A] p) ⊗ₜ[R] n ⊗ₜ[R] q
                                source
                                @[simp]
                                theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (m : M) (n : N) (p : P) (q : Q) :
                                ↑(LinearEquiv.symm (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M N P Q)) ((m ⊗ₜ[A] p) ⊗ₜ[R] n ⊗ₜ[R] q) = (m ⊗ₜ[R] n) ⊗ₜ[A] p ⊗ₜ[R] q