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

• 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.

References

• [C. Kassel, Quantum Groups (§II.4)][Kassel1995]

def LinearMap.liftBaseChangeEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] : (M →ₗ[R] N) ≃ₗ[A] TensorProduct R A M →ₗ[A] N

If M is an R-module and N is an A-module, then A-linear maps A ⊗[R] M →ₗ[A] N correspond to R linear maps M →ₗ[R] N by composing with M → A ⊗ M, x ↦ 1 ⊗ x.

@[reducible, inline]

abbrev LinearMap.liftBaseChange {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) : TensorProduct R A M →ₗ[A] N

If N is an A module, we may lift a linear map M →ₗ[R] N to A ⊗[R] M →ₗ[A] N

@[simp]

theorem LinearMap.liftBaseChange_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) (x : A) (y : M) : (liftBaseChange A l) (x ⊗ₜ[R] y) = x • l y

theorem LinearMap.liftBaseChange_one_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) (y : M) : (liftBaseChange A l) (1 ⊗ₜ[R] y) = l y

@[simp]

theorem LinearMap.liftBaseChangeEquiv_symm_apply {R : Type u_4} {M : Type u_2} {N : Type u_3} (A : Type u_1) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : TensorProduct R A M →ₗ[A] N) (x : M) : ((liftBaseChangeEquiv A).symm l) x = l (1 ⊗ₜ[R] x)

