The tensor product of R-algebras

This file provides results about the multiplicative structure on A ⊗[R] B when R is a commutative (semi)ring and A and B are both R-algebras. On these tensor products, multiplication is characterized by (a₁ ⊗ₜ b₁) * (a₂ ⊗ₜ b₂) = (a₁ * a₂) ⊗ₜ (b₁ * b₂).

Main declarations

• LinearMap.baseChange A f is the A-linear map A ⊗ f, for an R-linear map f.
• Algebra.TensorProduct.semiring: the ring structure on A ⊗[R] B for two R-algebras A, B.
• Algebra.TensorProduct.leftAlgebra: the S-algebra structure on A ⊗[R] B, for when A is additionally an S algebra.
• the structure isomorphisms
  • Algebra.TensorProduct.lid : R ⊗[R] A ≃ₐ[R] A
  • Algebra.TensorProduct.rid : A ⊗[R] R ≃ₐ[S] A (usually used with S = R or S = A)
  • Algebra.TensorProduct.comm : A ⊗[R] B ≃ₐ[R] B ⊗[R] A
  • Algebra.TensorProduct.assoc : ((A ⊗[R] B) ⊗[R] C) ≃ₐ[R] (A ⊗[R] (B ⊗[R] C))

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] [Module R M] [AddCommMonoid N] [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.

@[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] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (a : A) (x : M) : ↑(LinearMap.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] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : ↑(LinearMap.baseChange A f) = ↑(LinearMap.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] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (g : M →ₗ[R] N) : LinearMap.baseChange A (f + g) = LinearMap.baseChange A f + LinearMap.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] [Module R M] [AddCommMonoid N] [Module R N] : LinearMap.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] [Module R M] [AddCommMonoid N] [Module R N] (r : R) (f : M →ₗ[R] N) : LinearMap.baseChange A (r • f) = r • LinearMap.baseChange A f

@[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] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : ↑(LinearMap.baseChangeHom R A M N) f = LinearMap.baseChange A f

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

baseChange as a linear map.

@[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 : M →ₗ[R] N) (g : M →ₗ[R] N) : LinearMap.baseChange A (f - g) = LinearMap.baseChange A f - LinearMap.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) : LinearMap.baseChange A (-f) = -LinearMap.baseChange A f

The R-algebra structure on A ⊗[R] B

def Algebra.TensorProduct.mulAux {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a₁ : A) (b₁ : B) : TensorProduct R A B →ₗ[R] TensorProduct R A B

(Implementation detail) The multiplication map on A ⊗[R] B, for a fixed pure tensor in the first argument, as an R-linear map.

@[simp]

theorem Algebra.TensorProduct.mulAux_apply {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) : ↑(Algebra.TensorProduct.mulAux a₁ b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)

