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

• TensorProduct.AlgebraTensorModule.curry
• TensorProduct.AlgebraTensorModule.uncurry
• TensorProduct.AlgebraTensorModule.lcurry
• TensorProduct.AlgebraTensorModule.lift
• TensorProduct.AlgebraTensorModule.lift.equiv
• TensorProduct.AlgebraTensorModule.mk
• TensorProduct.AlgebraTensorModule.map
• TensorProduct.AlgebraTensorModule.mapBilinear
• TensorProduct.AlgebraTensorModule.congr
• TensorProduct.AlgebraTensorModule.rid
• TensorProduct.AlgebraTensorModule.homTensorHomMap
• TensorProduct.AlgebraTensorModule.assoc
• TensorProduct.AlgebraTensorModule.leftComm
• TensorProduct.AlgebraTensorModule.rightComm
• TensorProduct.AlgebraTensorModule.tensorTensorTensorComm
• LinearMap.baseChange A f is the A-linear map A ⊗ f, for an R-linear map f.

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

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.

@[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) : (curry f) a = (TensorProduct.curry (↑R f)) a

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 (curry f) = TensorProduct.curry (↑R f)

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 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.curry_injective_iff {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] {a₁ a₂ : TensorProduct R M N →ₗ[A] P} : a₁ = a₂ ↔ curry a₁ = curry a₂

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 h : TensorProduct R M N →ₗ[A] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) : g = h

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.

@[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) : (lift f) a = (TensorProduct.lift (↑R f)) a

@[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) : (lift f) (x ⊗ₜ[R] y) = (f x) y

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] [IsScalarTower R A P] [Module B 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.

@[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] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] N →ₗ[R] P) : (uncurry R A B M N P) f = lift f

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] [IsScalarTower R A P] [Module B 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.

@[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] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : TensorProduct R M N →ₗ[A] P) : (lcurry R A B M N P) f = curry f

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] [IsScalarTower R A P] [Module B 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.

def TensorProduct.AlgebraTensorModule.mk (R : Type uR) [CommSemiring R] (A : Type u_1) (M : Type u_2) (N : Type u_3) [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMulCommClass 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.

@[simp]

theorem TensorProduct.AlgebraTensorModule.mk_apply (R : Type uR) [CommSemiring R] (A : Type u_1) (M : Type u_2) (N : Type u_3) [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMulCommClass R A M] [AddCommMonoid N] [Module R N] (m : M) : (mk R A M N) m = { toFun := fun (x2 : N) => m ⊗ₜ[R] x2, map_add' := ⋯, map_smul' := ⋯ }

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

@[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) : (map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g 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] : 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) : map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = map f₂ g₂ ∘ₗ map f₁ g₁

@[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] : map 1 1 = 1

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₁ f₂ : M →ₗ[A] M) (g₁ g₂ : N →ₗ[R] N) : map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂

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₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (f₁ + f₂) g = map f₁ g + map f₂ g

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₁ g₂ : N →ₗ[R] Q) : map f (g₁ + g₂) = map f g₁ + map f g₂

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) : map f (r • g) = r • map f g

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] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (b : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (b • f) g = b • map f g

theorem TensorProduct.AlgebraTensorModule.map_eq {R : Type uR} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map f g = TensorProduct.map f g

The heterobasic version of map coincides with the regular version.

def TensorProduct.AlgebraTensorModule.lTensor {R : Type uR} (A : Type uA) (M : Type uM) {N : Type uN} {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 Q] [Module R Q] : (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R M Q

Heterobasic version of LinearMap.lTensor

@[simp]

theorem TensorProduct.AlgebraTensorModule.coe_lTensor {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {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 Q] [Module R Q] (f : N →ₗ[R] Q) : ⇑((lTensor A M) f) = ⇑(LinearMap.lTensor M f)

@[simp]

theorem TensorProduct.AlgebraTensorModule.restrictScalars_lTensor {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {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 Q] [Module R Q] (f : N →ₗ[R] Q) : ↑R ((lTensor A M) f) = LinearMap.lTensor M f

@[simp]

theorem TensorProduct.AlgebraTensorModule.lTensor_tmul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {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 Q] [Module R Q] (f : N →ₗ[R] Q) (m : M) (n : N) : ((lTensor A M) f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n

@[simp]

theorem TensorProduct.AlgebraTensorModule.lTensor_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] : (lTensor A M) LinearMap.id = LinearMap.id

theorem TensorProduct.AlgebraTensorModule.lTensor_comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} {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 Q] [Module R Q] [AddCommMonoid Q'] [Module R Q'] (f₂ : Q →ₗ[R] Q') (f₁ : N →ₗ[R] Q) : (lTensor A M) (f₂ ∘ₗ f₁) = (lTensor A M) f₂ ∘ₗ (lTensor A M) f₁

@[simp]

theorem TensorProduct.AlgebraTensorModule.lTensor_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] : (lTensor A M) 1 = 1

theorem TensorProduct.AlgebraTensorModule.lTensor_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₁ f₂ : N →ₗ[R] N) : (lTensor A M) (f₁ * f₂) = (lTensor A M) f₁ * (lTensor A M) f₂

def TensorProduct.AlgebraTensorModule.rTensor (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] : (M →ₗ[A] P) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R P N

Heterobasic version of LinearMap.rTensor

@[simp]

theorem TensorProduct.AlgebraTensorModule.coe_rTensor {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] P) : ⇑((rTensor R N) f) = ⇑(LinearMap.rTensor N (↑R f))

@[simp]

theorem TensorProduct.AlgebraTensorModule.restrictScalars_rTensor {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] P) : ↑R ((rTensor R N) f) = LinearMap.rTensor N (↑R f)

