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))
• Algebra.TensorProduct.liftEquiv: a universal property for the tensor product of algebras.

References

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

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

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

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

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

Equations

• LinearMap.baseChange A f = TensorProduct.AlgebraTensorModule.map LinearMap.id f

@[simp]

theorem LinearMap.baseChange_tmul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (a : A) (x : M) : (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] [AddCommMonoid N] [Module R M] [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] [AddCommMonoid N] [Module R M] [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] [AddCommMonoid N] [Module R M] [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] [AddCommMonoid N] [Module R M] [Module R N] (r : R) (f : M →ₗ[R] N) : LinearMap.baseChange A (r • f) = r • LinearMap.baseChange A f

@[simp]

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

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

@[simp]

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

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

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

baseChange as a linear map.

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

Equations

• LinearMap.baseChangeHom R A M N = { toFun := LinearMap.baseChange A, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

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

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

baseChange as an AlgHom.

Equations

• Module.End.baseChangeHom R A M = AlgHom.ofLinearMap (LinearMap.baseChangeHom R A M M) ⋯ ⋯

@[simp]

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

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

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

noncomputable 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]

noncomputable 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) : (LinearMap.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) : (LinearMap.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) : ((LinearMap.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' ∘ₗ LinearMap.liftBaseChange A l = LinearMap.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) : LinearMap.range (LinearMap.liftBaseChange A l) = Submodule.span A ↑(LinearMap.range l)

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

noncomputable 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

noncomputable 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

• Algebra.TensorProduct.instAddCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯

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]

noncomputable 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₂ : A) (b₁ : B) (b₂ : B) : (Algebra.TensorProduct.mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)

noncomputable 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₂ : A) (b₁ : 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} {a₃ : A} {b₁ : B} {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₂ : A} {b₁ : B} {b₂ : B} (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) : Commute (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂)

noncomputable 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

• Algebra.TensorProduct.instNonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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) : (Algebra.TensorProduct.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) : (Algebra.TensorProduct.mul x) (1 ⊗ₜ[R] 1) = x

noncomputable 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

• Algebra.TensorProduct.instNonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

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

noncomputable 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 = NonUnitalSemiring.mk ⋯

noncomputable 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

• Algebra.TensorProduct.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯

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

noncomputable 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) : Algebra.TensorProduct.includeLeftRingHom a = a ⊗ₜ[R] 1

noncomputable 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 = Algebra.mk (Algebra.TensorProduct.includeLeftRingHom.comp (algebraMap S A)) ⋯ ⋯

noncomputable 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

noncomputable 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) : Algebra.TensorProduct.includeLeft a = a ⊗ₜ[R] 1

noncomputable 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) : 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] : Algebra.TensorProduct.includeLeftRingHom.comp (algebraMap R A) = Algebra.TensorProduct.includeRight.comp (algebraMap R B)

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

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

Equations

• Algebra.TensorProduct.instAddCommGroupWithOne = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

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

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

Equations

• Algebra.TensorProduct.instNonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

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

Equations

• Algebra.TensorProduct.instNonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• Algebra.TensorProduct.instNonUnitalRing = NonUnitalRing.mk ⋯

noncomputable 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 = CommSemiring.mk ⋯

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

Equations

• Algebra.TensorProduct.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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 = 1 ⊗ₜ[R] ↑z

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

Equations

• Algebra.TensorProduct.instCommRing = CommRing.mk ⋯

@[reducible, inline]

noncomputable 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' ⋯

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

Equations

• ⋯ = ⋯

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

