feat(LinearAlgebra/PiTensorProduct): arbitrary tensor product of algebras (#9395)

Let $R$ be a commutative ring and $(A_i)$ a bunch of $R$-algebras, then $\bigotimes_{R} A$ is an $R$-algebra as well. In particular, taking $R$ to be $\mathbb{Z}$, we get tensor product of rings



Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: 3 people

Mathlib.lean

@@ -3328,6 +3328,7 @@ import Mathlib.RingTheory.Nullstellensatz
 import Mathlib.RingTheory.OreLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.OreSet
 import Mathlib.RingTheory.Perfection
+import Mathlib.RingTheory.PiTensorProduct
 import Mathlib.RingTheory.Polynomial.Basic
 import Mathlib.RingTheory.Polynomial.Bernstein
 import Mathlib.RingTheory.Polynomial.Chebyshev

Mathlib/LinearAlgebra/Multilinear/Basic.lean

@@ -1040,6 +1040,19 @@ sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g
     · exact Function.apply_update c f i (a • f₀) j
     · exact Function.apply_update c f i f₀ j
 
+/--
+Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module.
+Let us denote `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` by `M` and `M'` respectively.
+If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear
+map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` via `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`.
+-/
+@[simps!] def piLinearMap :
+    MultilinearMap R M₁' M₂ →ₗ[R]
+    MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) where
+  toFun g := (LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear
+  map_add' := by aesop
+  map_smul' := by aesop
+
 end
 
 /-- If one multiplies by `c i` the coordinates in a finset `s`, then the image under a multilinear

Mathlib/LinearAlgebra/PiTensorProduct.lean

@@ -357,6 +357,8 @@ open MultilinearMap
 
 variable {s}
 
+section lift
+
 /-- Auxiliary function to constructing a linear map `(⨂[R] i, s i) → E` given a
 `MultilinearMap R s E` with the property that its composition with the canonical
 `MultilinearMap R s (⨂[R] i, s i)` is the given multilinear map. -/
@@ -446,6 +448,84 @@ theorem lift_tprod : lift (tprod R : MultilinearMap R s _) = LinearMap.id :=
   Eq.symm <| lift.unique' rfl
 #align pi_tensor_product.lift_tprod PiTensorProduct.lift_tprod
 
+end lift
+
+section map
+
+variable {t t' : ι → Type*}
+variable [∀ i, AddCommMonoid (t i)] [∀ i, Module R (t i)]
+variable [∀ i, AddCommMonoid (t' i)] [∀ i, Module R (t' i)]
+
+/--
+Let `sᵢ` and `tᵢ` be two families of `R`-modules.
+Let `f` be a family of `R`-linear maps between `sᵢ` and `tᵢ`, i.e. `f : Πᵢ sᵢ → tᵢ`,
+then there is an induced map `⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`.
+
+This is `TensorProduct.map` for an arbitrary family of modules.
+-/
+def map (f : Π i, s i →ₗ[R] t i) : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i :=
+  lift <| (tprod R).compLinearMap f
+
+@[simp] lemma map_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) :
+    map f (tprod R x) = tprod R fun i ↦ f i (x i) :=
+  lift.tprod _
+
+/--
+Let `sᵢ` and `tᵢ` be families of `R`-modules.
+Then there is an `R`-linear map between `⨂ᵢ Hom(sᵢ, tᵢ)` and `Hom(⨂ᵢ sᵢ, ⨂ tᵢ)` defined by
+`⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ fᵢ aᵢ`.
+
+This is `TensorProduct.homTensorHomMap` for an arbitrary family of modules.
+
+Note that `PiTensorProduct.piTensorHomMap (tprod R f)` is equal to `PiTensorProduct.map f`.
+-/
+def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i :=
+  lift.toLinearMap ∘ₗ lift (MultilinearMap.piLinearMap <| tprod R)
+
+@[simp] lemma piTensorHomMap_tprod_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) :
+    piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by
+  simp [piTensorHomMap]
+
+lemma piTensorHomMap_tprod_eq_map (f : Π i, s i →ₗ[R] t i) :
+    piTensorHomMap (tprod R f) = map f := by
+  ext; simp
+
+/--
+Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, then `f : Πᵢ sᵢ → tᵢ → t'ᵢ` induces an
+element of `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` defined by `⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`.
+
+This is `PiTensorProduct.map` for two arbitrary families of modules.
+This is `TensorProduct.map₂` for families of modules.
+-/
+def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) :
+    (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i:=
+  lift <| LinearMap.compMultilinearMap piTensorHomMap <| (tprod R).compLinearMap f
+
+lemma map₂_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : Π i, s i) (y : Π i, t i) :
+    map₂ f (tprod R x) (tprod R y) = tprod R fun i ↦ f i (x i) (y i) := by
+  simp [map₂]
+
+/--
+Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules.
+Then there is an linear map from `⨂ᵢ Hom(sᵢ, Hom(tᵢ, t'ᵢ))` to `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))`
+defined by `⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`.
+
+This is `TensorProduct.homTensorHomMap` for two arbitrary families of modules.
+-/
+def piTensorHomMap₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R]
+    (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) where
+  toFun φ := lift <| LinearMap.compMultilinearMap piTensorHomMap <|
+    (lift <| MultilinearMap.piLinearMap <| tprod R) φ
+  map_add' x y := by dsimp; ext; simp
+  map_smul' r x := by dsimp; ext; simp
+
+@[simp] lemma piTensorHomMap₂_tprod_tprod_tprod
+    (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) :
+    piTensorHomMap₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by
+  simp [piTensorHomMap₂]
+
+end map
+
 section
 
 variable (R M)