@[simp]

theorem TensorProduct.AlgebraTensorModule.rTensor_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] P) (m : M) (n : N) : ((rTensor R N) f) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] n

@[simp]

theorem TensorProduct.AlgebraTensorModule.rTensor_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] : (rTensor R N) LinearMap.id = LinearMap.id

theorem TensorProduct.AlgebraTensorModule.rTensor_comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {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] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) : (rTensor R N) (f₂ ∘ₗ f₁) = (rTensor R N) f₂ ∘ₗ (rTensor R N) f₁

@[simp]

theorem TensorProduct.AlgebraTensorModule.rTensor_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] : (rTensor R N) 1 = 1

theorem TensorProduct.AlgebraTensorModule.rTensor_mul {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] (f₁ f₂ : M →ₗ[A] M) : (rTensor R M) (f₁ * f₂) = (rTensor R M) f₁ * (rTensor R M) f₂

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] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] : (M →ₗ[A] P) →ₗ[B] (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R P Q

Heterobasic version of TensorProduct.map_bilinear

@[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] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : ((mapBilinear R A B M N P Q) f) g = map f g

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] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] : TensorProduct R (M →ₗ[A] P) (N →ₗ[R] Q) →ₗ[B] TensorProduct R M N →ₗ[A] TensorProduct R P Q

Heterobasic version of TensorProduct.homTensorHomMap

@[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] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : (homTensorHomMap R A B M N P Q) (f ⊗ₜ[R] g) = map f g

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

@[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] : congr (LinearEquiv.refl A M) (LinearEquiv.refl R N) = LinearEquiv.refl A (TensorProduct R M N)

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') : congr (f₁ ≪≫ₗ f₂) (g₁ ≪≫ₗ g₂) = congr f₁ g₁ ≪≫ₗ congr f₂ g₂

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) : congr f.symm g.symm = (congr f g).symm

@[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] : congr 1 1 = 1

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₁ f₂ : M ≃ₗ[A] M) (g₁ g₂ : N ≃ₗ[R] N) : congr (f₁ * f₂) (g₁ * g₂) = congr f₁ g₁ * congr f₂ g₂

@[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) : (congr f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g 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) : (congr f g).symm (p ⊗ₜ[R] q) = f.symm p ⊗ₜ[R] g.symm q

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.