noncomputable 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) (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (h_one : f (1 ⊗ₜ[R] 1) = 1) : TensorProduct R A B →ₐ[S] C

Build an algebra morphism from a linear map out of a tensor product, and evidence that on pure tensors, it preserves multiplication and the identity.

Note that we state h_one using 1 ⊗ₜ[R] 1 instead of 1 so that lemmas about f applied to pure tensors can be directly applied by the caller (without needing TensorProduct.one_def).

Equations

• Algebra.TensorProduct.algHomOfLinearMapTensorProduct f h_mul h_one = AlgHom.ofLinearMap f h_one ⋯

@[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) (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (h_one : f (1 ⊗ₜ[R] 1) = 1) (x : TensorProduct R A B) : (Algebra.TensorProduct.algHomOfLinearMapTensorProduct f h_mul h_one) x = f x

noncomputable 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) (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (h_one : f (1 ⊗ₜ[R] 1) = 1) : TensorProduct R A B ≃ₐ[S] C

Build an algebra equivalence from a linear equivalence out of a tensor product, and evidence that on pure tensors, it preserves multiplication and the identity.

Note that we state h_one using 1 ⊗ₜ[R] 1 instead of 1 so that lemmas about f applied to pure tensors can be directly applied by the caller (without needing TensorProduct.one_def).

Equations

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

@[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) (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (h_one : f (1 ⊗ₜ[R] 1) = 1) (x : TensorProduct R A B) : (Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct f h_mul h_one) x = f x

noncomputable 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] [Semiring D] [Algebra R D] [Algebra R C] (f : TensorProduct R (TensorProduct R A B) C ≃ₗ[R] D) (h_mul : ∀ (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₂)) (h_one : f ((1 ⊗ₜ[R] 1) ⊗ₜ[R] 1) = 1) : 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.

Equations

• Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct f h_mul h_one = AlgEquiv.ofLinearEquiv f h_one ⋯

@[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] [Semiring D] [Algebra R D] [Algebra R C] (f : TensorProduct R (TensorProduct R A B) C ≃ₗ[R] D) (h_mul : ∀ (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₂)) (h_one : f ((1 ⊗ₜ[R] 1) ⊗ₜ[R] 1) = 1) (x : TensorProduct R (TensorProduct R A B) C) : (Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct f h_mul h_one) x = f x

noncomputable def Algebra.TensorProduct.lift {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] [Algebra R C] [IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)) : TensorProduct R A B →ₐ[S] C

The forward direction of the universal property of tensor products of algebras; any algebra morphism from the tensor product can be factored as the product of two algebra morphisms that commute.

See Algebra.TensorProduct.liftEquiv for the fact that every morphism factors this way.

Equations

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

@[simp]

theorem Algebra.TensorProduct.lift_tmul {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] [Algebra R C] [IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)) (a : A) (b : B) : (Algebra.TensorProduct.lift f g hfg) (a ⊗ₜ[R] b) = f a * g b

@[simp]

theorem Algebra.TensorProduct.lift_includeLeft_includeRight {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [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.TensorProduct.lift Algebra.TensorProduct.includeLeft Algebra.TensorProduct.includeRight ⋯ = AlgHom.id S (TensorProduct R A B)

@[simp]

theorem Algebra.TensorProduct.lift_comp_includeLeft {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] [Algebra R C] [IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)) : (Algebra.TensorProduct.lift f g hfg).comp Algebra.TensorProduct.includeLeft = f

@[simp]

theorem Algebra.TensorProduct.lift_comp_includeRight {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] [Algebra R C] [IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)) : (AlgHom.restrictScalars R (Algebra.TensorProduct.lift f g hfg)).comp Algebra.TensorProduct.includeRight = g

noncomputable def Algebra.TensorProduct.liftEquiv {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] [Algebra R C] [IsScalarTower R S C] : { fg : (A →ₐ[S] C) × (B →ₐ[R] C) // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) } ≃ (TensorProduct R A B →ₐ[S] C)

The universal property of the tensor product of algebras.

Pairs of algebra morphisms that commute are equivalent to algebra morphisms from the tensor product.

This is Algebra.TensorProduct.lift as an equivalence.

See also GradedTensorProduct.liftEquiv for an alternative commutativity requirement for graded algebra.

Equations

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

@[simp]

theorem Algebra.TensorProduct.liftEquiv_symm_apply_coe {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] [Algebra R C] [IsScalarTower R S C] (f' : TensorProduct R A B →ₐ[S] C) : ↑(Algebra.TensorProduct.liftEquiv.symm f') = (f'.comp Algebra.TensorProduct.includeLeft, (AlgHom.restrictScalars R f').comp Algebra.TensorProduct.includeRight)