def Algebra.TensorProduct.mul {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : TensorProduct R A B →ₗ[R] TensorProduct R A B →ₗ[R] TensorProduct R A B

(Implementation detail) The multiplication map on A ⊗[R] B, as an R-bilinear map.

@[simp]

theorem Algebra.TensorProduct.mul_apply {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) : ↑(↑Algebra.TensorProduct.mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)

theorem Algebra.TensorProduct.mul_assoc {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (x : TensorProduct R A B) (y : TensorProduct R A B) (z : TensorProduct R A B) : ↑(↑Algebra.TensorProduct.mul (↑(↑Algebra.TensorProduct.mul x) y)) z = ↑(↑Algebra.TensorProduct.mul x) (↑(↑Algebra.TensorProduct.mul y) z)

theorem Algebra.TensorProduct.one_mul {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (x : TensorProduct R A B) : ↑(↑Algebra.TensorProduct.mul (1 ⊗ₜ[R] 1)) x = x

theorem Algebra.TensorProduct.mul_one {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (x : TensorProduct R A B) : ↑(↑Algebra.TensorProduct.mul x) (1 ⊗ₜ[R] 1) = x

instance Algebra.TensorProduct.instOneTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : One (TensorProduct R A B)

theorem Algebra.TensorProduct.one_def {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : 1 = 1 ⊗ₜ[R] 1

instance Algebra.TensorProduct.instAddMonoidWithOneTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : AddMonoidWithOne (TensorProduct R A B)

theorem Algebra.TensorProduct.natCast_def {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (n : ℕ) : ↑n = ↑n ⊗ₜ[R] 1

instance Algebra.TensorProduct.instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : AddCommMonoid (TensorProduct R A B)

instance Algebra.TensorProduct.instMul {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : Mul (TensorProduct R A B)

@[simp]

theorem Algebra.TensorProduct.tmul_mul_tmul {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) : a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)

instance Algebra.TensorProduct.instSemiring {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : Semiring (TensorProduct R A B)

@[simp]

theorem Algebra.TensorProduct.tmul_pow {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a : A) (b : B) (k : ℕ) : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)

@[simp]

theorem Algebra.TensorProduct.includeLeftRingHom_apply {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a : A) : ↑Algebra.TensorProduct.includeLeftRingHom a = a ⊗ₜ[R] 1

def Algebra.TensorProduct.includeLeftRingHom {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : A →+* TensorProduct R A B

The ring morphism A →+* A ⊗[R] B sending a to a ⊗ₜ 1.

instance Algebra.TensorProduct.isScalarTower_right {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Monoid S] [DistribMulAction S A] [IsScalarTower S A A] [SMulCommClass R S A] : IsScalarTower S (TensorProduct R A B) (TensorProduct R A B)

instance Algebra.TensorProduct.sMulCommClass_right {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Monoid S] [DistribMulAction S A] [SMulCommClass S A A] [SMulCommClass R S A] : SMulCommClass S (TensorProduct R A B) (TensorProduct R A B)

instance Algebra.TensorProduct.leftAlgebra {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring S] [Algebra S A] [SMulCommClass R S A] : Algebra S (TensorProduct R A B)

instance Algebra.TensorProduct.instAlgebra {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : Algebra R (TensorProduct R A B)

The tensor product of two R-algebras is an R-algebra.

@[simp]

theorem Algebra.TensorProduct.algebraMap_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring S] [Algebra S A] [SMulCommClass R S A] (r : S) : ↑(algebraMap S (TensorProduct R A B)) r = ↑(algebraMap S A) r ⊗ₜ[R] 1

def Algebra.TensorProduct.includeLeft {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring S] [Algebra S A] [SMulCommClass R S A] : A →ₐ[S] TensorProduct R A B

The R-algebra morphism A →ₐ[R] A ⊗[R] B sending a to a ⊗ₜ 1.

@[simp]

theorem Algebra.TensorProduct.includeLeft_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring S] [Algebra S A] [SMulCommClass R S A] (a : A) : ↑Algebra.TensorProduct.includeLeft a = a ⊗ₜ[R] 1

def Algebra.TensorProduct.includeRight {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : B →ₐ[R] TensorProduct R A B

The algebra morphism B →ₐ[R] A ⊗[R] B sending b to 1 ⊗ₜ b.

@[simp]

theorem Algebra.TensorProduct.includeRight_apply {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (b : B) : ↑Algebra.TensorProduct.includeRight b = 1 ⊗ₜ[R] b

theorem Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : RingHom.comp Algebra.TensorProduct.includeLeftRingHom (algebraMap R A) = RingHom.comp (↑Algebra.TensorProduct.includeRight) (algebraMap R B)

theorem Algebra.TensorProduct.ext {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [CommSemiring S] [Algebra S A] [Algebra R S] [Algebra S C] [IsScalarTower R S A] [IsScalarTower R S C] ⦃f : TensorProduct R A B →ₐ[S] C⦄ ⦃g : TensorProduct R A B →ₐ[S] C⦄ (ha : AlgHom.comp f Algebra.TensorProduct.includeLeft = AlgHom.comp g Algebra.TensorProduct.includeLeft) (hb : AlgHom.comp (AlgHom.restrictScalars R f) Algebra.TensorProduct.includeRight = AlgHom.comp (AlgHom.restrictScalars R g) Algebra.TensorProduct.includeRight) : f = g

A version of TensorProduct.ext for AlgHom.

Using this as the @[ext] lemma instead of Algebra.TensorProduct.ext' allows ext to apply lemmas specific to A →ₐ[S] _ and B →ₐ[R] _; notably this allows recursion into nested tensor products of algebras.

See note [partially-applied ext lemmas].

theorem Algebra.TensorProduct.ext' {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [CommSemiring S] [Algebra S A] [Algebra R S] [Algebra S C] [IsScalarTower R S A] [IsScalarTower R S C] {g : TensorProduct R A B →ₐ[S] C} {h : TensorProduct R A B →ₐ[S] C} (H : ∀ (a : A) (b : B), ↑g (a ⊗ₜ[R] b) = ↑h (a ⊗ₜ[R] b)) : g = h

instance Algebra.TensorProduct.instRing {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] : Ring (TensorProduct R A B)

theorem Algebra.TensorProduct.intCast_def {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] (z : ℤ) : ↑z = ↑z ⊗ₜ[R] 1

instance Algebra.TensorProduct.instCommRing {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] : CommRing (TensorProduct R A B)

@[reducible]

def Algebra.TensorProduct.rightAlgebra {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] : Algebra B (TensorProduct R A B)

S ⊗[R] T has a T-algebra structure. This is not a global instance or else the action of S on S ⊗[R] S would be ambiguous.

instance Algebra.TensorProduct.right_isScalarTower {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] : IsScalarTower R B (TensorProduct R A B)

We now build the structure maps for the symmetric monoidal category of R-algebras.

def Algebra.TensorProduct.algHomOfLinearMapTensorProduct {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] (f : TensorProduct R A B →ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑f (a₁ ⊗ₜ[R] b₁) * ↑f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : S), ↑f (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S C) r) : TensorProduct R A B →ₐ[S] C

Build an algebra morphism from a linear map out of a tensor product, and evidence of multiplicativity on pure tensors.

@[simp]

theorem Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] (f : TensorProduct R A B →ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑f (a₁ ⊗ₜ[R] b₁) * ↑f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : S), ↑f (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S C) r) (x : TensorProduct R A B) : ↑(Algebra.TensorProduct.algHomOfLinearMapTensorProduct f w₁ w₂) x = ↑f x

def Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] (f : TensorProduct R A B ≃ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑f (a₁ ⊗ₜ[R] b₁) * ↑f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : S), ↑f (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S C) r) : TensorProduct R A B ≃ₐ[S] C

Build an algebra equivalence from a linear equivalence out of a tensor product, and evidence of multiplicativity on pure tensors.

@[simp]

theorem Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] (f : TensorProduct R A B ≃ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑f (a₁ ⊗ₜ[R] b₁) * ↑f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : S), ↑f (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S C) r) (x : TensorProduct R A B) : ↑(Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct f w₁ w₂) x = ↑f x

def Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : TensorProduct R (TensorProduct R A B) C ≃ₗ[R] D) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C), ↑f (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = ↑f ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * ↑f ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂)) (w₂ : ∀ (r : R), ↑f ((↑(algebraMap R A) r ⊗ₜ[R] 1) ⊗ₜ[R] 1) = ↑(algebraMap R D) r) : TensorProduct R (TensorProduct R A B) C ≃ₐ[R] D