theorem TensorProduct.AlgebraTensorModule.rid_eq_rid (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : AlgebraTensorModule.rid R R M = TensorProduct.rid R M

The heterobasic version of rid coincides with the regular version.

@[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) : (AlgebraTensorModule.rid R A M) (m ⊗ₜ[R] r) = r • 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) : (AlgebraTensorModule.rid R A M).symm m = m ⊗ₜ[R] 1

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 A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [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:

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.

@[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 A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] (m : M) (p : P) (q : Q) : (assoc R A B M P Q) (m ⊗ₜ[A] p ⊗ₜ[R] q) = m ⊗ₜ[A] (p ⊗ₜ[R] 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 A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] (m : M) (p : P) (q : Q) : (assoc R A B M P Q).symm (m ⊗ₜ[A] (p ⊗ₜ[R] q)) = m ⊗ₜ[A] p ⊗ₜ[R] q

theorem TensorProduct.AlgebraTensorModule.assoc_eq (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] : assoc R R R M P Q = TensorProduct.assoc R M P Q

The heterobasic version of assoc coincides with the regular version.

theorem TensorProduct.AlgebraTensorModule.rTensor_tensor (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} {P : Type uP} (P' : Type uP') [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 A P] [AddCommMonoid P'] [Module A P'] [Module R P] [IsScalarTower R A P] [Module R P'] [IsScalarTower R A P'] (g : P →ₗ[A] P') : LinearMap.rTensor (TensorProduct R M N) g = ↑(assoc R A A P' M N) ∘ₗ map (LinearMap.rTensor M g) LinearMap.id ∘ₗ ↑(assoc R A A P M N).symm

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] : TensorProduct A M (TensorProduct R A N) ≃ₗ[B] TensorProduct R M N

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

def TensorProduct.AlgebraTensorModule.distribBaseChange (R : Type uR) (A : Type uA) (M : Type uM) (N : Type uN) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : TensorProduct R A (TensorProduct R M N) ≃ₗ[A] TensorProduct A (TensorProduct R A M) (TensorProduct R A N)

Base change distributes over tensor product.

@[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) : (cancelBaseChange R A B M N) (m ⊗ₜ[A] (a ⊗ₜ[R] n)) = (a • m) ⊗ₜ[R] n

@[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) : (cancelBaseChange R A B M N).symm (m ⊗ₜ[R] n) = m ⊗ₜ[A] (1 ⊗ₜ[R] n)

theorem TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {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 N] [Module R N] [AddCommMonoid Q] [Module R Q] [Algebra A B] [IsScalarTower A B M] (f : N →ₗ[R] Q) : (lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N) = ↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f)

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 A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] : TensorProduct A M (TensorProduct R P Q) ≃ₗ[A] TensorProduct A P (TensorProduct R M Q)

Heterobasic version of TensorProduct.leftComm

@[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 A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] (m : M) (p : P) (q : Q) : (leftComm R A M P Q) (m ⊗ₜ[A] (p ⊗ₜ[R] q)) = p ⊗ₜ[A] (m ⊗ₜ[R] 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 A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] (m : M) (p : P) (q : Q) : (leftComm R A M P Q).symm (p ⊗ₜ[A] (m ⊗ₜ[R] q)) = m ⊗ₜ[A] (p ⊗ₜ[R] q)

theorem TensorProduct.AlgebraTensorModule.leftComm_eq (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] : leftComm R R M P Q = TensorProduct.leftComm R M P Q

The heterobasic version of leftComm coincides with the regular version.

