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_reducible]

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 = (tprod R) 1

@[instance_reducible]

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 y : (i : ι) → A i) : (mul ((tprod R) x)) ((tprod R) y) = (tprod R) (x * y)

@[instance_reducible]

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 y : PiTensorProduct R fun (i : ι) => A i) : x * y = (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 y : (i : ι) → A i) : (tprod R) x * (tprod R) y = (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₁ a₂ 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₁ 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 s : R) (x y : (i : ι) → A i) : r • (tprod R) x * s • (tprod R) y = (r * s) • (tprod R) (x * y)

@[instance_reducible]

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

• PiTensorProduct.instNonUnitalNonAssocSemiring = { toAddCommMonoid := inferInstance, toMul := PiTensorProduct.instMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

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) : (mul ((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) : (mul x) ((tprod R) 1) = x

@[instance_reducible]

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

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

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 = { toFun := ⇑(PiTensorProduct.tprod R), map_one' := ⋯, map_mul' := ⋯ }

@[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) : (tprodMonoidHom R) a = (tprod R) a

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 y z : PiTensorProduct R fun (i : ι) => A i) : (mul ((mul x) y)) z = (mul x) ((mul y) z)

@[instance_reducible]

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 = { toNonUnitalNonAssocSemiring := PiTensorProduct.instNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

@[instance_reducible]

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

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

@[instance_reducible]

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 = (tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))

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.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) : (singleAlgHom i) a = (tprod R) ((MonoidHom.mulSingle A i) 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.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) : (liftAlgHom f one mul) a = (lift f) a

@[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 : (↑s).Pairwise (Function.onFun Commute x)) : (tprod R) (s.noncommProd x hx) = s.noncommProd (fun (k : κ) => (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 g : (PiTensorProduct R fun (i : ι) => A i) →ₐ[R] S⦄ (h : ∀ (i : ι), f.comp (singleAlgHom i) = g.comp (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 ⊗ ⋯$.

theorem PiTensorProduct.algHom_ext_iff {ι : 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 g : (PiTensorProduct R fun (i : ι) => A i) →ₐ[R] S} : f = g ↔ ∀ (i : ι), f.comp (singleAlgHom i) = g.comp (singleAlgHom i)

@[instance_reducible]

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 y : PiTensorProduct R fun (i : ι) => A i) : (mul x) y = (mul y) x

@[instance_reducible]

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 = { toSemiring := PiTensorProduct.instSemiring, mul_comm := ⋯ }

@[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) : (tprod R) (∏ k ∈ s, x k) = ∏ k ∈ s, (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) : (constantBaseRingEquiv ι R) ((tprod R) x) = ∏ i : ι, x i

@[simp]

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

@[instance_reducible]

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

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