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 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 ⋯ ⋯ ⋯ ⋯

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.single (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) ⋯ ⋯

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 ⋯

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 ⋯