Maps between tensor products of R-algebras

This file provides results about maps between tensor products of R-algebras.

Main declarations

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

def Module.End.lTensorAlgHom (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : End R M →ₐ[R] End R (TensorProduct R N M)

The map LinearMap.lTensorHom which sends f ↦ 1 ⊗ f as a morphism of algebras.

Equations

• Module.End.lTensorAlgHom R M N = AlgHom.ofLinearMap (LinearMap.lTensorHom N) ⋯ ⋯

@[simp]

theorem Module.End.lTensorAlgHom_apply_apply (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (a : End R M) (a✝ : TensorProduct R N M) : ((lTensorAlgHom R M N) a) a✝ = (TensorProduct.liftAux ((TensorProduct.mk R N M).compl₂ a)) a✝

def Module.End.rTensorAlgHom (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : End R M →ₐ[R] End R (TensorProduct R M N)

The map LinearMap.rTensorHom which sends f ↦ f ⊗ 1 as a morphism of algebras.

Equations

• Module.End.rTensorAlgHom R M N = AlgHom.ofLinearMap (LinearMap.rTensorHom N) ⋯ ⋯

@[simp]

theorem Module.End.rTensorAlgHom_apply_apply (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (a : End R M) (a✝ : TensorProduct R M N) : ((rTensorAlgHom R M N) a) a✝ = (TensorProduct.liftAux (TensorProduct.mk R M N ∘ₗ a)) a✝

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

theorem LinearMap.map_mul_of_map_mul_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] {f : TensorProduct R A B →ₗ[S] C} (hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (x y : TensorProduct R A B) : f (x * y) = f x * f y

To check a linear map preserves multiplication, it suffices to check it on pure tensors. See algHomOfLinearMapTensorProduct for a bundled version.

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) : (algHomOfLinearMapTensorProduct f h_mul h_one) x = f x

def Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] (f : TensorProduct R A B ≃ₗ[S] C) (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) : (algEquivOfLinearEquivTensorProduct f h_mul h_one) x = f x

def Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [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) : (algEquivOfLinearEquivTripleTensorProduct f h_mul h_one) x = f x

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) : (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] : lift includeLeft 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)) : (lift f g hfg).comp 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 (lift f g hfg)).comp includeRight = g

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_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) }) : liftEquiv fg = lift (↑fg).1 (↑fg).2 ⋯

@[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) : ↑(liftEquiv.symm f') = (f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight)

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] : (TensorProduct.lid R A).toLinearEquiv = _root_.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) : (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) : (TensorProduct.lid R A).symm a = 1 ⊗ₜ[R] a

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

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

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

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

def Algebra.TensorProduct.mapOfCompatibleSMul (R : Type u_3) (S : Type u_4) (A : Type u_5) (B : Type u_6) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra S A] [Algebra S B] [SMulCommClass R S A] [TensorProduct.CompatibleSMul R S A B] : TensorProduct S A B →ₐ[S] TensorProduct R A B

If A and B are both R- and S-algebras and their actions on them commute, and if the S-action on A ⊗[R] B can switch between the two factors, then there is a canonical S-algebra homomorphism from A ⊗[S] B to A ⊗[R] B.

Equations

• Algebra.TensorProduct.mapOfCompatibleSMul R S A B = AlgHom.ofLinearMap (TensorProduct.mapOfCompatibleSMul R S A B) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.mapOfCompatibleSMul_tmul (R : Type u_3) (S : Type u_4) (A : Type u_5) (B : Type u_6) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra S A] [Algebra S B] [SMulCommClass R S A] [TensorProduct.CompatibleSMul R S A B] (m : A) (n : B) : (mapOfCompatibleSMul R S A B) (m ⊗ₜ[S] n) = m ⊗ₜ[R] n

theorem Algebra.TensorProduct.mapOfCompatibleSMul_surjective (R : Type u_3) (S : Type u_4) (A : Type u_5) (B : Type u_6) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra S A] [Algebra S B] [SMulCommClass R S A] [TensorProduct.CompatibleSMul R S A B] : Function.Surjective ⇑(mapOfCompatibleSMul R S A B)

def Algebra.TensorProduct.mapOfCompatibleSMul' (R : Type u_3) (S : Type u_4) (A : Type u_5) (B : Type u_6) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra S A] [Algebra S B] [SMulCommClass R S A] [TensorProduct.CompatibleSMul R S A B] : TensorProduct S A B →ₐ[R] TensorProduct R A B

