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.

instance PiTensorProduct.instOne {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → AddCommMonoidWithOne (A i)] [(i : ι) → Module R (A i)] : One (PiTensorProduct R fun (i : ι) => A i)

Equations

• PiTensorProduct.instOne = { one := (PiTensorProduct.tprod R) 1 }

theorem PiTensorProduct.one_def {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → AddCommMonoidWithOne (A i)] [(i : ι) → Module R (A i)] : 1 = (PiTensorProduct.tprod R) 1

instance PiTensorProduct.instAddCommMonoidWithOne {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → AddCommMonoidWithOne (A i)] [(i : ι) → Module R (A i)] : AddCommMonoidWithOne (PiTensorProduct R fun (i : ι) => A i)

Equations

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

def PiTensorProduct.mul {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] : (PiTensorProduct R fun (i : ι) => A i) →ₗ[R] (PiTensorProduct R fun (i : ι) => A i) →ₗ[R] PiTensorProduct R fun (i : ι) => A i

The multiplication in tensor product of rings is induced by (xᵢ) * (yᵢ) = (xᵢ * yᵢ)

Equations

• PiTensorProduct.mul = PiTensorProduct.piTensorHomMap₂ ((PiTensorProduct.tprod R) fun (x : ι) => LinearMap.mul R (A x))

@[simp]

theorem PiTensorProduct.mul_tprod_tprod {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] (x : (i : ι) → A i) (y : (i : ι) → A i) : (PiTensorProduct.mul ((PiTensorProduct.tprod R) x)) ((PiTensorProduct.tprod R) y) = (PiTensorProduct.tprod R) (x * y)

instance PiTensorProduct.instMul {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] : Mul (PiTensorProduct R fun (i : ι) => A i)

Equations

• PiTensorProduct.instMul = { mul := fun (x y : PiTensorProduct R fun (i : ι) => A i) => (PiTensorProduct.mul x) y }

theorem PiTensorProduct.mul_def {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] (x : PiTensorProduct R fun (i : ι) => A i) (y : PiTensorProduct R fun (i : ι) => A i) : x * y = (PiTensorProduct.mul x) y

@[simp]

theorem PiTensorProduct.tprod_mul_tprod {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] (x : (i : ι) → A i) (y : (i : ι) → A i) : (PiTensorProduct.tprod R) x * (PiTensorProduct.tprod R) y = (PiTensorProduct.tprod R) (x * y)

theorem SemiconjBy.tprod {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] {a₁ : (i : ι) → A i} {a₂ : (i : ι) → A i} {a₃ : (i : ι) → A i} (ha : SemiconjBy a₁ a₂ a₃) : SemiconjBy ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂) ((PiTensorProduct.tprod R) a₃)

theorem Commute.tprod {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] {a₁ : (i : ι) → A i} {a₂ : (i : ι) → A i} (ha : Commute a₁ a₂) : Commute ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂)

theorem PiTensorProduct.smul_tprod_mul_smul_tprod {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] (r : R) (s : R) (x : (i : ι) → A i) (y : (i : ι) → A i) : r • (PiTensorProduct.tprod R) x * s • (PiTensorProduct.tprod R) y = (r * s) • (PiTensorProduct.tprod R) (x * y)

instance PiTensorProduct.instNonUnitalNonAssocSemiring {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] : NonUnitalNonAssocSemiring (PiTensorProduct R fun (i : ι) => A i)

Equations

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

theorem PiTensorProduct.one_mul {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] (x : PiTensorProduct R fun (i : ι) => A i) : (PiTensorProduct.mul ((PiTensorProduct.tprod R) 1)) x = x

theorem PiTensorProduct.mul_one {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] (x : PiTensorProduct R fun (i : ι) => A i) : (PiTensorProduct.mul x) ((PiTensorProduct.tprod R) 1) = x

instance PiTensorProduct.instNonAssocSemiring {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] : NonAssocSemiring (PiTensorProduct R fun (i : ι) => A i)

Equations

• PiTensorProduct.instNonAssocSemiring = let __spread.0 := PiTensorProduct.instNonUnitalNonAssocSemiring; NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem PiTensorProduct.tprodMonoidHom_apply {ι : Type u_1} (R : Type u_3) {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] (a : (i : ι) → A i) : (PiTensorProduct.tprodMonoidHom R) a = (PiTensorProduct.tprod R) a