theorem LinearMap.liftBaseChange_comp {R : Type u_3} {M : Type u_4} {N : Type u_5} (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] {P : Type u_1} [AddCommMonoid P] [Module A P] [Module R P] [IsScalarTower R A P] (l : M →ₗ[R] N) (l' : N →ₗ[A] P) : l' ∘ₗ liftBaseChange A l = liftBaseChange A (↑R l' ∘ₗ l)

@[simp]

theorem LinearMap.range_liftBaseChange {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) : (liftBaseChange A l).range = Submodule.span A ↑l.range

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

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

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

instance Algebra.TensorProduct.instAddCommMonoidWithOne {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [AddCommMonoidWithOne A] [Module R A] [AddCommMonoidWithOne B] [Module R B] : AddCommMonoidWithOne (TensorProduct R A B)

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

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

@[irreducible]

def Algebra.TensorProduct.mul {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B 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] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (a₁ a₂ : A) (b₁ b₂ : B) : (mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)

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

@[simp]

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

theorem SemiconjBy.tmul {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] {a₁ a₂ a₃ : A} {b₁ b₂ b₃ : B} (ha : SemiconjBy a₁ a₂ a₃) (hb : SemiconjBy b₁ b₂ b₃) : SemiconjBy (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃)

theorem Commute.tmul {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] {a₁ a₂ : A} {b₁ b₂ : B} (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) : Commute (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂)

instance Algebra.TensorProduct.instNonUnitalNonAssocSemiring {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] : NonUnitalNonAssocSemiring (TensorProduct R A B)

@[instance 100]

instance Algebra.TensorProduct.isScalarTower_right {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B 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 100]

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

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

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

instance Algebra.TensorProduct.instNonAssocSemiring {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] : NonAssocSemiring (TensorProduct R A B)

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

instance Algebra.TensorProduct.instNonUnitalSemiring {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] : NonUnitalSemiring (TensorProduct R A 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)

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.

@[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) : includeLeftRingHom a = a ⊗ₜ[R] 1

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)

theorem Algebra.TensorProduct.algebraMap_def {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] : algebraMap S (TensorProduct R A B) = includeLeftRingHom.comp (algebraMap S A)

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

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

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) : 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) : 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] : includeLeftRingHom.comp (algebraMap R A) = includeRight.comp (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 g : TensorProduct R A B →ₐ[S] C⦄ (ha : f.comp includeLeft = g.comp includeLeft) (hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp 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_iff {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 g : TensorProduct R A B →ₐ[S] C} : f = g ↔ f.comp includeLeft = g.comp includeLeft ∧ (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight

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 h : TensorProduct R A B →ₐ[S] C} (H : ∀ (a : A) (b : B), g (a ⊗ₜ[R] b) = h (a ⊗ₜ[R] b)) : g = h

theorem Algebra.TensorProduct.ringHom_ext {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {C : Type u_3} [Semiring C] {f g : TensorProduct R A B →+* C} (h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom) (h₂ : f.comp includeRight.toRingHom = g.comp includeRight.toRingHom) : f = g

theorem Algebra.TensorProduct.ringHom_ext_iff {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {C : Type u_3} [Semiring C] {f g : TensorProduct R A B →+* C} : f = g ↔ f.comp includeLeftRingHom = g.comp includeLeftRingHom ∧ f.comp includeRight.toRingHom = g.comp includeRight.toRingHom

instance Algebra.TensorProduct.instAddCommGroupWithOne {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [AddCommGroupWithOne A] [Module R A] [AddCommMonoidWithOne B] [Module R B] : AddCommGroupWithOne (TensorProduct R A B)

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

instance Algebra.TensorProduct.instNonUnitalNonAssocRing {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] : NonUnitalNonAssocRing (TensorProduct R A B)

instance Algebra.TensorProduct.instNonAssocRing {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] : NonAssocRing (TensorProduct R A B)

instance Algebra.TensorProduct.instNonUnitalRing {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] : NonUnitalRing (TensorProduct R A B)

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

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

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

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

@[reducible, inline]

abbrev Algebra.TensorProduct.rightAlgebra {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [CommSemiring 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.

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

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

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

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

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

theorem Algebra.TensorProduct.closure_range_union_range_eq_top (R : Type uR) (A : Type uA) (B : Type uB) [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] : Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight) = ⊤

theorem Algebra.TensorProduct.adjoin_one_tmul_image_eq_top {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] (s : Set B) (hs : adjoin R s = ⊤) : adjoin A ((fun (x : B) => 1 ⊗ₜ[R] x) '' s) = ⊤

If s generates T as an R-algebra, then { 1 ⊗ x | x ∈ s } generates A ⊗[R] T as an A-algebra.

theorem Algebra.TensorProduct.mk_one_injective_of_isScalarTower {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] : Function.Injective ⇑((TensorProduct.mk R S M) 1)

If M is a B-module that is also an A-module, the canonical map M →ₗ[A] B ⊗[A] M is injective.

theorem Algebra.baseChange_lmul {R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {A : Type u_3} [CommSemiring A] [Algebra R A] (f : B) : LinearMap.baseChange A ((lmul R B) f) = (lmul A (TensorProduct R A B)) (1 ⊗ₜ[R] f)

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

theorem TensorProduct.Algebra.linearMap_comp_mul' {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] : Algebra.linearMap R (TensorProduct R A B) ∘ₗ LinearMap.mul' R R = map (Algebra.linearMap R A) (Algebra.linearMap R B)

theorem Submodule.map_range_rTensor_subtype_lid {R : Type u_1} {Q : Type u_2} [CommSemiring R] [AddCommMonoid Q] [Module R Q] {I : Submodule R R} : map (↑(TensorProduct.lid R Q)) (LinearMap.rTensor Q I.subtype).range = I • ⊤

theorem TensorProduct.mk_surjective (R : Type u_1) (M : Type u_2) (S : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Algebra R S] (h : Function.Surjective ⇑(algebraMap R S)) : Function.Surjective ⇑((mk R S M) 1)

theorem TensorProduct.flip_mk_surjective {R : Type u_1} (S : Type u_3) {T : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] [Ring T] [Algebra R T] (h : Function.Surjective ⇑(algebraMap R T)) : Function.Surjective ⇑((mk R S T).flip 1)

theorem Algebra.TensorProduct.includeRight_surjective {R : Type u_1} {S : Type u_3} (T : Type u_4) [CommSemiring R] [Semiring S] [Algebra R S] [Ring T] [Algebra R T] (h : Function.Surjective ⇑(algebraMap R S)) : Function.Surjective ⇑includeRight

theorem Algebra.TensorProduct.includeLeft_surjective {R : Type u_1} {T : Type u_4} [CommSemiring R] [Ring T] [Algebra R T] (S : Type u_5) (A : Type u_6) [CommSemiring S] [Semiring A] [Algebra S A] [Algebra R A] [SMulCommClass R S A] (h : Function.Surjective ⇑(algebraMap R T)) : Function.Surjective ⇑includeLeft

@[simp]

theorem TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] : LinearMap.mul' R (TensorProduct R A B) ∘ₗ ↑(tensorTensorTensorComm R A A B B) = map (LinearMap.mul' R A) (LinearMap.mul' R B)

theorem LinearMap.mul'_tensor {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] : mul' R (TensorProduct R A B) = TensorProduct.map (mul' R A) (mul' R B) ∘ₗ ↑(TensorProduct.tensorTensorTensorComm R A B A B)

theorem LinearMap.mulLeft_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] (a : A) (b : B) : mulLeft R (a ⊗ₜ[R] b) = TensorProduct.map (mulLeft R a) (mulLeft R b)

theorem LinearMap.mulRight_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] (a : A) (b : B) : mulRight R (a ⊗ₜ[R] b) = TensorProduct.map (mulRight R a) (mulRight R b)

noncomputable instance TensorProduct.instStarMul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] [StarRing R] [StarRing A] [StarRing B] [StarModule R A] [StarModule R B] : StarMul (TensorProduct R A B)

noncomputable instance TensorProduct.instStarRing {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] [StarRing R] [StarRing A] [StarRing B] [StarModule R A] [StarModule R B] : StarRing (TensorProduct R A B)