@[simp]

theorem Algebra.TensorProduct.liftEquiv_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] [Algebra R C] [IsScalarTower R S C] (fg : { fg : (A →ₐ[S] C) × (B →ₐ[R] C) // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }) : Algebra.TensorProduct.liftEquiv fg = Algebra.TensorProduct.lift (↑fg).1 (↑fg).2 ⋯

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

Equations

• Algebra.TensorProduct.lid R A = Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (TensorProduct.lid R A) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.lid_toLinearEquiv (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] : (Algebra.TensorProduct.lid R A).toLinearEquiv = TensorProduct.lid R A

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

@[simp]

theorem Algebra.TensorProduct.lid_symm_apply (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) : (Algebra.TensorProduct.lid R A).symm a = 1 ⊗ₜ[R] a

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

Equations

• Algebra.TensorProduct.rid R S A = Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (TensorProduct.AlgebraTensorModule.rid R S A) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.rid_toLinearEquiv (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] : (Algebra.TensorProduct.rid R S A).toLinearEquiv = TensorProduct.AlgebraTensorModule.rid R 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

@[simp]

theorem Algebra.TensorProduct.rid_symm_apply (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] (a : A) : (Algebra.TensorProduct.rid R S A).symm a = a ⊗ₜ[R] 1

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

Equations

• Algebra.TensorProduct.comm R A B = Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (TensorProduct.comm R A B) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.comm_toLinearEquiv (R : Type uR) (A : Type uA) (B : Type uB) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : (Algebra.TensorProduct.comm R A B).toLinearEquiv = TensorProduct.comm R A B

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

@[simp]

theorem Algebra.TensorProduct.comm_symm_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).symm (b ⊗ₜ[R] a) = a ⊗ₜ[R] b

theorem Algebra.TensorProduct.comm_symm (R : Type uR) (A : Type uA) (B : Type uB) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : (Algebra.TensorProduct.comm R A B).symm = Algebra.TensorProduct.comm R B 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 : TensorProduct R A B | ∃ (a : A) (b : 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] : (TensorProduct.assoc R A B C) ((1 ⊗ₜ[R] 1) ⊗ₜ[R] 1) = 1

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

Equations

• Algebra.TensorProduct.assoc R A B C = Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct (TensorProduct.assoc R A B C) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.assoc_toLinearEquiv (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] : (Algebra.TensorProduct.assoc R A B C).toLinearEquiv = TensorProduct.assoc R A B C

@[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) : (Algebra.TensorProduct.assoc R A B C) ((a ⊗ₜ[R] b) ⊗ₜ[R] c) = a ⊗ₜ[R] b ⊗ₜ[R] c

@[simp]

theorem Algebra.TensorProduct.assoc_symm_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) : (Algebra.TensorProduct.assoc R A B C).symm (a ⊗ₜ[R] b ⊗ₜ[R] c) = (a ⊗ₜ[R] b) ⊗ₜ[R] c

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

Equations

• Algebra.TensorProduct.map f g = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (TensorProduct.AlgebraTensorModule.map f.toLinearMap g.toLinearMap) ⋯ ⋯

