Documentation

Mathlib.RingTheory.PiTensorProduct

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
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)] :
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
Instances For
    @[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) :
    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₃) :
    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₂) :
    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) :
    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)] :
    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) :
    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
    Instances For
      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
      • PiTensorProduct.instAlgebra = let __spread.0 := PiTensorProduct.hasSMul'; Algebra.mk { toFun := fun (x : R') => x 1, map_one' := , map_mul' := , map_zero' := , map_add' := }
      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) :
      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.
      Instances For
        @[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
        Instances For
          @[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 fun (a b : κ) => Commute (x a) (x b)) :
          (PiTensorProduct.tprod R) (s.noncommProd x hx) = s.noncommProd (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 : ι), f.comp (PiTensorProduct.singleAlgHom i) = g.comp (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
          @[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) (ks, x k) = ks, (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.
          Instances For
            @[simp]
            theorem PiTensorProduct.constantBaseRingEquiv_tprod {ι : Type u_1} {R : Type u_3} [CommSemiring R] [Fintype ι] (x : ιR) :
            @[simp]
            theorem PiTensorProduct.constantBaseRingEquiv_symm {ι : Type u_1} {R : Type u_3} [CommSemiring R] [Fintype ι] (r : R) :
            (PiTensorProduct.constantBaseRingEquiv ι R).symm 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