Build an algebra equivalence from a linear equivalence out of a triple tensor product, and evidence of multiplicativity on pure tensors.

@[simp]

theorem Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : TensorProduct R (TensorProduct R A B) C ≃ₗ[R] D) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C), ↑f (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = ↑f ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * ↑f ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂)) (w₂ : ∀ (r : R), ↑f ((↑(algebraMap R A) r ⊗ₜ[R] 1) ⊗ₜ[R] 1) = ↑(algebraMap R D) r) (x : TensorProduct R (TensorProduct R A B) C) : ↑(Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct f w₁ w₂) x = ↑f x

def Algebra.TensorProduct.lid (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R R A ≃ₐ[R] A

The base ring is a left identity for the tensor product of algebra, up to algebra isomorphism.

@[simp]

theorem Algebra.TensorProduct.lid_tmul (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (a : A) : ↑(Algebra.TensorProduct.lid R A) (r ⊗ₜ[R] a) = r • a

def Algebra.TensorProduct.rid (R : Type uR) (S : Type uS) (A : Type uA) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] : TensorProduct R A R ≃ₐ[S] A

The base ring is a right identity for the tensor product of algebra, up to algebra isomorphism.

Note that if A is commutative this can be instantiated with S = A.

@[simp]

theorem Algebra.TensorProduct.rid_tmul {R : Type uR} (S : Type uS) {A : Type uA} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (r : R) (a : A) : ↑(Algebra.TensorProduct.rid R S A) (a ⊗ₜ[R] r) = r • a

def Algebra.TensorProduct.comm (R : Type uR) (A : Type uA) (B : Type uB) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : TensorProduct R A B ≃ₐ[R] TensorProduct R B A

The tensor product of R-algebras is commutative, up to algebra isomorphism.

@[simp]

theorem Algebra.TensorProduct.comm_tmul (R : Type uR) (A : Type uA) (B : Type uB) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a : A) (b : B) : ↑(Algebra.TensorProduct.comm R A B) (a ⊗ₜ[R] b) = b ⊗ₜ[R] a

theorem Algebra.TensorProduct.adjoin_tmul_eq_top (R : Type uR) (A : Type uA) (B : Type uB) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : Algebra.adjoin R {t | ∃ a b, a ⊗ₜ[R] b = t} = ⊤

theorem Algebra.TensorProduct.assoc_aux_1 {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) (c₁ : C) (c₂ : C) : ↑(TensorProduct.assoc R A B C) (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = ↑(TensorProduct.assoc R A B C) ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * ↑(TensorProduct.assoc R A B C) ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂)

theorem Algebra.TensorProduct.assoc_aux_2 {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (r : R) : ↑(TensorProduct.assoc R A B C) ((↑(algebraMap R A) r ⊗ₜ[R] 1) ⊗ₜ[R] 1) = ↑(algebraMap R (TensorProduct R A (TensorProduct R B C))) r

def Algebra.TensorProduct.assoc {R : Type uR} (A : Type uA) (B : Type uB) (C : Type uC) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] : TensorProduct R (TensorProduct R A B) C ≃ₐ[R] TensorProduct R A (TensorProduct R B C)

The associator for tensor product of R-algebras, as an algebra isomorphism.

@[simp]

theorem Algebra.TensorProduct.assoc_tmul {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (a : A) (b : B) (c : C) : ↑(TensorProduct.assoc R A B C) ((a ⊗ₜ[R] b) ⊗ₜ[R] c) = a ⊗ₜ[R] b ⊗ₜ[R] c

def Algebra.TensorProduct.map {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[S] B) (g : C →ₐ[R] D) : TensorProduct R A C →ₐ[S] TensorProduct R B D

The tensor product of a pair of algebra morphisms.

@[simp]

theorem Algebra.TensorProduct.map_tmul {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[S] B) (g : C →ₐ[R] D) (a : A) (c : C) : ↑(Algebra.TensorProduct.map f g) (a ⊗ₜ[R] c) = ↑f a ⊗ₜ[R] ↑g c

@[simp]

theorem Algebra.TensorProduct.map_id {R : Type uR} {S : Type uS} {A : Type uA} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring C] [Algebra R C] : Algebra.TensorProduct.map (AlgHom.id S A) (AlgHom.id R C) = AlgHom.id S (TensorProduct R A C)