@[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] [Semiring D] [Algebra R D] [Semiring E] [Algebra R E] [Semiring F] [Algebra R F] [Algebra S C] [IsScalarTower R S C] (f₂ : B →ₐ[S] C) (f₁ : A →ₐ[S] B) (g₂ : E →ₐ[R] F) (g₁ : D →ₐ[R] E) : Algebra.TensorProduct.map (f₂.comp f₁) (g₂.comp g₁) = (Algebra.TensorProduct.map f₂ g₂).comp (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) : (Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft = Algebra.TensorProduct.includeLeft.comp 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.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight = Algebra.TensorProduct.includeRight.comp 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) : (Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeRight = Algebra.TensorProduct.includeRight.comp 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) : (Algebra.TensorProduct.map f g).range = (Algebra.TensorProduct.includeLeft.comp f).range ⊔ (Algebra.TensorProduct.includeRight.comp g).range

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

Equations

• Algebra.TensorProduct.congr f g = AlgEquiv.ofAlgHom (Algebra.TensorProduct.map ↑f ↑g) (Algebra.TensorProduct.map ↑f.symm ↑g.symm) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.congr_toLinearEquiv {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 f g).toLinearEquiv = TensorProduct.AlgebraTensorModule.congr f.toLinearEquiv g.toLinearEquiv

@[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) : (Algebra.TensorProduct.congr f g).symm x = (Algebra.TensorProduct.map ↑f.symm ↑g.symm) 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] [Semiring D] [Algebra R D] [Semiring E] [Algebra R E] [Semiring F] [Algebra R F] [Algebra S C] [IsScalarTower R S C] (f₁ : A ≃ₐ[S] B) (f₂ : B ≃ₐ[S] C) (g₁ : D ≃ₐ[R] E) (g₂ : E ≃ₐ[R] F) : Algebra.TensorProduct.congr (f₁.trans f₂) (g₁.trans g₂) = (Algebra.TensorProduct.congr f₁ g₁).trans (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 f.symm g.symm = (Algebra.TensorProduct.congr f g).symm

@[reducible, inline]

noncomputable abbrev 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.

This is just a special case of Algebra.TensorProduct.lift for when C is commutative.

Equations

• Algebra.TensorProduct.productLeftAlgHom f g = Algebra.TensorProduct.lift f g ⋯

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

Equations

• Algebra.TensorProduct.lmul' R = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (LinearMap.mul' R S) ⋯ ⋯

theorem Algebra.TensorProduct.lmul'_toLinearMap {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : (Algebra.TensorProduct.lmul' R).toLinearMap = 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] : (Algebra.TensorProduct.lmul' R).comp 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] : (Algebra.TensorProduct.lmul' R).comp Algebra.TensorProduct.includeRight = AlgHom.id R S

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

This is a special case of Algebra.TensorProduct.productLeftAlgHom for when the two base rings are the same.

Equations

• Algebra.TensorProduct.productMap f g = Algebra.TensorProduct.productLeftAlgHom f g

theorem Algebra.TensorProduct.productMap_eq_comp_map {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) : Algebra.TensorProduct.productMap f g = (Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f g)

@[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) : (Algebra.TensorProduct.productMap f g).comp 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) : (Algebra.TensorProduct.productMap f g).comp 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) : (Algebra.TensorProduct.productMap f g).range = f.range ⊔ g.range

noncomputable def Algebra.TensorProduct.basisAux {R : Type uR} (A : Type uA) {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring 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).

Equations

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

theorem Algebra.TensorProduct.basisAux_tmul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring 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) ⋯ (b.repr m)

theorem Algebra.TensorProduct.basisAux_map_smul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring 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ι} [CommSemiring R] [Semiring 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.

Equations

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

@[simp]

theorem Algebra.TensorProduct.basis_repr_tmul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring 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) ⋯ (b.repr m)

