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)

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.

Equations

• LinearMap.liftBaseChangeEquiv A = (LinearMap.ringLmapEquivSelf A A (M →ₗ[R] N)).symm.trans (TensorProduct.AlgebraTensorModule.lift.equiv R A A A M N)

@[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

Equations

• LinearMap.liftBaseChange A l = (LinearMap.liftBaseChangeEquiv A) l

@[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

@[implicit_reducible]

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)

Equations

• Algebra.TensorProduct.instOneTensorProduct = { one := 1 ⊗ₜ[R] 1 }

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

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Algebra.TensorProduct.mul = TensorProduct.map₂ (LinearMap.mul R A) (LinearMap.mul R B)

@[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₂)

@[implicit_reducible]

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)

Equations

• Algebra.TensorProduct.instMul = { mul := fun (a b : TensorProduct R A B) => (Algebra.TensorProduct.mul 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₂)

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

@[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

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

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)

@[implicit_reducible]

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)

Equations

• Algebra.TensorProduct.instNonUnitalSemiring = { toNonUnitalNonAssocSemiring := Algebra.TensorProduct.instNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• Algebra.TensorProduct.includeLeftRingHom = { toFun := fun (a : A) => a ⊗ₜ[R] 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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

@[implicit_reducible]

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)

Equations

• Algebra.TensorProduct.leftAlgebra = { toSMul := TensorProduct.leftHasSMul, algebraMap := Algebra.TensorProduct.includeLeftRingHom.comp (algebraMap S A), commutes' := ⋯, smul_def' := ⋯ }

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)

@[implicit_reducible]

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.

Equations

• Algebra.TensorProduct.instAlgebra = inferInstance

@[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.

Equations

• Algebra.TensorProduct.includeLeft = { toRingHom := Algebra.TensorProduct.includeLeftRingHom, commutes' := ⋯ }

@[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.

Equations

• Algebra.TensorProduct.includeRight = { toFun := fun (b : B) => 1 ⊗ₜ[R] b, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[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

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

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

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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)

Equations

• Algebra.TensorProduct.instCommSemiring = { toSemiring := inferInstance, mul_comm := ⋯ }

@[implicit_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

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

@[implicit_reducible]

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)

Equations

• Algebra.TensorProduct.instCommRing = { toRing := inferInstance, mul_comm := ⋯ }

@[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.

Equations

• Algebra.TensorProduct.rightAlgebra = Algebra.TensorProduct.includeRight.toAlgebra' ⋯

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.

Equations

• TensorProduct.Algebra.moduleAux = TensorProduct.lift { toFun := fun (a : A) => a • (Algebra.lsmul R R M).toLinearMap, map_add' := ⋯, map_smul' := ⋯ }

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

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

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)

@[implicit_reducible]

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)

Equations

• TensorProduct.instStarMul = { toInvolutiveStar := TensorProduct.instInvolutiveStar, star_mul := ⋯ }

@[implicit_reducible]

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)

Equations

• TensorProduct.instStarRing = { toStarMul := TensorProduct.instStarMul, star_add := ⋯ }

def AlgHom.liftEquiv (R : Type u_4) (S : Type u_5) (A : Type u_6) (B : Type u_7) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra S B] [Algebra R S] [Algebra R B] [IsScalarTower R S B] : (A →ₐ[R] B) ≃ (TensorProduct R S A →ₐ[S] B)

Universal property of the base change of algebra.

An algebra map from the base change is equivalent to an algebra map over the base ring.

In categorical terms, this is an adjunction between:

1. A ↦ S ⊗[R] A, a functor R-Alg ⥤ S-Alg (the base change).
2. B ↦ B, a functor S-Alg ⥤ R-Alg (the restriction).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgHom.liftEquiv_tmul {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra S B] [Algebra R S] [Algebra R B] [IsScalarTower R S B] (f : A →ₐ[R] B) (s : S) (a : A) : ((liftEquiv R S A B) f) (s ⊗ₜ[R] a) = s • f a

@[simp]

theorem AlgHom.liftEquiv_symm_apply {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra S B] [Algebra R S] [Algebra R B] [IsScalarTower R S B] (f : TensorProduct R S A →ₐ[S] B) (a : A) : ((liftEquiv R S A B).symm f) a = f (1 ⊗ₜ[R] a)

theorem Algebra.TensorProduct.ext_ring {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra S B] [Algebra R S] [Algebra R B] [IsScalarTower R S B] {f g : TensorProduct R S A →ₐ[S] B} (h : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight) : f = g

theorem Algebra.TensorProduct.ext_ring_iff {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra S B] [Algebra R S] [Algebra R B] [IsScalarTower R S B] {f g : TensorProduct R S A →ₐ[S] B} : f = g ↔ (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight