feat(RingTheory/TensorProduct): the universal property of the tensor …

…product of algebras (#7409)

The construction used for `CliffordAlgebra.ofBaseChange` generalizes into a universal property for building arbitrary algebra morphisms out of the tensor product.

It turns out this is a known result; it is mentioned at https://en.wikipedia.org/wiki/Tensor_product_of_algebras#Further_properties which cites the linked reference, though the version added by this PR is heterobasic like the rest of this file.

This is a generalization of the existing `Algebra.TensorProduct.productLeftAlgHom` to non-commutative rings.

Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

@@ -61,31 +61,19 @@ module. -/
 -- `noncomputable` is a performance workaround for mathlib4#7103
 noncomputable def ofBaseChange (Q : QuadraticForm R V) :
     A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) :=
-  Algebra.TensorProduct.algHomOfLinearMapTensorProduct
-    (TensorProduct.AlgebraTensorModule.lift <|
-      let f : A →ₗ[A] _ := (Algebra.lsmul A A (CliffordAlgebra (Q.baseChange A))).toLinearMap
-      LinearMap.flip <| LinearMap.flip (({
-        toFun := fun f : CliffordAlgebra (Q.baseChange A) →ₗ[A] CliffordAlgebra (Q.baseChange A) =>
-          LinearMap.restrictScalars R f
-        map_add' := fun f g => LinearMap.ext fun x => rfl
-        map_smul' := fun (c : A) g => LinearMap.ext fun x => rfl
-      } : _ →ₗ[A] _) ∘ₗ f) ∘ₗ (ofBaseChangeAux A Q).toLinearMap)
-    (fun z₁ z₂ b₁ b₂ =>
-      show (z₁ * z₂) • ofBaseChangeAux A Q (b₁ * b₂)
-        = z₁ • ofBaseChangeAux A Q b₁ * z₂ • ofBaseChangeAux A Q b₂
-      by rw [map_mul, smul_mul_smul])
-    (show (1 : A) • ofBaseChangeAux A Q 1 = 1
-      by rw [map_one, one_smul])
+  Algebra.TensorProduct.lift (Algebra.ofId _ _) (ofBaseChangeAux A Q)
+    fun _a _x => Algebra.commutes _ _
 
 @[simp] theorem ofBaseChange_tmul_ι (Q : QuadraticForm R V) (z : A) (v : V) :
     ofBaseChange A Q (z ⊗ₜ ι Q v) = ι (Q.baseChange A) (z ⊗ₜ v) := by
-  show z • ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v)
-  rw [ofBaseChangeAux_ι, ←map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
+  show algebraMap _ _ z * ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v)
+  rw [ofBaseChangeAux_ι, ←Algebra.smul_def, ←map_smul, TensorProduct.smul_tmul', smul_eq_mul,
+    mul_one]
 
 @[simp] theorem ofBaseChange_tmul_one (Q : QuadraticForm R V) (z : A) :
     ofBaseChange A Q (z ⊗ₜ 1) = algebraMap _ _ z := by
-  show z • ofBaseChangeAux A Q 1 = _
-  rw [map_one, ←Algebra.algebraMap_eq_smul_one]
+  show algebraMap _ _ z * ofBaseChangeAux A Q 1 = _
+  rw [map_one, mul_one]
 
 /-- Convert from the clifford algebra over a base-changed module to the base-changed clifford
 algebra. -/

Mathlib/RingTheory/TensorProduct.lean

@@ -28,6 +28,11 @@ multiplication is characterized by `(a₁ ⊗ₜ b₁) * (a₂ ⊗ₜ b₂) = (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)][kasselTensorProducts1995]
 
 -/
 
@@ -228,6 +233,16 @@ theorem tmul_mul_tmul (a₁ a₂ : A) (b₁ b₂ : B) :
   rfl
 #align algebra.tensor_product.tmul_mul_tmul Algebra.TensorProduct.tmul_mul_tmul
 
+theorem _root_.SemiconjBy.tmul {a₁ a₂ a₃ : A} {b₁ b₂ b₃ : B}
+    (ha : SemiconjBy a₁ a₂ a₃) (hb : SemiconjBy b₁ b₂ b₃) :
+    SemiconjBy (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃) :=
+  congr_arg₂ (· ⊗ₜ[R] ·) ha.eq hb.eq
+
+nonrec theorem _root_.Commute.tmul {a₁ a₂ : A} {b₁ b₂ : B}
+    (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :
+    Commute (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) :=
+  ha.tmul hb
+
 instance instNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (A ⊗[R] B) where
   left_distrib a b c := by simp [HMul.hMul, Mul.mul]
   right_distrib a b c := by simp [HMul.hMul, Mul.mul]
@@ -652,6 +667,65 @@ theorem algEquivOfLinearEquivTripleTensorProduct_apply (f h_mul h_one x) :
   rfl
 #align algebra.tensor_product.alg_equiv_of_linear_equiv_triple_tensor_product_apply Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply
 
+section lift
+variable [IsScalarTower R S A] [IsScalarTower R 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. -/
+def lift (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) : (A ⊗[R] B) →ₐ[S] C :=
+  algHomOfLinearMapTensorProduct
+    (AlgebraTensorModule.lift <|
+      letI restr : (C →ₗ[S] C) →ₗ[S] _ :=
+        { toFun := (·.restrictScalars R)
+          map_add' := fun f g => LinearMap.ext fun x => rfl
+          map_smul' := fun c g => LinearMap.ext fun x => rfl }
+      LinearMap.flip <| (restr ∘ₗ LinearMap.mul S C ∘ₗ f.toLinearMap).flip ∘ₗ g)
+    (fun a₁ a₂ b₁ b₂ => show f (a₁ * a₂) * g (b₁ * b₂) = f a₁ * g b₁ * (f a₂ * g b₂) by
+      rw [f.map_mul, g.map_mul, (hfg a₂ b₁).mul_mul_mul_comm])
+    (show f 1 * g 1 = 1 by rw [f.map_one, g.map_one, one_mul])
+
+@[simp]
+theorem lift_tmul (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y))
+    (a : A) (b : B) :
+    lift f g hfg (a ⊗ₜ b) = f a * g b :=
+  rfl
+
+@[simp]
+theorem lift_includeLeft_includeRight :
+    lift includeLeft includeRight (fun a b => (Commute.one_right _).tmul (Commute.one_left _)) =
+      .id S (A ⊗[R] B) := by
+  ext <;> simp
+
+@[simp]
+theorem lift_comp_includeLeft (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) :
+    (lift f g hfg).comp includeLeft = f :=
+  AlgHom.ext <| by simp
+
+@[simp]
+theorem lift_comp_includeRight (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) :
+    ((lift f g hfg).restrictScalars R).comp includeRight = g :=
+  AlgHom.ext <| by simp
+
+/-- 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. -/
+@[simps]
+def liftEquiv [IsScalarTower R S A] [IsScalarTower R S C] :
+    {fg : (A →ₐ[S] C) × (B →ₐ[R] C) // ∀ x y, Commute (fg.1 x) (fg.2 y)}
+      ≃ ((A ⊗[R] B) →ₐ[S] C) where
+  toFun fg := lift fg.val.1 fg.val.2 fg.prop
+  invFun f' := ⟨(f'.comp includeLeft, (f'.restrictScalars R).comp includeRight), fun x y =>
+    ((Commute.one_right _).tmul (Commute.one_left _)).map f'⟩
+  left_inv fg := by ext <;> simp
+  right_inv f' := by ext <;> simp
+
+end lift
+
 end
 
 variable [CommSemiring R] [CommSemiring S] [Algebra R S]
@@ -677,8 +751,7 @@ protected nonrec def lid : R ⊗[R] A ≃ₐ[R] A :=
 #align algebra.tensor_product.lid Algebra.TensorProduct.lid
 
 @[simp]
-theorem lid_tmul (r : R) (a : A) : (TensorProduct.lid R A : R ⊗ A → A) (r ⊗ₜ a) = r • a := by
-  simp [TensorProduct.lid]
+theorem lid_tmul (r : R) (a : A) : (TensorProduct.lid R A : R ⊗ A → A) (r ⊗ₜ a) = r • a := rfl
 #align algebra.tensor_product.lid_tmul Algebra.TensorProduct.lid_tmul
 
 variable (S)
@@ -711,8 +784,8 @@ protected def comm : A ⊗[R] B ≃ₐ[R] B ⊗[R] A :=
 
 @[simp]
 theorem comm_tmul (a : A) (b : B) :
-    (TensorProduct.comm R A B : A ⊗[R] B → B ⊗[R] A) (a ⊗ₜ b) = b ⊗ₜ a := by
-  simp [TensorProduct.comm]
+    (TensorProduct.comm R A B : A ⊗[R] B → B ⊗[R] A) (a ⊗ₜ b) = b ⊗ₜ a :=
+  rfl
 #align algebra.tensor_product.comm_tmul Algebra.TensorProduct.comm_tmul
 
 theorem adjoin_tmul_eq_top : adjoin R { t : A ⊗[R] B | ∃ a b, a ⊗ₜ[R] b = t } = ⊤ :=
@@ -844,6 +917,24 @@ end Monoidal
 
 section
 
+variable [CommSemiring R] [CommSemiring S] [Algebra R S]
+variable [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A]
+variable [Semiring B] [Algebra R B]
+variable [CommSemiring C] [Algebra R C] [Algebra S C] [IsScalarTower R 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. -/
+abbrev productLeftAlgHom (f : A →ₐ[S] C) (g : B →ₐ[R] C) : A ⊗[R] B →ₐ[S] C :=
+  lift f g (fun _ _ => Commute.all _ _)
+#align algebra.tensor_product.product_left_alg_hom Algebra.TensorProduct.productLeftAlgHom
+
+end
+
+section
+
 variable [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S]
 
 variable [Algebra R A] [Algebra R B] [Algebra R S]
@@ -882,11 +973,16 @@ theorem lmul'_comp_includeRight : (lmul' R : _ →ₐ[R] S).comp includeRight =
 
 /-- 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.
 -/
-def productMap : A ⊗[R] B →ₐ[R] S :=
-  (lmul' R).comp (TensorProduct.map f g)
+def productMap : A ⊗[R] B →ₐ[R] S := productLeftAlgHom f g
 #align algebra.tensor_product.product_map Algebra.TensorProduct.productMap
 
+theorem productMap_eq_comp_map : productMap f g = (lmul' R).comp (TensorProduct.map f g) := by
+  ext <;> rfl
+
 @[simp]
 theorem productMap_apply_tmul (a : A) (b : B) : productMap f g (a ⊗ₜ b) = f a * g b := rfl
 
@@ -898,7 +994,7 @@ theorem productMap_left_apply (a : A) : productMap f g (a ⊗ₜ 1) = f a := by
 
 @[simp]
 theorem productMap_left : (productMap f g).comp includeLeft = f :=
-  AlgHom.ext <| by simp
+  lift_comp_includeLeft _ _ (fun _ _ => Commute.all _ _)
 #align algebra.tensor_product.product_map_left Algebra.TensorProduct.productMap_left
 
 theorem productMap_right_apply (b : B) :
@@ -907,37 +1003,18 @@ theorem productMap_right_apply (b : B) :
 
 @[simp]
 theorem productMap_right : (productMap f g).comp includeRight = g :=
-  AlgHom.ext <| by simp
+  lift_comp_includeRight _ _ (fun _ _ => Commute.all _ _)
 #align algebra.tensor_product.product_map_right Algebra.TensorProduct.productMap_right
 
 theorem productMap_range : (productMap f g).range = f.range ⊔ g.range := by
-  rw [productMap, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp, ← AlgHom.range_comp,
+  rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
+    ← AlgHom.range_comp,
     ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
     AlgHom.id_comp, AlgHom.id_comp]
 #align algebra.tensor_product.product_map_range Algebra.TensorProduct.productMap_range
 
 end
 
-section
-
-variable [CommSemiring R] [CommSemiring S] [Algebra R S]
-variable [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A]
-variable [Semiring B] [Algebra R B]
-variable [CommSemiring C] [Algebra R C] [Algebra S C] [IsScalarTower R 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. -/
-@[simps!]
-def productLeftAlgHom (f : A →ₐ[S] C) (g : B →ₐ[R] C) : A ⊗[R] B →ₐ[S] C :=
-  { (productMap (f.restrictScalars R) g).toRingHom with
-    commutes' := fun r => by
-      dsimp
-      simp }
-#align algebra.tensor_product.product_left_alg_hom Algebra.TensorProduct.productLeftAlgHom
-
-end
-
 section Basis
 
 universe uM uι

docs/references.bib

@@ -1542,6 +1542,21 @@ @Book{            Kashiwara2006
   title         = {Categories and Sheaves}
 }
 
+@InBook{          kasselTensorProducts1995,
+  title         = {Tensor {{Products}}},
+  booktitle     = {Quantum {{Groups}}},
+  author        = {Kassel, Christian},
+  year          = {1995},
+  volume        = {155},
+  pages         = {23--38},
+  publisher     = {{Springer New York}},
+  address       = {{New York, NY}},
+  doi           = {10.1007/978-1-4612-0783-2_2},
+  urldate       = {2023-09-28},
+  collaborator  = {Kassel, Christian},
+  isbn          = {978-1-4612-6900-7 978-1-4612-0783-2}
+}
+
 @Book{            katz_mazur,
   author        = {Katz, Nicholas M. and Mazur, Barry},
   title         = {Arithmetic moduli of elliptic curves},