theorem Algebra.TensorProduct.basis_repr_symm_apply {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (a : A) (i : ι) : (Algebra.TensorProduct.basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)

@[simp]

theorem Algebra.TensorProduct.basis_apply {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) : (Algebra.TensorProduct.basis A b) i = 1 ⊗ₜ[R] b i

theorem Algebra.TensorProduct.basis_repr_symm_apply' {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring 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

theorem Basis.baseChange_linearMap {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] {ι' : Type u_1} {N : Type u_2} [Fintype ι'] [DecidableEq ι'] [AddCommMonoid N] [Module R N] (A : Type u_3) [CommSemiring A] [Algebra R A] (b : Basis ι R M) (b' : Basis ι' R N) (ij : ι × ι') : LinearMap.baseChange A ((b'.linearMap b) ij) = ((Algebra.TensorProduct.basis A b').linearMap (Algebra.TensorProduct.basis A b)) ij

theorem Basis.baseChange_end {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (A : Type u_3) [CommSemiring A] [Algebra R A] [DecidableEq ι] (b : Basis ι R M) (ij : ι × ι) : LinearMap.baseChange A (b.end ij) = (Algebra.TensorProduct.basis A b).end ij

noncomputable instance Algebra.TensorProduct.instFreeTensorProduct (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [CommSemiring A] [Algebra R A] : Module.Free A (TensorProduct R A M)

Equations

• ⋯ = ⋯

@[simp]

theorem LinearMap.toMatrix_baseChange {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} {ι₂ : Type u_5} (A : Type u_6) [Fintype ι] [Finite ι₂] [DecidableEq ι] [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) : (LinearMap.toMatrix (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂)) (LinearMap.baseChange A f) = ((LinearMap.toMatrix b₁ b₂) f).map ⇑(algebraMap R A)

noncomputable def LinearMap.tensorProduct (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct R A (M →ₗ[R] N) →ₗ[A] TensorProduct R A M →ₗ[A] TensorProduct R A N

The natural linear map $A ⊗ \text{Hom}_R(M, N) → \text{Hom}_A (M_A, N_A)$, where $M_A$ and $N_A$ are the respective modules over $A$ obtained by extension of scalars.

See LinearMap.tensorProductEnd for this map specialized to endomorphisms, and bundled as A-algebra homomorphism.

Equations

• LinearMap.tensorProduct R A M N = TensorProduct.AlgebraTensorModule.lift { toFun := fun (a : A) => a • LinearMap.baseChangeHom R A M N, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.tensorProduct_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : ∀ (a : TensorProduct R A (M →ₗ[R] N)), (LinearMap.tensorProduct R A M N) a = (TensorProduct.liftAux (↑R { toFun := fun (a : A) => a • LinearMap.baseChangeHom R A M N, map_add' := ⋯, map_smul' := ⋯ })) a

noncomputable def LinearMap.tensorProductEnd (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] : TensorProduct R A (Module.End R M) →ₐ[A] Module.End A (TensorProduct R A M)

The natural A-algebra homomorphism $A ⊗ (\text{End}_R M) → \text{End}_A (A ⊗ M)$, where M is an R-module, and A an R-algebra.

Equations

• LinearMap.tensorProductEnd R A M = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (LinearMap.tensorProduct R A M M) ⋯ ⋯

@[simp]

theorem LinearMap.tensorProductEnd_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] (a : TensorProduct R A (Module.End R M)) : (LinearMap.tensorProductEnd R A M) a = (TensorProduct.liftAux (↑R { toFun := fun (a : A) => a • LinearMap.baseChangeHom R A M M, map_add' := ⋯, map_smul' := ⋯ })) a

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

Equations

• Module.endTensorEndAlgHom = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (TensorProduct.AlgebraTensorModule.homTensorHomMap R A S M N M N) ⋯ ⋯

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.finite_sup {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] [Algebra K L] (E1 : Subalgebra K L) (E2 : Subalgebra K L) [Module.Finite K ↥E1] [Module.Finite K ↥E2] : Module.Finite K ↥(E1 ⊔ E2)

noncomputable 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) : (TensorProduct.Algebra.moduleAux (a ⊗ₜ[R] b)) m = a • b • m

noncomputable 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

• TensorProduct.Algebra.module = Module.mk ⋯ ⋯

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