theorem Algebra.TensorProduct.map_comp {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} {E : Type uE} {F : Type uF} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] [Semiring E] [Algebra R E] [Semiring F] [Algebra R F] (f₂ : B →ₐ[S] C) (f₁ : A →ₐ[S] B) (g₂ : E →ₐ[R] F) (g₁ : D →ₐ[R] E) : Algebra.TensorProduct.map (AlgHom.comp f₂ f₁) (AlgHom.comp g₂ g₁) = AlgHom.comp (Algebra.TensorProduct.map f₂ g₂) (Algebra.TensorProduct.map f₁ g₁)

@[simp]

theorem Algebra.TensorProduct.map_comp_includeLeft {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[S] B) (g : C →ₐ[R] D) : AlgHom.comp (Algebra.TensorProduct.map f g) Algebra.TensorProduct.includeLeft = AlgHom.comp Algebra.TensorProduct.includeLeft f

@[simp]

theorem Algebra.TensorProduct.map_restrictScalars_comp_includeRight {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[S] B) (g : C →ₐ[R] D) : AlgHom.comp (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)) Algebra.TensorProduct.includeRight = AlgHom.comp Algebra.TensorProduct.includeRight g

@[simp]

theorem Algebra.TensorProduct.map_comp_includeRight {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) : AlgHom.comp (Algebra.TensorProduct.map f g) Algebra.TensorProduct.includeRight = AlgHom.comp Algebra.TensorProduct.includeRight g

theorem Algebra.TensorProduct.map_range {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) : AlgHom.range (Algebra.TensorProduct.map f g) = AlgHom.range (AlgHom.comp Algebra.TensorProduct.includeLeft f) ⊔ AlgHom.range (AlgHom.comp Algebra.TensorProduct.includeRight g)

def Algebra.TensorProduct.congr {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) : TensorProduct R A C ≃ₐ[S] TensorProduct R B D

Construct an isomorphism between tensor products of an S-algebra with an R-algebra from S- and R- isomorphisms between the tensor factors.

@[simp]

theorem Algebra.TensorProduct.congr_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) (x : TensorProduct R A C) : ↑(Algebra.TensorProduct.congr f g) x = ↑(Algebra.TensorProduct.map ↑f ↑g) x

@[simp]

theorem Algebra.TensorProduct.congr_symm_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) (x : TensorProduct R B D) : ↑(AlgEquiv.symm (Algebra.TensorProduct.congr f g)) x = ↑(Algebra.TensorProduct.map ↑(AlgEquiv.symm f) ↑(AlgEquiv.symm g)) x

@[simp]

theorem Algebra.TensorProduct.congr_refl {R : Type uR} {S : Type uS} {A : Type uA} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring C] [Algebra R C] : Algebra.TensorProduct.congr AlgEquiv.refl AlgEquiv.refl = AlgEquiv.refl

theorem Algebra.TensorProduct.congr_trans {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} {E : Type uE} {F : Type uF} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] [Semiring E] [Algebra R E] [Semiring F] [Algebra R F] (f₁ : A ≃ₐ[S] B) (f₂ : B ≃ₐ[S] C) (g₁ : D ≃ₐ[R] E) (g₂ : E ≃ₐ[R] F) : Algebra.TensorProduct.congr (AlgEquiv.trans f₁ f₂) (AlgEquiv.trans g₁ g₂) = AlgEquiv.trans (Algebra.TensorProduct.congr f₁ g₁) (Algebra.TensorProduct.congr f₂ g₂)

theorem Algebra.TensorProduct.congr_symm {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) : Algebra.TensorProduct.congr (AlgEquiv.symm f) (AlgEquiv.symm g) = AlgEquiv.symm (Algebra.TensorProduct.congr f g)

def Algebra.TensorProduct.lmul' (R : Type uR) {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : TensorProduct R S S →ₐ[R] S

LinearMap.mul' is an AlgHom on commutative rings.