Mathlib/RingTheory/PiTensorProduct.lean

@@ -0,0 +1,231 @@
+/-
+Copyright (c) 2024 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+
+import Mathlib.LinearAlgebra.PiTensorProduct
+import Mathlib.Algebra.Algebra.Bilinear
+
+/-!
+# Tensor product of `R`-algebras and rings
+
+If `(Aᵢ)` is a family of `R`-algebras then the `R`-tensor product `⨂ᵢ Aᵢ` is an `R`-algebra as well
+with structure map defined by `r ↦ r • 1`.
+
+In particular if we take `R` to be `ℤ`, then this collapses into the tensor product of rings.
+-/
+
+open TensorProduct Function
+
+variable {ι R' R : Type*} {A : ι → Type*}
+
+namespace PiTensorProduct
+
+noncomputable section AddCommMonoidWithOne
+
+variable [CommSemiring R] [∀ i, AddCommMonoidWithOne (A i)] [∀ i, Module R (A i)]
+
+instance instOne : One (⨂[R] i, A i) where
+  one := tprod R 1
+
+lemma one_def : 1 = tprod R (1 : Π i, A i) := rfl
+
+instance instAddCommMonoidWithOne : AddCommMonoidWithOne (⨂[R] i, A i) where
+  __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i))
+  __ := instOne
+
+end AddCommMonoidWithOne
+
+noncomputable section NonUnitalNonAssocSemiring
+
+variable [CommSemiring R] [∀ i, NonUnitalNonAssocSemiring (A i)]
+variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)]
+
+attribute [aesop safe] mul_add mul_smul_comm smul_mul_assoc add_mul in
+/--
+The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)`
+-/
+def mul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) :=
+  PiTensorProduct.piTensorHomMap₂ <| tprod R fun _ ↦ LinearMap.mul _ _
+
+@[simp] lemma mul_tprod_tprod (x y : (i : ι) → A i) :
+    mul (tprod R x) (tprod R y) = tprod R (x * y) := by
+  simp only [mul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply']
+  rfl
+
+instance instMul : Mul (⨂[R] i, A i) where
+  mul x y := mul x y
+
+lemma mul_def (x y : ⨂[R] i, A i) : x * y = mul x y := rfl
+
+@[simp] lemma tprod_mul_tprod (x y : (i : ι) → A i) :
+    tprod R x * tprod R y = tprod R (x * y) :=
+  mul_tprod_tprod x y
+
+lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) :
+    (r • tprod R x) * (s • tprod R y) = (r * s) • tprod R (x * y) := by
+  change mul _ _ = _
+  rw [map_smul, map_smul, mul_comm r s, mul_smul]
+  simp only [LinearMap.smul_apply, mul_tprod_tprod]
+
+instance instNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (⨂[R] i, A i) where
+  __ := instMul
+  __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i))
+  left_distrib _ _ _ := (mul _).map_add _ _
+  right_distrib _ _ _ := mul.map_add₂ _ _ _
+  zero_mul _ := mul.map_zero₂ _
+  mul_zero _ := map_zero (mul _)
+
+end NonUnitalNonAssocSemiring
+
+noncomputable section NonAssocSemiring
+
+variable [CommSemiring R] [∀ i, NonAssocSemiring (A i)]
+variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)]
+
+protected lemma one_mul (x : ⨂[R] i, A i) : mul (tprod R 1) x = x := by
+  induction x using PiTensorProduct.induction_on with
+  | smul_tprod => simp
+  | add _ _ h1 h2 => simp [map_add, h1, h2]
+
+protected lemma mul_one (x : ⨂[R] i, A i) : mul x (tprod R 1) = x := by
+  induction x using PiTensorProduct.induction_on with
+  | smul_tprod => simp
+  | add _ _ h1 h2 => simp [h1, h2]
+
+instance instNonAssocSemiring : NonAssocSemiring (⨂[R] i, A i) where
+  __ := instNonUnitalNonAssocSemiring
+  one_mul := PiTensorProduct.one_mul
+  mul_one := PiTensorProduct.mul_one
+
+end NonAssocSemiring
+
+noncomputable section NonUnitalSemiring
+
+variable [CommSemiring R] [∀ i, NonUnitalSemiring (A i)]
+variable [∀ i, Module R (A i)] [∀ i, SMulCommClass R (A i) (A i)] [∀ i, IsScalarTower R (A i) (A i)]
+
+protected lemma mul_assoc (x y z : ⨂[R] i, A i) : mul (mul x y) z = mul x (mul y z) := by
+  -- restate as an equality of morphisms so that we can use `ext`
+  suffices LinearMap.llcomp R _ _ _ mul ∘ₗ mul =
+      (LinearMap.llcomp R _ _ _ LinearMap.lflip <| LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by
+    exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z
+  ext x y z
+  dsimp [← mul_def]
+  simpa only [tprod_mul_tprod] using congr_arg (tprod R) (mul_assoc x y z)
+
+instance instNonUnitalSemiring : NonUnitalSemiring (⨂[R] i, A i) where
+  __ := instNonUnitalNonAssocSemiring
+  mul_assoc := PiTensorProduct.mul_assoc
+
+end NonUnitalSemiring
+
+noncomputable section Semiring
+
+variable [CommSemiring R'] [CommSemiring R] [∀ i, Semiring (A i)]
+variable [Algebra R' R] [∀ i, Algebra R (A i)] [∀ i, Algebra R' (A i)]
+variable [∀ i, IsScalarTower R' R (A i)]
+
+instance instSemiring : Semiring (⨂[R] i, A i) where
+  __ := instNonUnitalSemiring
+  __ := instNonAssocSemiring
+
+instance instAlgebra : Algebra R' (⨂[R] i, A i) where
+  __ := hasSMul'
+  toFun := (· • 1)
+  map_one' := by simp
+  map_mul' r s := show (r * s) • 1 = mul (r • 1) (s • 1)  by
+    rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply, mul_comm,
+      mul_smul]
+    congr
+    show (1 : ⨂[R] i, A i) = 1 * 1
+    rw [mul_one]
+  map_zero' := by simp
+  map_add' := by simp [add_smul]
+  commutes' r x := by
+    simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
+    change mul _ _ = mul _ _
+    rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply]
+    change r • (1 * x) = r • (x * 1)
+    rw [mul_one, one_mul]
+  smul_def' r x := by
+    simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
+    change _ = mul _ _
+    rw [LinearMap.map_smul_of_tower, LinearMap.smul_apply]
+    change _ = r • (1 * x)
+    rw [one_mul]
+
+lemma algebraMap_apply (r : R') (i : ι) [DecidableEq ι] :
+    algebraMap R' (⨂[R] i, A i) r = tprod R (Pi.mulSingle i (algebraMap R' (A i) r)) := by
+  change r • tprod R 1 = _
+  have : Pi.mulSingle i (algebraMap R' (A i) r) = update (fun i ↦ 1) i (r • 1) := by
+    rw [Algebra.algebraMap_eq_smul_one]; rfl
+  rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_smul, update_eq_self, smul_one_smul]
+  congr
+
+/--
+The map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...`
+-/
+@[simps]
+def singleAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where
+  toFun a := tprod R (MonoidHom.single _ i a)
+  map_one' := by simp only [_root_.map_one]; rfl
+  map_mul' a a' := by simp
+  map_zero' := MultilinearMap.map_update_zero _ _ _
+  map_add' _ _ := MultilinearMap.map_add _ _ _ _ _
+  commutes' r := show tprodCoeff R _ _ = r • tprodCoeff R _ _ by
+    rw [Algebra.algebraMap_eq_smul_one]
+    erw [smul_tprodCoeff]
+    rfl
+
+/--
+Lifting a multilinear map to an algebra homomorphism from tensor product
+-/
+@[simps!]
+def liftAlgHom {S : Type*} [Semiring S] [Algebra R S]
+    (f : MultilinearMap R A S)
+    (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : (⨂[R] i, A i) →ₐ[R] S :=
+  AlgHom.ofLinearMap (lift f) (show lift f (tprod R 1) = 1 by simp [one]) <|
+    LinearMap.map_mul_iff _ |>.mpr <| by aesop
+
+end Semiring
+
+noncomputable section Ring
+
+variable [CommRing R] [∀ i, Ring (A i)] [∀ i, Algebra R (A i)]
+
+instance instRing : Ring (⨂[R] i, A i) where
+  __ := instSemiring
+  __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i)
+
+end Ring
+
+noncomputable section CommSemiring
+
+variable [CommSemiring R] [∀ i, CommSemiring (A i)] [∀ i, Algebra R (A i)]
+
+protected lemma mul_comm (x y : ⨂[R] i, A i) : mul x y = mul y x := by
+  suffices mul (R := R) (A := A) = mul.flip from
+    DFunLike.congr_fun (DFunLike.congr_fun this x) y
+  ext x y
+  dsimp
+  simp only [mul_tprod_tprod, mul_tprod_tprod, mul_comm x y]
+
+instance instCommSemiring : CommSemiring (⨂[R] i, A i) where
+  __ := instSemiring
+  __ := inferInstanceAs <| AddCommMonoid (⨂[R] i, A i)
+  mul_comm := PiTensorProduct.mul_comm
+
+end CommSemiring
+
+noncomputable section CommRing
+
+variable [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
+instance instCommRing : CommRing (⨂[R] i, A i) where
+  __ := instCommSemiring
+  __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i)
+
+end CommRing
+
+end PiTensorProduct