def PiTensorProduct.tprodMonoidHom {ι : Type u_1} (R : Type u_3) {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonAssocSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] : ((i : ι) → A i) →* PiTensorProduct R fun (i : ι) => A i

PiTensorProduct.tprod as a MonoidHom.

Equations

• PiTensorProduct.tprodMonoidHom R = { toOneHom := { toFun := ⇑(PiTensorProduct.tprod R), map_one' := ⋯ }, map_mul' := ⋯ }

theorem PiTensorProduct.mul_assoc {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] (x : PiTensorProduct R fun (i : ι) => A i) (y : PiTensorProduct R fun (i : ι) => A i) (z : PiTensorProduct R fun (i : ι) => A i) : (PiTensorProduct.mul ((PiTensorProduct.mul x) y)) z = (PiTensorProduct.mul x) ((PiTensorProduct.mul y) z)

instance PiTensorProduct.instNonUnitalSemiring {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → NonUnitalSemiring (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] : NonUnitalSemiring (PiTensorProduct R fun (i : ι) => A i)

Equations

• PiTensorProduct.instNonUnitalSemiring = let __spread.0 := PiTensorProduct.instNonUnitalNonAssocSemiring; NonUnitalSemiring.mk ⋯

instance PiTensorProduct.instSemiring {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] : Semiring (PiTensorProduct R fun (i : ι) => A i)

Equations

• PiTensorProduct.instSemiring = let __spread.0 := PiTensorProduct.instNonUnitalSemiring; let __spread.1 := PiTensorProduct.instNonAssocSemiring; Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRec ⋯ ⋯

instance PiTensorProduct.instAlgebra {ι : Type u_1} {R' : Type u_2} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R'] [CommSemiring R] [(i : ι) → Semiring (A i)] [Algebra R' R] [(i : ι) → Algebra R (A i)] : Algebra R' (PiTensorProduct R fun (i : ι) => A i)

Equations

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

theorem PiTensorProduct.algebraMap_apply {ι : Type u_1} {R' : Type u_2} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R'] [CommSemiring R] [(i : ι) → Semiring (A i)] [Algebra R' R] [(i : ι) → Algebra R (A i)] [(i : ι) → Algebra R' (A i)] [∀ (i : ι), IsScalarTower R' R (A i)] (r : R') (i : ι) [DecidableEq ι] : (algebraMap R' (PiTensorProduct R fun (i : ι) => A i)) r = (PiTensorProduct.tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))

@[simp]

theorem PiTensorProduct.singleAlgHom_apply {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [DecidableEq ι] (i : ι) (a : A i) : (PiTensorProduct.singleAlgHom i) a = (PiTensorProduct.tprod R) ((MonoidHom.mulSingle (fun (i : ι) => A i) i) a)

def PiTensorProduct.singleAlgHom {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [DecidableEq ι] (i : ι) : A i →ₐ[R] PiTensorProduct R fun (i : ι) => A i

The map Aᵢ ⟶ ⨂ᵢ Aᵢ given by a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...

Equations

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

@[simp]

theorem PiTensorProduct.liftAlgHom_apply {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {S : Type u_5} [Semiring S] [Algebra R S] (f : MultilinearMap R A S) (one : f 1 = 1) (mul : ∀ (x y : (i : ι) → A i), f (x * y) = f x * f y) (a : PiTensorProduct R fun (i : ι) => A i) : (PiTensorProduct.liftAlgHom f one mul) a = (PiTensorProduct.lift f) a

def PiTensorProduct.liftAlgHom {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {S : Type u_5} [Semiring S] [Algebra R S] (f : MultilinearMap R A S) (one : f 1 = 1) (mul : ∀ (x y : (i : ι) → A i), f (x * y) = f x * f y) : (PiTensorProduct R fun (i : ι) => A i) →ₐ[R] S

Lifting a multilinear map to an algebra homomorphism from tensor product

Equations

• PiTensorProduct.liftAlgHom f one mul = AlgHom.ofLinearMap (PiTensorProduct.lift f) ⋯ ⋯

@[simp]

theorem PiTensorProduct.tprod_noncommProd {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {κ : Type u_5} (s : Finset κ) (x : κ → (i : ι) → A i) (hx : Set.Pairwise ↑s fun (a b : κ) => Commute (x a) (x b)) : (PiTensorProduct.tprod R) (Finset.noncommProd s x hx) = Finset.noncommProd s (fun (k : κ) => (PiTensorProduct.tprod R) (x k)) ⋯

theorem PiTensorProduct.algHom_ext {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {S : Type u_5} [Finite ι] [DecidableEq ι] [Semiring S] [Algebra R S] ⦃f : (PiTensorProduct R fun (i : ι) => A i) →ₐ[R] S⦄ ⦃g : (PiTensorProduct R fun (i : ι) => A i) →ₐ[R] S⦄ (h : ∀ (i : ι), AlgHom.comp f (PiTensorProduct.singleAlgHom i) = AlgHom.comp g (PiTensorProduct.singleAlgHom i)) : f = g

To show two algebra morphisms from finite tensor products are equal, it suffices to show that they agree on elements of the form $1 ⊗ ⋯ ⊗ a ⊗ 1 ⊗ ⋯$.

instance PiTensorProduct.instRing {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommRing R] [(i : ι) → Ring (A i)] [(i : ι) → Algebra R (A i)] : Ring (PiTensorProduct R fun (i : ι) => A i)

Equations

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

theorem PiTensorProduct.mul_comm {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → CommSemiring (A i)] [(i : ι) → Algebra R (A i)] (x : PiTensorProduct R fun (i : ι) => A i) (y : PiTensorProduct R fun (i : ι) => A i) : (PiTensorProduct.mul x) y = (PiTensorProduct.mul y) x

instance PiTensorProduct.instCommSemiring {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → CommSemiring (A i)] [(i : ι) → Algebra R (A i)] : CommSemiring (PiTensorProduct R fun (i : ι) => A i)

Equations

• PiTensorProduct.instCommSemiring = let __spread.0 := PiTensorProduct.instSemiring; let __spread.1 := inferInstanceAs (AddCommMonoid (PiTensorProduct R fun (i : ι) => A i)); CommSemiring.mk ⋯

@[simp]

theorem PiTensorProduct.tprod_prod {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommSemiring R] [(i : ι) → CommSemiring (A i)] [(i : ι) → Algebra R (A i)] {κ : Type u_5} (s : Finset κ) (x : κ → (i : ι) → A i) : (PiTensorProduct.tprod R) (Finset.prod s fun (k : κ) => x k) = Finset.prod s fun (k : κ) => (PiTensorProduct.tprod R) (x k)

noncomputable def PiTensorProduct.constantBaseRingEquiv (ι : Type u_1) (R : Type u_3) [CommSemiring R] [Fintype ι] : (PiTensorProduct R fun (x : ι) => R) ≃ₐ[R] R

The algebra equivalence from the tensor product of the constant family with value R to R, given by multiplication of the entries.

Equations

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

@[simp]

theorem PiTensorProduct.constantBaseRingEquiv_tprod {ι : Type u_1} {R : Type u_3} [CommSemiring R] [Fintype ι] (x : ι → R) : (PiTensorProduct.constantBaseRingEquiv ι R) ((PiTensorProduct.tprod R) x) = Finset.prod Finset.univ fun (i : ι) => x i

@[simp]

theorem PiTensorProduct.constantBaseRingEquiv_symm {ι : Type u_1} {R : Type u_3} [CommSemiring R] [Fintype ι] (r : R) : (AlgEquiv.symm (PiTensorProduct.constantBaseRingEquiv ι R)) r = (algebraMap R (PiTensorProduct R fun (x : ι) => R)) r

instance PiTensorProduct.instCommRing {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [CommRing R] [(i : ι) → CommRing (A i)] [(i : ι) → Algebra R (A i)] : CommRing (PiTensorProduct R fun (i : ι) => A i)

Equations

• PiTensorProduct.instCommRing = let __spread.0 := PiTensorProduct.instCommSemiring; let __spread.1 := inferInstanceAs (AddCommGroup (PiTensorProduct R fun (i : ι) => A i)); CommRing.mk ⋯