theorem Algebra.TensorProduct.lmul'_toLinearMap {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : AlgHom.toLinearMap (Algebra.TensorProduct.lmul' R) = LinearMap.mul' R S

@[simp]

theorem Algebra.TensorProduct.lmul'_apply_tmul {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] (a : S) (b : S) : ↑(Algebra.TensorProduct.lmul' R) (a ⊗ₜ[R] b) = a * b

@[simp]

theorem Algebra.TensorProduct.lmul'_comp_includeLeft {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : AlgHom.comp (Algebra.TensorProduct.lmul' R) Algebra.TensorProduct.includeLeft = AlgHom.id R S

@[simp]

theorem Algebra.TensorProduct.lmul'_comp_includeRight {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : AlgHom.comp (Algebra.TensorProduct.lmul' R) Algebra.TensorProduct.includeRight = AlgHom.id R S

def Algebra.TensorProduct.productMap {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) : TensorProduct R A B →ₐ[R] S

If S is commutative, for a pair of morphisms f : A →ₐ[R] S, g : B →ₐ[R] S, We obtain a map A ⊗[R] B →ₐ[R] S that commutes with f, g via a ⊗ b ↦ f(a) * g(b).

@[simp]

theorem Algebra.TensorProduct.productMap_apply_tmul {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (a : A) (b : B) : ↑(Algebra.TensorProduct.productMap f g) (a ⊗ₜ[R] b) = ↑f a * ↑g b

theorem Algebra.TensorProduct.productMap_left_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (a : A) : ↑(Algebra.TensorProduct.productMap f g) (a ⊗ₜ[R] 1) = ↑f a

@[simp]

theorem Algebra.TensorProduct.productMap_left {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) : AlgHom.comp (Algebra.TensorProduct.productMap f g) Algebra.TensorProduct.includeLeft = f

theorem Algebra.TensorProduct.productMap_right_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (b : B) : ↑(Algebra.TensorProduct.productMap f g) (1 ⊗ₜ[R] b) = ↑g b

@[simp]

theorem Algebra.TensorProduct.productMap_right {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) : AlgHom.comp (Algebra.TensorProduct.productMap f g) Algebra.TensorProduct.includeRight = g

theorem Algebra.TensorProduct.productMap_range {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) : AlgHom.range (Algebra.TensorProduct.productMap f g) = AlgHom.range f ⊔ AlgHom.range g

@[simp]

theorem Algebra.TensorProduct.productLeftAlgHom_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [CommSemiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C) : ∀ (a : TensorProduct R A B), ↑(Algebra.TensorProduct.productLeftAlgHom f g) a = ↑(Algebra.TensorProduct.lmul' R) (↑(Algebra.TensorProduct.map (AlgHom.restrictScalars R f) g) a)

def Algebra.TensorProduct.productLeftAlgHom {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [CommSemiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C) : TensorProduct R A B →ₐ[S] C

If A, B, C are R-algebras, A and C are also S-algebras (forming a tower as ·/S/R), then the product map of f : A →ₐ[S] C and g : B →ₐ[R] C is an S-algebra homomorphism.

noncomputable def Algebra.TensorProduct.basisAux {R : Type uR} (A : Type uA) {M : Type uM} {ι : Type uι} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : TensorProduct R A M ≃ₗ[R] ι →₀ A

Given an R-algebra A and an R-basis of M, this is an R-linear isomorphism A ⊗[R] M ≃ (ι →₀ A) (which is in fact A-linear).

theorem Algebra.TensorProduct.basisAux_tmul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (a : A) (m : M) : ↑(Algebra.TensorProduct.basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ↑(algebraMap R A) (_ : ↑(algebraMap R A) 0 = 0) (↑b.repr m)

theorem Algebra.TensorProduct.basisAux_map_smul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (a : A) (x : TensorProduct R A M) : ↑(Algebra.TensorProduct.basisAux A b) (a • x) = a • ↑(Algebra.TensorProduct.basisAux A b) x

noncomputable def Algebra.TensorProduct.basis {R : Type uR} (A : Type uA) {M : Type uM} {ι : Type uι} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : Basis ι A (TensorProduct R A M)

Given a R-algebra A, this is the A-basis of A ⊗[R] M induced by a R-basis of M.

@[simp]

theorem Algebra.TensorProduct.basis_repr_tmul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (a : A) (m : M) : ↑(Algebra.TensorProduct.basis A b).repr (a ⊗ₜ[R] m) = a • Finsupp.mapRange ↑(algebraMap R A) (_ : ↑(algebraMap R A) 0 = 0) (↑b.repr m)

theorem Algebra.TensorProduct.basis_repr_symm_apply {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (a : A) (i : ι) : (↑(LinearEquiv.symm (Algebra.TensorProduct.basis A b).repr) fun₀ | i => a) = a ⊗ₜ[R] ↑(LinearEquiv.symm b.repr) fun₀ | i => 1

@[simp]

theorem Algebra.TensorProduct.basis_repr_symm_apply' {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (a : A) (i : ι) : a • ↑(Algebra.TensorProduct.basis A b) i = a ⊗ₜ[R] ↑b i

def Module.endTensorEndAlgHom {R : Type u_1} {S : Type u_2} {A : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [CommSemiring S] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Algebra S A] [Algebra R A] [Module R M] [Module S M] [Module A M] [Module R N] [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S M] : TensorProduct R (Module.End A M) (Module.End R N) →ₐ[S] Module.End A (TensorProduct R M N)

The algebra homomorphism from End M ⊗ End N to End (M ⊗ N) sending f ⊗ₜ g to the TensorProduct.map f g, the tensor product of the two maps.

This is an AlgHom version of TensorProduct.AlgebraTensorModule.homTensorHomMap. Like that definition, this is generalized across many different rings; namely a tower of algebras A/S/R.

theorem Module.endTensorEndAlgHom_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [CommSemiring S] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Algebra S A] [Algebra R A] [Module R M] [Module S M] [Module A M] [Module R N] [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S M] (f : Module.End A M) (g : Module.End R N) : ↑Module.endTensorEndAlgHom (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g

theorem Subalgebra.finiteDimensional_sup {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] (E1 : Subalgebra K L) (E2 : Subalgebra K L) [FiniteDimensional K { x // x ∈ E1 }] [FiniteDimensional K { x // x ∈ E2 }] : FiniteDimensional K { x // x ∈ E1 ⊔ E2 }

def TensorProduct.Algebra.moduleAux {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] : TensorProduct R A B →ₗ[R] M →ₗ[R] M

An auxiliary definition, used for constructing the Module (A ⊗[R] B) M in TensorProduct.Algebra.module below.

theorem TensorProduct.Algebra.moduleAux_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] (a : A) (b : B) (m : M) : ↑(↑TensorProduct.Algebra.moduleAux (a ⊗ₜ[R] b)) m = a • b • m

def TensorProduct.Algebra.module {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] : Module (TensorProduct R A B) M

If M is a representation of two different R-algebras A and B whose actions commute, then it is a representation the R-algebra A ⊗[R] B.

An important example arises from a semiring S; allowing S to act on itself via left and right multiplication, the roles of R, A, B, M are played by ℕ, S, Sᵐᵒᵖ, S. This example is important because a submodule of S as a Module over S ⊗[ℕ] Sᵐᵒᵖ is a two-sided ideal.

NB: This is not an instance because in the case B = A and M = A ⊗[R] A we would have a diamond of smul actions. Furthermore, this would not be a mere definitional diamond but a true mathematical diamond in which A ⊗[R] A had two distinct scalar actions on itself: one from its multiplication, and one from this would-be instance. Arguably we could live with this but in any case the real fix is to address the ambiguity in notation, probably along the lines outlined here: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929258

theorem TensorProduct.Algebra.smul_def {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (a : A) (b : B) (m : M) : a ⊗ₜ[R] b • m = a • b • m