# Documentation

Mathlib.RingTheory.TensorProduct

# The tensor product of R-algebras #

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

## Main declarations #

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

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

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

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

Instances For
@[simp]
theorem LinearMap.baseChange_tmul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [] [] [Algebra R A] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) (a : A) (x : M) :
↑() (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} [] [] [Algebra R A] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) :
↑() = ↑()
@[simp]
theorem LinearMap.baseChange_add {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [] [] [Algebra R A] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) (g : M →ₗ[R] N) :
@[simp]
theorem LinearMap.baseChange_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [] [] [Algebra R A] [] [Module R M] [] [Module R N] :
@[simp]
theorem LinearMap.baseChange_smul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [] [] [Algebra R A] [] [Module R M] [] [Module R N] (r : R) (f : M →ₗ[R] N) :
@[simp]
theorem LinearMap.baseChangeHom_apply (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [] [] [Algebra R A] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) :
↑() f =
def LinearMap.baseChangeHom (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [] [] [Algebra R A] [] [Module R M] [] [Module R N] :

baseChange as a linear map.

Instances For
@[simp]
theorem LinearMap.baseChange_sub {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [] [Ring A] [Algebra R A] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) (g : M →ₗ[R] N) :
@[simp]
theorem LinearMap.baseChange_neg {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [] [Ring A] [Algebra R A] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) :

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

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

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

Instances For
@[simp]
theorem Algebra.TensorProduct.mulAux_apply {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) :
↑() (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
def Algebra.TensorProduct.mul {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :

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

Instances For
@[simp]
theorem Algebra.TensorProduct.mul_apply {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) :
↑(Algebra.TensorProduct.mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
theorem Algebra.TensorProduct.mul_assoc {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (x : ) (y : ) (z : ) :
↑(Algebra.TensorProduct.mul (↑(Algebra.TensorProduct.mul x) y)) z = ↑(Algebra.TensorProduct.mul x) (↑(Algebra.TensorProduct.mul y) z)
theorem Algebra.TensorProduct.one_mul {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (x : ) :
↑(Algebra.TensorProduct.mul (1 ⊗ₜ[R] 1)) x = x
theorem Algebra.TensorProduct.mul_one {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (x : ) :
↑(Algebra.TensorProduct.mul x) (1 ⊗ₜ[R] 1) = x
theorem Algebra.TensorProduct.one_def {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :
1 = 1 ⊗ₜ[R] 1
theorem Algebra.TensorProduct.natCast_def {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (n : ) :
n = n ⊗ₜ[R] 1
instance Algebra.TensorProduct.instMul {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :
Mul ()
@[simp]
theorem Algebra.TensorProduct.tmul_mul_tmul {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) :
a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
instance Algebra.TensorProduct.instSemiring {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :
@[simp]
theorem Algebra.TensorProduct.tmul_pow {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (a : A) (b : B) (k : ) :
a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
@[simp]
theorem Algebra.TensorProduct.includeLeftRingHom_apply {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] (a : A) :
Algebra.TensorProduct.includeLeftRingHom a = a ⊗ₜ[R] 1
def Algebra.TensorProduct.includeLeftRingHom {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :

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

Instances For
instance Algebra.TensorProduct.isScalarTower_right {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] [] [] [] [] :
instance Algebra.TensorProduct.sMulCommClass_right {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] [] [] [] [] :
instance Algebra.TensorProduct.leftAlgebra {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra S A] [] :
Algebra S ()
instance Algebra.TensorProduct.instAlgebra {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :
Algebra R ()

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

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

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

Instances For
@[simp]
theorem Algebra.TensorProduct.includeLeft_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra S A] [] (a : A) :
Algebra.TensorProduct.includeLeft a = a ⊗ₜ[R] 1
def Algebra.TensorProduct.includeRight {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :

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

Instances For
@[simp]
theorem Algebra.TensorProduct.includeRight_apply {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [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} [] [] [Algebra R A] [] [Algebra R B] :
RingHom.comp Algebra.TensorProduct.includeLeftRingHom () = RingHom.comp (Algebra.TensorProduct.includeRight) ()
theorem Algebra.TensorProduct.ext {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] [] [Algebra S A] [Algebra R S] [Algebra S C] [] [] ⦃f : →ₐ[S] C ⦃g : →ₐ[S] C (ha : AlgHom.comp f Algebra.TensorProduct.includeLeft = AlgHom.comp g Algebra.TensorProduct.includeLeft) (hb : AlgHom.comp () Algebra.TensorProduct.includeRight = AlgHom.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} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] [] [Algebra S A] [Algebra R S] [Algebra S C] [] [] {g : →ₐ[S] C} {h : →ₐ[S] C} (H : ∀ (a : A) (b : B), g (a ⊗ₜ[R] b) = h (a ⊗ₜ[R] b)) :
g = h
instance Algebra.TensorProduct.instRing {R : Type uR} {A : Type uA} {B : Type uB} [] [Ring A] [Algebra R A] [Ring B] [Algebra R B] :
Ring ()
theorem Algebra.TensorProduct.intCast_def {R : Type uR} {A : Type uA} {B : Type uB} [] [Ring A] [Algebra R A] [Ring B] [Algebra R B] (z : ) :
z = z ⊗ₜ[R] 1
instance Algebra.TensorProduct.instCommRing {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :
@[reducible]
def Algebra.TensorProduct.rightAlgebra {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :
Algebra 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.

Instances For
instance Algebra.TensorProduct.right_isScalarTower {R : Type uR} {A : Type uA} {B : Type uB} [] [] [Algebra R A] [] [Algebra R B] :

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

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

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

Instances For
@[simp]
theorem Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [] [Algebra S C] (f : →ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : S), f (↑() r ⊗ₜ[R] 1) = ↑() r) (x : ) :
= f x
def Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [] [Algebra S C] (f : ≃ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : S), f (↑() r ⊗ₜ[R] 1) = ↑() r) :

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

Instances For
@[simp]
theorem Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [] [Algebra S C] (f : ≃ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : S), f (↑() r ⊗ₜ[R] 1) = ↑() r) (x : ) :
= f x
def Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] [] [Algebra R D] (f : TensorProduct R () C ≃ₗ[R] D) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C), f (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = f ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * f ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂)) (w₂ : ∀ (r : R), f ((↑() r ⊗ₜ[R] 1) ⊗ₜ[R] 1) = ↑() r) :

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

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

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

Instances For
@[simp]
theorem Algebra.TensorProduct.lid_tmul (R : Type uR) (A : Type uA) [] [] [Algebra R A] (r : R) (a : A) :
↑() (r ⊗ₜ[R] a) = r a
def Algebra.TensorProduct.rid (R : Type uR) (S : Type uS) (A : Type uA) [] [] [Algebra R S] [] [Algebra R A] [Algebra 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.

Instances For
@[simp]
theorem Algebra.TensorProduct.rid_tmul {R : Type uR} (S : Type uS) {A : Type uA} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] (r : R) (a : A) :
↑() (a ⊗ₜ[R] r) = r a
def Algebra.TensorProduct.comm (R : Type uR) (A : Type uA) (B : Type uB) [] [] [Algebra R A] [] [Algebra R B] :

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

Instances For
@[simp]
theorem Algebra.TensorProduct.comm_tmul (R : Type uR) (A : Type uA) (B : Type uB) [] [] [Algebra R A] [] [Algebra R B] (a : A) (b : B) :
↑() (a ⊗ₜ[R] b) = b ⊗ₜ[R] a
theorem Algebra.TensorProduct.adjoin_tmul_eq_top (R : Type uR) (A : Type uA) (B : Type uB) [] [] [Algebra R A] [] [Algebra R B] :
Algebra.adjoin R {t | a b, a ⊗ₜ[R] b = t} =
theorem Algebra.TensorProduct.assoc_aux_1 {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) (c₁ : C) (c₂ : C) :
↑() (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = ↑() ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * ↑() ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂)
theorem Algebra.TensorProduct.assoc_aux_2 {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (r : R) :
↑() ((↑() r ⊗ₜ[R] 1) ⊗ₜ[R] 1) = ↑(algebraMap R (TensorProduct R A ())) r
def Algebra.TensorProduct.assoc {R : Type uR} (A : Type uA) (B : Type uB) (C : Type uC) [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] :

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

Instances For
@[simp]
theorem Algebra.TensorProduct.assoc_tmul {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (a : A) (b : B) (c : C) :
↑() ((a ⊗ₜ[R] b) ⊗ₜ[R] c) = a ⊗ₜ[R] b ⊗ₜ[R] c
def Algebra.TensorProduct.map {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [] [Algebra R D] (f : A →ₐ[S] B) (g : C →ₐ[R] D) :

The tensor product of a pair of algebra morphisms.

Instances For
@[simp]
theorem Algebra.TensorProduct.map_tmul {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [] [Algebra R D] (f : A →ₐ[S] B) (g : C →ₐ[R] D) (a : A) (c : C) :
↑() (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} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R 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} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [Algebra S C] [] [] [Algebra R D] [] [Algebra R E] [] [Algebra R F] (f₂ : B →ₐ[S] C) (f₁ : A →ₐ[S] B) (g₂ : E →ₐ[R] F) (g₁ : D →ₐ[R] E) :
@[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} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [] [Algebra R D] (f : A →ₐ[S] B) (g : C →ₐ[R] D) :
AlgHom.comp () Algebra.TensorProduct.includeLeft = AlgHom.comp Algebra.TensorProduct.includeLeft f
@[simp]
theorem Algebra.TensorProduct.map_restrictScalars_comp_includeRight {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [] [Algebra R D] (f : A →ₐ[S] B) (g : C →ₐ[R] D) :
AlgHom.comp () Algebra.TensorProduct.includeRight = AlgHom.comp Algebra.TensorProduct.includeRight g
@[simp]
theorem Algebra.TensorProduct.map_comp_includeRight {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] [] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
AlgHom.comp () Algebra.TensorProduct.includeRight = AlgHom.comp Algebra.TensorProduct.includeRight g
theorem Algebra.TensorProduct.map_range {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] [] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
= AlgHom.range (AlgHom.comp Algebra.TensorProduct.includeLeft f) AlgHom.range (AlgHom.comp Algebra.TensorProduct.includeRight g)
def Algebra.TensorProduct.congr {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [] [Algebra R D] (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) :

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

Instances For
@[simp]
theorem Algebra.TensorProduct.congr_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [] [Algebra R D] (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) (x : ) :
↑() x = ↑() 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} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [] [Algebra R D] (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) (x : ) :
↑() x = ↑() x
@[simp]
theorem Algebra.TensorProduct.congr_refl {R : Type uR} {S : Type uS} {A : Type uA} {C : Type uC} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [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} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [Algebra S C] [] [] [Algebra R D] [] [Algebra R E] [] [Algebra R F] (f₁ : A ≃ₐ[S] B) (f₂ : B ≃ₐ[S] C) (g₁ : D ≃ₐ[R] E) (g₂ : E ≃ₐ[R] F) :
theorem Algebra.TensorProduct.congr_symm {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [Algebra S B] [] [] [Algebra R C] [] [Algebra R D] (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) :
def Algebra.TensorProduct.lmul' (R : Type uR) {S : Type uS} [] [] [Algebra R S] :

LinearMap.mul' is an AlgHom on commutative rings.

Instances For
theorem Algebra.TensorProduct.lmul'_toLinearMap {R : Type uR} {S : Type uS} [] [] [Algebra R S] :
@[simp]
theorem Algebra.TensorProduct.lmul'_apply_tmul {R : Type uR} {S : Type uS} [] [] [Algebra R S] (a : S) (b : S) :
↑() (a ⊗ₜ[R] b) = a * b
@[simp]
theorem Algebra.TensorProduct.lmul'_comp_includeLeft {R : Type uR} {S : Type uS} [] [] [Algebra R S] :
AlgHom.comp () Algebra.TensorProduct.includeLeft =
@[simp]
theorem Algebra.TensorProduct.lmul'_comp_includeRight {R : Type uR} {S : Type uS} [] [] [Algebra R S] :
AlgHom.comp () Algebra.TensorProduct.includeRight =
def Algebra.TensorProduct.productMap {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : 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).

Instances For
@[simp]
theorem Algebra.TensorProduct.productMap_apply_tmul {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (a : A) (b : B) :
↑() (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} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (a : A) :
↑() (a ⊗ₜ[R] 1) = f a
@[simp]
theorem Algebra.TensorProduct.productMap_left {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) :
AlgHom.comp () Algebra.TensorProduct.includeLeft = f
theorem Algebra.TensorProduct.productMap_right_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (b : B) :
↑() (1 ⊗ₜ[R] b) = g b
@[simp]
theorem Algebra.TensorProduct.productMap_right {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) :
AlgHom.comp () Algebra.TensorProduct.includeRight = g
theorem Algebra.TensorProduct.productMap_range {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) :
@[simp]
theorem Algebra.TensorProduct.productLeftAlgHom_apply {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [] [Algebra R C] [Algebra S C] [] (f : A →ₐ[S] C) (g : B →ₐ[R] C) :
∀ (a : ), = ↑() (↑() a)
def Algebra.TensorProduct.productLeftAlgHom {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [] [] [Algebra R S] [] [Algebra R A] [Algebra S A] [] [] [Algebra R B] [] [Algebra R C] [Algebra S C] [] (f : A →ₐ[S] C) (g : B →ₐ[R] 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.

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

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

Instances For
theorem Algebra.TensorProduct.basisAux_tmul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [] [Ring A] [Algebra R A] [] [Module R M] (b : Basis ι R M) (a : A) (m : M) :
↑() (a ⊗ₜ[R] m) = a Finsupp.mapRange ↑() (_ : ↑() 0 = 0) (b.repr m)
theorem Algebra.TensorProduct.basisAux_map_smul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [] [Ring A] [Algebra R A] [] [Module R M] (b : Basis ι R M) (a : A) (x : ) :
↑() (a x) = a ↑() x
noncomputable def Algebra.TensorProduct.basis {R : Type uR} (A : Type uA) {M : Type uM} {ι : Type uι} [] [Ring A] [Algebra R A] [] [Module R M] (b : Basis ι R M) :
Basis ι A ()

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

Instances For
@[simp]
theorem Algebra.TensorProduct.basis_repr_tmul {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [] [Ring A] [Algebra R A] [] [Module R M] (b : Basis ι R M) (a : A) (m : M) :
().repr (a ⊗ₜ[R] m) = a Finsupp.mapRange ↑() (_ : ↑() 0 = 0) (b.repr m)
theorem Algebra.TensorProduct.basis_repr_symm_apply {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [] [Ring A] [Algebra R A] [] [Module R M] (b : Basis ι R M) (a : A) (i : ι) :
(↑(LinearEquiv.symm ().repr) fun₀ | i => a) = a ⊗ₜ[R] ↑(LinearEquiv.symm b.repr) fun₀ | i => 1
@[simp]
theorem Algebra.TensorProduct.basis_repr_symm_apply' {R : Type uR} {A : Type uA} {M : Type uM} {ι : Type uι} [] [Ring A] [Algebra R A] [] [Module R M] (b : Basis ι R M) (a : A) (i : ι) :
a ↑() i = a ⊗ₜ[R] b i
def Module.endTensorEndAlgHom {R : Type u_1} {S : Type u_2} {A : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [Module R M] [Module S M] [Module A M] [Module R 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.

Instances For
theorem Module.endTensorEndAlgHom_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [Module R M] [Module S M] [Module A M] [Module R N] [] [] [] (f : ) (g : ) :
Module.endTensorEndAlgHom (f ⊗ₜ[R] g) =
theorem Subalgebra.finiteDimensional_sup {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (E1 : ) (E2 : ) [FiniteDimensional K { x // x E1 }] [FiniteDimensional K { x // x E2 }] :
FiniteDimensional K { x // x E1 E2 }
def TensorProduct.Algebra.moduleAux {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [] [] [Module R M] [] [] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [] [] :

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

Instances For
theorem TensorProduct.Algebra.moduleAux_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [] [] [Module R M] [] [] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [] [] (a : A) (b : B) (m : M) :
↑(TensorProduct.Algebra.moduleAux (a ⊗ₜ[R] b)) m = a b m
def TensorProduct.Algebra.module {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [] [] [Module R M] [] [] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [] [] [] :
Module () 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

Instances For
theorem TensorProduct.Algebra.smul_def {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [] [] [Module R M] [] [] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [] [] [] (a : A) (b : B) (m : M) :
a ⊗ₜ[R] b m = a b m