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.

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

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.

Equations
Instances For
    @[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) :
    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].

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

    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.

    Equations
    Instances For
      @[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) :
      @[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) :
      noncomputable 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] :

      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.

      Equations
      Instances For
        @[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) :
        noncomputable 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] :

        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.

        Equations
        Instances For
          @[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) :
          noncomputable 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] :

          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.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            noncomputable 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] :

            Heterobasic version of TensorProduct.mk:

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

            Equations
            Instances For
              @[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 = { toFun := fun (x : N) => m ⊗ₜ[R] x, map_add' := , map_smul' := }
              noncomputable 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) :

              Heterobasic version of TensorProduct.map

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[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) :
                @[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
                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) :
                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) :
                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) :
                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) :
                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) :
                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) :
                noncomputable 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] :

                Heterobasic version of TensorProduct.map_bilinear

                Equations
                Instances For
                  @[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) :
                  noncomputable 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] :

                  Heterobasic version of TensorProduct.homTensorHomMap

                  Equations
                  Instances For
                    @[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) :
                    noncomputable 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) :

                    Heterobasic version of TensorProduct.congr

                    Equations
                    Instances For
                      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') :
                      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) :
                      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) :
                      @[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) :
                      @[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) :
                      (TensorProduct.AlgebraTensorModule.congr f g).symm (p ⊗ₜ[R] q) = f.symm p ⊗ₜ[R] g.symm q
                      noncomputable 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] :

                      Heterobasic version of TensorProduct.rid.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[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) :
                        @[simp]
                        theorem TensorProduct.AlgebraTensorModule.rid_symm_apply (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] (m : M) :
                        noncomputable 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] :

                        Heterobasic version of TensorProduct.assoc:

                        B-linear equivalence between (M ⊗[A] P) ⊗[R] Q and M ⊗[A] (P ⊗[R] Q).

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[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) :
                          @[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) :
                          noncomputable def TensorProduct.AlgebraTensorModule.cancelBaseChange (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) [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 N] [Module R N] [Algebra A B] [IsScalarTower A B M] :

                          B-linear equivalence between M ⊗[A] (A ⊗[R] N) and M ⊗[R] N. In particular useful with B = A.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} [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 N] [Module R N] [Algebra A B] [IsScalarTower A B M] (m : M) (n : N) (a : A) :
                            @[simp]
                            theorem TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} [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 N] [Module R N] [Algebra A B] [IsScalarTower A B M] (m : M) (n : N) :
                            noncomputable 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] :

                            Heterobasic version of TensorProduct.leftComm

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[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) :
                              @[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) :
                              noncomputable 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] :

                              A tensor product analogue of mul_right_comm.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[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) :
                                @[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) :
                                noncomputable 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] :

                                Heterobasic version of tensorTensorTensorComm.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[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) :
                                  @[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) :
                                  noncomputable def Submodule.baseChange {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

                                  If A is an R-algebra, any R-submodule p of an R-module M may be pushed forward to an A-submodule of A ⊗ M.

                                  This "base change" operation is also known as "extension of scalars".

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Submodule.baseChange_bot {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
                                    @[simp]
                                    theorem Submodule.baseChange_top {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
                                    theorem Submodule.tmul_mem_baseChange_of_mem {R : Type u_1} {M : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] {p : Submodule R M} (a : A) {m : M} (hm : m p) :
                                    @[simp]
                                    theorem Submodule.baseChange_span {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (s : Set M) :