def TensorProduct.AlgebraTensorModule.rightComm (R : Type uR) (S : Type uS) (B : Type uB) (M : Type uM) (P : Type uP) (Q : Type uQ) [CommSemiring R] [Semiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [Module B M] [IsScalarTower R B M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [CommSemiring S] [Module S M] [Module S P] [Algebra S B] [IsScalarTower S B M] [SMulCommClass R S M] [SMulCommClass S R M] : TensorProduct R (TensorProduct S M P) Q ≃ₗ[B] TensorProduct S (TensorProduct R M Q) P

A tensor product analogue of mul_right_comm.

Suppose we have a diagram of algebras R → B ← S, and a B-module M, S-module P, R-module Q, then

(M ⊗ˢ P)      ⎛ M ⎞ ⊗ˢ P
 ⊗ᴿ       ≅ᴮ  ⎜ ⊗ᴿ⎟
 Q            ⎝ Q ⎠

@[simp]

theorem TensorProduct.AlgebraTensorModule.rightComm_tmul (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [Module B M] [IsScalarTower R B M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [CommSemiring S] [Module S M] [Module S P] [Algebra S B] [IsScalarTower S B M] [SMulCommClass R S M] [SMulCommClass S R M] (m : M) (p : P) (q : Q) : (rightComm R S B M P Q) (m ⊗ₜ[S] p ⊗ₜ[R] q) = m ⊗ₜ[R] q ⊗ₜ[S] p

@[simp]

theorem TensorProduct.AlgebraTensorModule.rightComm_symm (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [Module B M] [IsScalarTower R B M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [CommSemiring S] [Module S M] [Module S P] [Algebra S B] [IsScalarTower S B M] [SMulCommClass R S M] [SMulCommClass S R M] : (rightComm R S B M P Q).symm = rightComm S R B M Q P

theorem TensorProduct.AlgebraTensorModule.rightComm_symm_tmul (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [Module B M] [IsScalarTower R B M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [CommSemiring S] [Module S M] [Module S P] [Algebra S B] [IsScalarTower S B M] [SMulCommClass R S M] [SMulCommClass S R M] (m : M) (p : P) (q : Q) : (rightComm R S B M P Q).symm (m ⊗ₜ[R] q ⊗ₜ[S] p) = m ⊗ₜ[S] p ⊗ₜ[R] q

theorem TensorProduct.AlgebraTensorModule.rightComm_eq (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] : rightComm R R R M P Q = TensorProduct.rightComm R M P Q

The heterobasic version of leftComm coincides with the regular version.

def TensorProduct.AlgebraTensorModule.tensorTensorTensorComm (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (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 N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] [CommSemiring S] [Algebra R S] [Algebra S B] [Module S M] [Module S N] [IsScalarTower R S M] [SMulCommClass A S M] [SMulCommClass S A M] [IsScalarTower S B M] [IsScalarTower R S N] : TensorProduct A (TensorProduct S M N) (TensorProduct R P Q) ≃ₗ[B] TensorProduct S (TensorProduct A M P) (TensorProduct R N Q)

Heterobasic version of tensorTensorTensorComm.

Suppose we have towers of algebras R → S → B and R → A → B, and a B-module M, S-module N, A-module P, R-module Q, then

(M ⊗ˢ N)      ⎛ M ⎞ ⊗ˢ ⎛ N ⎞
 ⊗ᴬ       ≅ᴮ  ⎜ ⊗ᴬ⎟    ⎜ ⊗ᴿ⎟
(P ⊗ᴿ Q)      ⎝ P ⎠    ⎝ Q ⎠

@[simp]

theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {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 N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] [CommSemiring S] [Algebra R S] [Algebra S B] [Module S M] [Module S N] [IsScalarTower R S M] [SMulCommClass A S M] [SMulCommClass S A M] [IsScalarTower S B M] [IsScalarTower R S N] (m : M) (n : N) (p : P) (q : Q) : (tensorTensorTensorComm R S A B M N P Q) (m ⊗ₜ[S] n ⊗ₜ[A] (p ⊗ₜ[R] q)) = m ⊗ₜ[A] p ⊗ₜ[S] (n ⊗ₜ[R] q)

@[simp]

theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {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 N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] [CommSemiring S] [Algebra R S] [Algebra S B] [Module S M] [Module S N] [IsScalarTower R S M] [SMulCommClass A S M] [SMulCommClass S A M] [IsScalarTower S B M] [IsScalarTower R S N] : (tensorTensorTensorComm R S A B M N P Q).symm = tensorTensorTensorComm R A S B M P N Q

theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {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 N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module R Q] [Module R P] [IsScalarTower R A P] [Algebra A B] [IsScalarTower A B M] [CommSemiring S] [Algebra R S] [Algebra S B] [Module S M] [Module S N] [IsScalarTower R S M] [SMulCommClass A S M] [SMulCommClass S A M] [IsScalarTower S B M] [IsScalarTower R S N] (m : M) (n : N) (p : P) (q : Q) : (tensorTensorTensorComm R S A B M N P Q).symm (m ⊗ₜ[A] p ⊗ₜ[S] (n ⊗ₜ[R] q)) = m ⊗ₜ[S] n ⊗ₜ[A] (p ⊗ₜ[R] q)

theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq (R : Type uR) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] : tensorTensorTensorComm R R R R M N P Q = TensorProduct.tensorTensorTensorComm R M N P Q

The heterobasic version of tensorTensorTensorComm coincides with the regular version.

The base-change of a linear map of R-modules to a linear map of A-modules

def LinearMap.baseChange {R : Type u_1} (A : Type u_2) {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : TensorProduct R A M →ₗ[A] TensorProduct R A N

baseChange A f for f : M →ₗ[R] N is the A-linear map A ⊗[R] M →ₗ[A] A ⊗[R] N.

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

@[simp]

theorem LinearMap.baseChange_tmul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (a : A) (x : M) : (baseChange A f) (a ⊗ₜ[R] x) = a ⊗ₜ[R] f x

theorem LinearMap.baseChange_eq_ltensor {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : ⇑(baseChange A f) = ⇑(lTensor A f)

@[simp]

theorem LinearMap.baseChange_add {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : M →ₗ[R] N) : baseChange A (f + g) = baseChange A f + baseChange A g

@[simp]

theorem LinearMap.baseChange_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : baseChange A 0 = 0

@[simp]

theorem LinearMap.baseChange_smul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) (f : M →ₗ[R] N) : baseChange A (r • f) = r • baseChange A f

@[simp]

theorem LinearMap.baseChange_id {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : baseChange A id = id

theorem LinearMap.baseChange_comp {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : baseChange A (g ∘ₗ f) = baseChange A g ∘ₗ baseChange A f

@[simp]

theorem LinearMap.baseChange_one (R : Type u_1) {A : Type u_2} (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : baseChange A 1 = 1

theorem LinearMap.baseChange_mul {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f g : Module.End R M) : baseChange A (f * g) = baseChange A f * baseChange A g

def LinearEquiv.baseChange (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : M ≃ₗ[R] N) : TensorProduct R A M ≃ₗ[A] TensorProduct R A N

baseChange A e for e : M ≃ₗ[R] N is the A-linear map A ⊗[R] M ≃ₗ[A] A ⊗[R] N.

def LinearMap.baseChangeHom (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : (M →ₗ[R] N) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A N

baseChange as a linear map.

When M = N, this is true more strongly as Module.End.baseChangeHom.

@[simp]

theorem LinearMap.baseChangeHom_apply (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : (baseChangeHom R A M N) f = baseChange A f

def Module.End.baseChangeHom (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : End R M →ₐ[R] End A (TensorProduct R A M)

baseChange as an AlgHom.

@[simp]

theorem Module.End.baseChangeHom_apply_apply (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (a : End R M) (a✝ : TensorProduct R A M) : ((baseChangeHom R A M) a) a✝ = (TensorProduct.liftAux (↑R { toFun := fun (h : M →ₗ[R] TensorProduct R A M) => h ∘ₗ a, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ ↑R (TensorProduct.AlgebraTensorModule.mk R A A M))) a✝

theorem LinearMap.baseChange_pow (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : Module.End R M) (n : ℕ) : baseChange A (f ^ n) = baseChange A f ^ n

theorem LinearMap.rTensor_baseChange {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (φ : A →ₐ[R] B) (t : TensorProduct R A M) (f : M →ₗ[R] N) : (rTensor N φ.toLinearMap) ((baseChange A f) t) = (baseChange B f) ((rTensor M φ.toLinearMap) t)

@[simp]

theorem LinearMap.baseChange_sub {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f g : M →ₗ[R] N) : baseChange A (f - g) = baseChange A f - baseChange A g

@[simp]

theorem LinearMap.baseChange_neg {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : baseChange A (-f) = -baseChange A f

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) : Submodule A (TensorProduct R A 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".

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) : a ⊗ₜ[R] m ∈ baseChange A p

theorem Submodule.baseChange_eq_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] (p : Submodule R M) : baseChange A p = span A ↑(map ((TensorProduct.mk R A M) 1) p)

@[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] : baseChange A ⊥ = ⊥

@[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] : baseChange A ⊤ = ⊤

@[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) : baseChange A (span R s) = span A (⇑((TensorProduct.mk R A M) 1) '' s)