mapOfCompatibleSMul R S A B is also A-linear.

Equations

• Algebra.TensorProduct.mapOfCompatibleSMul' R S A B = AlgHom.ofLinearMap (TensorProduct.mapOfCompatibleSMul' R S A B) ⋯ ⋯

def Algebra.TensorProduct.equivOfCompatibleSMul (R : Type u_3) (S : Type u_4) (A : Type u_5) (B : Type u_6) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra S A] [Algebra S B] [SMulCommClass R S A] [TensorProduct.CompatibleSMul R S A B] [TensorProduct.CompatibleSMul S R A B] : TensorProduct S A B ≃ₐ[S] TensorProduct R A B

If the R- and S-actions on A and B satisfy CompatibleSMul both ways, then A ⊗[S] B is canonically isomorphic to A ⊗[R] B.

Equations

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

def Algebra.TensorProduct.lidOfCompatibleSMul (R : Type u_3) (S : Type u_4) (A : Type u_5) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] [Algebra S A] [Algebra R S] [TensorProduct.CompatibleSMul R S S A] [TensorProduct.CompatibleSMul S R S A] : TensorProduct R S A ≃ₐ[S] A

If the R- and S- action on S and A satisfy CompatibleSMul both ways, then S ⊗[R] A is canonically isomorphic to A.

Equations

• Algebra.TensorProduct.lidOfCompatibleSMul R S A = (Algebra.TensorProduct.equivOfCompatibleSMul R S S A).symm.trans (Algebra.TensorProduct.lid S A)

theorem Algebra.TensorProduct.lidOfCompatibleSMul_tmul (R : Type u_3) (S : Type u_4) (A : Type u_5) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] [Algebra S A] [Algebra R S] [TensorProduct.CompatibleSMul R S S A] [TensorProduct.CompatibleSMul S R S A] (s : S) (a : A) : (lidOfCompatibleSMul R S A) (s ⊗ₜ[R] a) = s • a

instance Algebra.TensorProduct.instCompatibleSMulRat {R : Type u_7} {M : Type u_8} {N : Type u_9} [CommSemiring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module ℚ M] [Module ℚ N] : TensorProduct.CompatibleSMul R ℚ M N

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] : (TensorProduct.comm R A B).toLinearEquiv = _root_.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) : (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) : (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] : (TensorProduct.comm R A B).symm = TensorProduct.comm R B A

@[simp]

theorem Algebra.TensorProduct.comm_comp_includeLeft (R : Type uR) (A : Type uA) (B : Type uB) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : (↑(TensorProduct.comm R A B)).comp includeLeft = includeRight

@[simp]

theorem Algebra.TensorProduct.comm_comp_includeRight (R : Type uR) (A : Type uA) (B : Type uB) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : (↑(TensorProduct.comm R A B)).comp includeRight = includeLeft

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] : 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) (b₁ b₂ : B) (c₁ c₂ : C) : (_root_.TensorProduct.assoc R A B C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = (_root_.TensorProduct.assoc R A B C) (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * (_root_.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] : (_root_.TensorProduct.assoc R A B C) (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) = 1

def Algebra.TensorProduct.assoc (R : Type uR) (S : Type uS) (A : Type uA) (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 C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] : TensorProduct R (TensorProduct S A C) D ≃ₐ[S] TensorProduct S A (TensorProduct R C D)

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

Equations

• Algebra.TensorProduct.assoc R S A C D = AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.assoc R S S A C D) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.assoc_toLinearEquiv (R : Type uR) (S : Type uS) (A : Type uA) (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 C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] : (TensorProduct.assoc R S A C D).toLinearEquiv = TensorProduct.AlgebraTensorModule.assoc R S S A C D

@[simp]

theorem Algebra.TensorProduct.assoc_tmul (R : Type uR) (S : Type uS) {A : Type uA} {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 C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (a : A) (b : C) (c : D) : (TensorProduct.assoc R S A C D) (a ⊗ₜ[S] b ⊗ₜ[R] c) = a ⊗ₜ[S] (b ⊗ₜ[R] c)

@[simp]

theorem Algebra.TensorProduct.assoc_symm_tmul (R : Type uR) (S : Type uS) {A : Type uA} {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 C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (a : A) (b : C) (c : D) : (TensorProduct.assoc R S A C D).symm (a ⊗ₜ[S] (b ⊗ₜ[R] c)) = a ⊗ₜ[S] b ⊗ₜ[R] c

def Algebra.TensorProduct.cancelBaseChange (R : Type uR) (S : Type uS) [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Type u_3) (A : Type u_4) (B : Type u_5) [CommSemiring T] [CommSemiring A] [CommSemiring B] [Algebra R T] [Algebra R A] [Algebra R B] [Algebra T A] [IsScalarTower R T A] [Algebra S A] [IsScalarTower R S A] [Algebra S T] [IsScalarTower S T A] : TensorProduct S A (TensorProduct R S B) ≃ₐ[T] TensorProduct R A B

The natural isomorphism A ⊗[S] (S ⊗[R] B) ≃ₐ[T] A ⊗[R] B.

Equations

• Algebra.TensorProduct.cancelBaseChange R S T A B = (AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.cancelBaseChange R S T A B).symm ⋯ ⋯).symm

@[simp]

theorem Algebra.TensorProduct.cancelBaseChange_tmul (R : Type uR) (S : Type uS) [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Type u_3) (A : Type u_4) (B : Type u_5) [CommSemiring T] [CommSemiring A] [CommSemiring B] [Algebra R T] [Algebra R A] [Algebra R B] [Algebra T A] [IsScalarTower R T A] [Algebra S A] [IsScalarTower R S A] [Algebra S T] [IsScalarTower S T A] (a : A) (s : S) (b : B) : (cancelBaseChange R S T A B) (a ⊗ₜ[S] (s ⊗ₜ[R] b)) = (s • a) ⊗ₜ[R] b

@[simp]

theorem Algebra.TensorProduct.cancelBaseChange_symm_tmul (R : Type uR) (S : Type uS) [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Type u_3) (A : Type u_4) (B : Type u_5) [CommSemiring T] [CommSemiring A] [CommSemiring B] [Algebra R T] [Algebra R A] [Algebra R B] [Algebra T A] [IsScalarTower R T A] [Algebra S A] [IsScalarTower R S A] [Algebra S T] [IsScalarTower S T A] (a : A) (b : B) : (cancelBaseChange R S T A B).symm (a ⊗ₜ[R] b) = a ⊗ₜ[S] (1 ⊗ₜ[R] b)

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] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) : TensorProduct R A B →ₐ[S] TensorProduct R C 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] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) (a : A) (b : B) : (map f g) (a ⊗ₜ[R] b) = f a ⊗ₜ[R] g b

@[simp]

theorem Algebra.TensorProduct.map_id {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] : map (AlgHom.id S A) (AlgHom.id R B) = AlgHom.id S (TensorProduct R A B)

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

theorem Algebra.TensorProduct.map_id_comp {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {D : Type uD} {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] [Semiring D] [Algebra R D] [Semiring F] [Algebra R F] (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D) : map (AlgHom.id S A) (g₂.comp g₁) = (map (AlgHom.id S A) g₂).comp (map (AlgHom.id S A) g₁)

theorem Algebra.TensorProduct.map_comp_id {R : Type uR} {S : Type uS} {A : Type uA} {C : Type uC} {E : Type uE} [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 S C] [IsScalarTower R S C] [Semiring E] [Algebra R E] [Algebra S E] [IsScalarTower R S E] (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C) : map (f₂.comp f₁) (AlgHom.id R E) = (map f₂ (AlgHom.id R E)).comp (map f₁ (AlgHom.id 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} [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 R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) : (map f g).comp includeLeft = 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] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) : (AlgHom.restrictScalars R (map f g)).comp includeRight = 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] C) (g : B →ₐ[R] D) : (map f g).comp includeRight = 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] C) (g : B →ₐ[R] D) : (map f g).range = (includeLeft.comp f).range ⊔ (includeRight.comp g).range

theorem Algebra.TensorProduct.comm_comp_map {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] C) (g : B →ₐ[R] D) : (↑(TensorProduct.comm R C D)).comp (map f g) = (map g f).comp ↑(TensorProduct.comm R A B)

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

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

@[simp]

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

def Algebra.TensorProduct.leftComm (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 A (TensorProduct R B C) ≃ₐ[R] TensorProduct R B (TensorProduct R A C)

Tensor product of algebras analogue of mul_left_comm.

This is the algebra version of TensorProduct.leftComm.

Equations

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

@[simp]

theorem Algebra.TensorProduct.leftComm_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] (m : A) (n : B) (p : C) : (leftComm R A B C) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = n ⊗ₜ[R] (m ⊗ₜ[R] p)

@[simp]

theorem Algebra.TensorProduct.leftComm_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] (m : A) (n : B) (p : C) : (leftComm R A B C).symm (n ⊗ₜ[R] (m ⊗ₜ[R] p)) = m ⊗ₜ[R] (n ⊗ₜ[R] p)

@[simp]

theorem Algebra.TensorProduct.leftComm_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] : ↑(leftComm R A B C) = _root_.TensorProduct.leftComm R A B C

def Algebra.TensorProduct.tensorTensorTensorComm (R : Type uR) (R' : Type u_1) (S : Type uS) (T : Type u_2) (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] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] [CommSemiring T] [Algebra R T] [Algebra T A] [IsScalarTower R T A] [SMulCommClass S T A] [Algebra S T] [IsScalarTower S T A] [CommSemiring R'] [Algebra R R'] [Algebra R' T] [Algebra R' A] [Algebra R' B] [IsScalarTower R R' A] [SMulCommClass S R' A] [SMulCommClass R' S A] [IsScalarTower R' T A] [IsScalarTower R R' B] : TensorProduct S (TensorProduct R' A B) (TensorProduct R C D) ≃ₐ[T] TensorProduct R' (TensorProduct S A C) (TensorProduct R B D)

Tensor product of algebras analogue of mul_mul_mul_comm.

This is the algebra version of TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.

Equations

• Algebra.TensorProduct.tensorTensorTensorComm R R' S T A B C D = AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.tensorTensorTensorComm_tmul {R : Type uR} {R' : Type u_1} {S : Type uS} {T : Type u_2} {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] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] [CommSemiring T] [Algebra R T] [Algebra T A] [IsScalarTower R T A] [SMulCommClass S T A] [Algebra S T] [IsScalarTower S T A] [CommSemiring R'] [Algebra R R'] [Algebra R' T] [Algebra R' A] [Algebra R' B] [IsScalarTower R R' A] [SMulCommClass S R' A] [SMulCommClass R' S A] [IsScalarTower R' T A] [IsScalarTower R R' B] (m : A) (n : B) (p : C) (q : D) : (tensorTensorTensorComm R R' S T A B C D) (m ⊗ₜ[R'] n ⊗ₜ[S] (p ⊗ₜ[R] q)) = m ⊗ₜ[S] p ⊗ₜ[R'] (n ⊗ₜ[R] q)

@[simp]

theorem Algebra.TensorProduct.tensorTensorTensorComm_symm_tmul {R : Type uR} {R' : Type u_1} {S : Type uS} {T : Type u_2} {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] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] [CommSemiring T] [Algebra R T] [Algebra T A] [IsScalarTower R T A] [SMulCommClass S T A] [Algebra S T] [IsScalarTower S T A] [CommSemiring R'] [Algebra R R'] [Algebra R' T] [Algebra R' A] [Algebra R' B] [IsScalarTower R R' A] [SMulCommClass S R' A] [SMulCommClass R' S A] [IsScalarTower R' T A] [IsScalarTower R R' B] (m : A) (n : C) (p : B) (q : D) : (tensorTensorTensorComm R R' S T A B C D).symm (m ⊗ₜ[S] n ⊗ₜ[R'] (p ⊗ₜ[R] q)) = m ⊗ₜ[R'] p ⊗ₜ[S] (n ⊗ₜ[R] q)

theorem Algebra.TensorProduct.tensorTensorTensorComm_symm {R : Type uR} {R' : Type u_1} {S : Type uS} {T : Type u_2} {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] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] [CommSemiring T] [Algebra R T] [Algebra T A] [IsScalarTower R T A] [SMulCommClass S T A] [Algebra S T] [IsScalarTower S T A] [CommSemiring R'] [Algebra R R'] [Algebra R' T] [Algebra R' A] [Algebra R' B] [IsScalarTower R R' A] [SMulCommClass S R' A] [SMulCommClass R' S A] [IsScalarTower R' T A] [IsScalarTower R R' B] : (tensorTensorTensorComm R R' S T A B C D).symm = tensorTensorTensorComm R S R' T A C B D

theorem Algebra.TensorProduct.tensorTensorTensorComm_toLinearEquiv {R : Type uR} {R' : Type u_1} {S : Type uS} {T : Type u_2} {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] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] [CommSemiring T] [Algebra R T] [Algebra T A] [IsScalarTower R T A] [SMulCommClass S T A] [Algebra S T] [IsScalarTower S T A] [CommSemiring R'] [Algebra R R'] [Algebra R' T] [Algebra R' A] [Algebra R' B] [IsScalarTower R R' A] [SMulCommClass S R' A] [SMulCommClass R' S A] [IsScalarTower R' T A] [IsScalarTower R R' B] : (tensorTensorTensorComm R R' S T A B C D).toLinearEquiv = TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D

@[simp]

theorem Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorComm {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] : (tensorTensorTensorComm R R R R A B C D).toLinearEquiv = _root_.TensorProduct.tensorTensorTensorComm R A B C D

theorem Algebra.TensorProduct.map_bijective {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} (hf : Function.Bijective ⇑f) (hg : Function.Bijective ⇑g) : Function.Bijective ⇑(map f g)

theorem Algebra.TensorProduct.includeLeft_bijective {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] (h : Function.Bijective ⇑(algebraMap R B)) : Function.Bijective ⇑includeLeft

theorem Algebra.TensorProduct.includeRight_bijective {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (h : Function.Bijective ⇑(algebraMap R A)) : Function.Bijective ⇑includeRight

@[reducible, inline]

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 ⋯

theorem Algebra.TensorProduct.tmul_one_eq_one_tmul {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 A) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r

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

LinearMap.mul' as an AlgHom over the algebra.

Equations

• Algebra.TensorProduct.lmul'' R = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (let __spread.0 := LinearMap.mul' R S; { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }) ⋯ ⋯

theorem Algebra.TensorProduct.lmul''_eq_lid_comp_mapOfCompatibleSMul (R : Type uR) {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : lmul'' R = (↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul' S R S S)

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' as an AlgHom over the base ring.

Equations

• Algebra.TensorProduct.lmul' R = AlgHom.restrictScalars R (Algebra.TensorProduct.lmul'' R)

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

theorem Algebra.TensorProduct.lmul'_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) : (lmul' R).comp (map f g) = lift f g ⋯

def Algebra.TensorProduct.lmulEquiv (R : Type uR) (S : Type uS) [CommSemiring R] [CommSemiring S] [Algebra R S] [TensorProduct.CompatibleSMul R S S S] : TensorProduct R S S ≃ₐ[S] S

If multiplication by elements of S can switch between the two factors of S ⊗[R] S, then lmul'' is an isomorphism.

Equations

• Algebra.TensorProduct.lmulEquiv R S = AlgEquiv.ofAlgHom (Algebra.TensorProduct.lmul'' R) Algebra.TensorProduct.includeLeft ⋯ ⋯

theorem Algebra.TensorProduct.lmulEquiv_eq_lidOfCompatibleSMul {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] [TensorProduct.CompatibleSMul R S S S] : lmulEquiv R S = lidOfCompatibleSMul R S S

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

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

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) : productMap f g = (lmul' R).comp (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) : (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) : (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) : (productMap f g).comp 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) : (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) : (productMap f g).comp 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) : (productMap f g).range = f.range ⊔ g.range

def LinearMap.tensorProduct (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid 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) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (a✝ : TensorProduct R A (M →ₗ[R] N)) : (tensorProduct R A M N) a✝ = (TensorProduct.liftAux (↑R { toFun := fun (a : A) => a • baseChangeHom R A M N, map_add' := ⋯, map_smul' := ⋯ })) a✝

def LinearMap.tensorProductEnd (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid 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) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (a : TensorProduct R A (Module.End R M)) : (tensorProductEnd R A M) a = (TensorProduct.liftAux (↑R { toFun := fun (a : A) => a • baseChangeHom R A M M, map_add' := ⋯, map_smul' := ⋯ })) a

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 (End A M) (End R N) →ₐ[S] 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 : End A M) (g : End R N) : endTensorEndAlgHom (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g