Documentation

Mathlib.LinearAlgebra.PiTensorProduct

Tensor product of an indexed family of modules over commutative semirings #

We define the tensor product of an indexed family s : ι → Type* of modules over commutative semirings. We denote this space by ⨂[R] i, s i and define it as FreeAddMonoid (R × Π i, s i) quotiented by the appropriate equivalence relation. The treatment follows very closely that of the binary tensor product in LinearAlgebra/TensorProduct.lean.

Main definitions #

Notations #

Implementation notes #

TODO #

Tags #

multilinear, tensor, tensor product

inductive PiTensorProduct.Eqv {ι : Type u_1} (R : Type u_4) [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
FreeAddMonoid (R × ((i : ι) → s i))FreeAddMonoid (R × ((i : ι) → s i))Prop

The relation on FreeAddMonoid (R × Π i, s i) that generates a congruence whose quotient is the tensor product.

Instances For
    noncomputable def PiTensorProduct {ι : Type u_1} (R : Type u_4) [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
    Type (max (max u_1 u_4) u_7)

    PiTensorProduct R s with R a commutative semiring and s : ι → Type* is the tensor product of all the s i's. This is denoted by ⨂[R] i, s i.

    Equations
    Instances For

      Pretty printer defined by notation3 command.

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

        This enables the notation ⨂[R] i : ι, s i for the pi tensor product PiTensorProduct, given an indexed family of types s : ι → Type*.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable instance PiTensorProduct.instAddCommMonoid {ι : Type u_1} {R : Type u_4} [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
          AddCommMonoid (PiTensorProduct R fun (i : ι) => s i)
          Equations
          noncomputable instance PiTensorProduct.instInhabited {ι : Type u_1} {R : Type u_4} [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
          Inhabited (PiTensorProduct R fun (i : ι) => s i)
          Equations
          noncomputable def PiTensorProduct.tprodCoeff {ι : Type u_1} (R : Type u_4) [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (r : R) (f : (i : ι) → s i) :
          PiTensorProduct R fun (i : ι) => s i

          tprodCoeff R r f with r : R and f : Π i, s i is the tensor product of the vectors f i over all i : ι, multiplied by the coefficient r. Note that this is meant as an auxiliary definition for this file alone, and that one should use tprod defined below for most purposes.

          Equations
          Instances For
            theorem PiTensorProduct.zero_tprodCoeff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (f : (i : ι) → s i) :
            theorem PiTensorProduct.zero_tprodCoeff' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z : R) (f : (i : ι) → s i) (i : ι) (hf : f i = 0) :
            theorem PiTensorProduct.add_tprodCoeff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (m₁ : s i) (m₂ : s i) :
            theorem PiTensorProduct.add_tprodCoeff' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z₁ : R) (z₂ : R) (f : (i : ι) → s i) :
            theorem PiTensorProduct.smul_tprodCoeff_aux {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (r : R) :
            theorem PiTensorProduct.smul_tprodCoeff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (r : R₁) [SMul R₁ R] [IsScalarTower R₁ R R] [SMul R₁ (s i)] [IsScalarTower R₁ R (s i)] :
            noncomputable def PiTensorProduct.liftAddHom {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {F : Type u_10} [AddCommMonoid F] (φ : R × ((i : ι) → s i)F) (C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0φ (r, f) = 0) (C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0) (C_add : ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i), φ (r, Function.update f i m₁) + φ (r, Function.update f i m₂) = φ (r, Function.update f i (m₁ + m₂))) (C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)) (C_smul : ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, Function.update f i (r' f i)) = φ (r' * r, f)) :
            (PiTensorProduct R fun (i : ι) => s i) →+ F

            Construct an AddMonoidHom from (⨂[R] i, s i) to some space F from a function φ : (R × Π i, s i) → F with the appropriate properties.

            Equations
            Instances For
              theorem PiTensorProduct.induction_on' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {motive : (PiTensorProduct R fun (i : ι) => s i)Prop} (z : PiTensorProduct R fun (i : ι) => s i) (tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)) (add : ∀ (x y : PiTensorProduct R fun (i : ι) => s i), motive xmotive ymotive (x + y)) :
              motive z

              Induct using tprodCoeff

              noncomputable instance PiTensorProduct.hasSMul' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] :
              SMul R₁ (PiTensorProduct R fun (i : ι) => s i)
              Equations
              noncomputable instance PiTensorProduct.instSMul {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
              SMul R (PiTensorProduct R fun (i : ι) => s i)
              Equations
              • PiTensorProduct.instSMul = PiTensorProduct.hasSMul'
              theorem PiTensorProduct.smul_tprodCoeff' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] (r : R₁) (z : R) (f : (i : ι) → s i) :
              theorem PiTensorProduct.smul_add {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] (r : R₁) (x : PiTensorProduct R fun (i : ι) => s i) (y : PiTensorProduct R fun (i : ι) => s i) :
              r (x + y) = r x + r y
              noncomputable instance PiTensorProduct.distribMulAction' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] :
              DistribMulAction R₁ (PiTensorProduct R fun (i : ι) => s i)
              Equations
              noncomputable instance PiTensorProduct.smulCommClass' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {R₂ : Type u_6} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] [Monoid R₂] [DistribMulAction R₂ R] [SMulCommClass R₂ R R] [SMulCommClass R₁ R₂ R] :
              SMulCommClass R₁ R₂ (PiTensorProduct R fun (i : ι) => s i)
              Equations
              • =
              noncomputable instance PiTensorProduct.isScalarTower' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {R₂ : Type u_6} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] [Monoid R₂] [DistribMulAction R₂ R] [SMulCommClass R₂ R R] [SMul R₁ R₂] [IsScalarTower R₁ R₂ R] :
              IsScalarTower R₁ R₂ (PiTensorProduct R fun (i : ι) => s i)
              Equations
              • =
              noncomputable instance PiTensorProduct.module' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Semiring R₁] [Module R₁ R] [SMulCommClass R₁ R R] :
              Module R₁ (PiTensorProduct R fun (i : ι) => s i)
              Equations
              noncomputable instance PiTensorProduct.instModule {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
              Module R (PiTensorProduct R fun (i : ι) => s i)
              Equations
              • PiTensorProduct.instModule = PiTensorProduct.module'
              noncomputable instance PiTensorProduct.instSMulCommClass {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
              SMulCommClass R R (PiTensorProduct R fun (i : ι) => s i)
              Equations
              • =
              noncomputable instance PiTensorProduct.instIsScalarTower {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
              IsScalarTower R R (PiTensorProduct R fun (i : ι) => s i)
              Equations
              • =
              noncomputable def PiTensorProduct.tprod {ι : Type u_1} (R : Type u_4) [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
              MultilinearMap R s (PiTensorProduct R fun (i : ι) => s i)

              The canonical MultilinearMap R s (⨂[R] i, s i).

              tprod R fun i => f i has notation ⨂ₜ[R] i, f i.

              Equations
              Instances For

                The canonical MultilinearMap R s (⨂[R] i, s i).

                tprod R fun i => f i has notation ⨂ₜ[R] i, f i.

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

                  Pretty printer defined by notation3 command.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem PiTensorProduct.tprod_eq_tprodCoeff_one {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
                    @[simp]
                    theorem PiTensorProduct.tprodCoeff_eq_smul_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z : R) (f : (i : ι) → s i) :
                    theorem FreeAddMonoid.toPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (p : FreeAddMonoid (R × ((i : ι) → s i))) :
                    p = (List.map (fun (x : R × ((i : ι) → s i)) => x.1 ⨂ₜ[R] (i : ι), x.2 i) p).sum

                    The image of an element p of FreeAddMonoid (R × Π i, s i) in the PiTensorProduct is equal to the sum of a • ⨂ₜ[R] i, m i over all the entries (a, m) of p.

                    noncomputable def PiTensorProduct.lifts {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (x : PiTensorProduct R fun (i : ι) => s i) :
                    Set (FreeAddMonoid (R × ((i : ι) → s i)))

                    The set of lifts of an element x of ⨂[R] i, s i in FreeAddMonoid (R × Π i, s i).

                    Equations
                    Instances For
                      theorem PiTensorProduct.mem_lifts_iff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (x : PiTensorProduct R fun (i : ι) => s i) (p : FreeAddMonoid (R × ((i : ι) → s i))) :
                      p x.lifts (List.map (fun (x : R × ((i : ι) → s i)) => x.1 ⨂ₜ[R] (i : ι), x.2 i) p).sum = x

                      An element p of FreeAddMonoid (R × Π i, s i) lifts an element x of ⨂[R] i, s i if and only if x is equal to the sum of a • ⨂ₜ[R] i, m i over all the entries (a, m) of p.

                      theorem PiTensorProduct.nonempty_lifts {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (x : PiTensorProduct R fun (i : ι) => s i) :
                      x.lifts.Nonempty

                      Every element of ⨂[R] i, s i has a lift in FreeAddMonoid (R × Π i, s i).

                      theorem PiTensorProduct.lifts_zero {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :

                      The empty list lifts the element 0 of ⨂[R] i, s i.

                      theorem PiTensorProduct.lifts_add {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {x : PiTensorProduct R fun (i : ι) => s i} {y : PiTensorProduct R fun (i : ι) => s i} {p : FreeAddMonoid (R × ((i : ι) → s i))} {q : FreeAddMonoid (R × ((i : ι) → s i))} (hp : p x.lifts) (hq : q y.lifts) :
                      p + q (x + y).lifts

                      If elements p,q of FreeAddMonoid (R × Π i, s i) lift elements x,y of ⨂[R] i, s i respectively, then p + q lifts x + y.

                      theorem PiTensorProduct.lifts_smul {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {x : PiTensorProduct R fun (i : ι) => s i} {p : FreeAddMonoid (R × ((i : ι) → s i))} (h : p x.lifts) (a : R) :
                      List.map (fun (y : R × ((i : ι) → s i)) => (a * y.1, y.2)) p (a x).lifts

                      If an element p of FreeAddMonoid (R × Π i, s i) lifts an element x of ⨂[R] i, s i, and if a is an element of R, then the list obtained by multiplying the first entry of each element of p by a lifts a • x.

                      theorem PiTensorProduct.induction_on {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {motive : (PiTensorProduct R fun (i : ι) => s i)Prop} (z : PiTensorProduct R fun (i : ι) => s i) (smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (r (PiTensorProduct.tprod R) f)) (add : ∀ (x y : PiTensorProduct R fun (i : ι) => s i), motive xmotive ymotive (x + y)) :
                      motive z

                      Induct using scaled versions of PiTensorProduct.tprod.

                      theorem PiTensorProduct.ext_iff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ₁ : (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] E} {φ₂ : (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] E} :
                      φ₁ = φ₂ φ₁.compMultilinearMap (PiTensorProduct.tprod R) = φ₂.compMultilinearMap (PiTensorProduct.tprod R)
                      theorem PiTensorProduct.ext {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ₁ : (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] E} {φ₂ : (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] E} (H : φ₁.compMultilinearMap (PiTensorProduct.tprod R) = φ₂.compMultilinearMap (PiTensorProduct.tprod R)) :
                      φ₁ = φ₂
                      theorem PiTensorProduct.span_tprod_eq_top {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :

                      The pure tensors (i.e. the elements of the image of PiTensorProduct.tprod) span the tensor product.

                      noncomputable def PiTensorProduct.liftAux {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (φ : MultilinearMap R s E) :
                      (PiTensorProduct R fun (i : ι) => s i) →+ E

                      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.

                      Equations
                      Instances For
                        theorem PiTensorProduct.liftAux_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (φ : MultilinearMap R s E) (f : (i : ι) → s i) :
                        theorem PiTensorProduct.liftAux_tprodCoeff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (φ : MultilinearMap R s E) (z : R) (f : (i : ι) → s i) :
                        theorem PiTensorProduct.liftAux.smul {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ : MultilinearMap R s E} (r : R) (x : PiTensorProduct R fun (i : ι) => s i) :
                        noncomputable def PiTensorProduct.lift {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] :
                        MultilinearMap R s E ≃ₗ[R] (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] E

                        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 E is the given multilinear map φ.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem PiTensorProduct.lift.tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ : MultilinearMap R s E} (f : (i : ι) → s i) :
                          (PiTensorProduct.lift φ) ((PiTensorProduct.tprod R) f) = φ f
                          theorem PiTensorProduct.lift.unique' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ : MultilinearMap R s E} {φ' : (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] E} (H : φ'.compMultilinearMap (PiTensorProduct.tprod R) = φ) :
                          φ' = PiTensorProduct.lift φ
                          theorem PiTensorProduct.lift.unique {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ : MultilinearMap R s E} {φ' : (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] E} (H : ∀ (f : (i : ι) → s i), φ' ((PiTensorProduct.tprod R) f) = φ f) :
                          φ' = PiTensorProduct.lift φ
                          @[simp]
                          theorem PiTensorProduct.lift_symm {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (φ' : (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] E) :
                          PiTensorProduct.lift.symm φ' = φ'.compMultilinearMap (PiTensorProduct.tprod R)
                          @[simp]
                          theorem PiTensorProduct.lift_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
                          PiTensorProduct.lift (PiTensorProduct.tprod R) = LinearMap.id
                          noncomputable def PiTensorProduct.map {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) :
                          (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] PiTensorProduct R fun (i : ι) => 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.

                          Equations
                          Instances For
                            @[simp]
                            theorem PiTensorProduct.map_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (x : (i : ι) → s i) :
                            (PiTensorProduct.map f) ((PiTensorProduct.tprod R) x) = ⨂ₜ[R] (i : ι), (f i) (x i)
                            theorem PiTensorProduct.map_range_eq_span_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) :
                            LinearMap.range (PiTensorProduct.map f) = Submodule.span R {t_1 : PiTensorProduct R fun (i : ι) => t i | ∃ (m : (i : ι) → s i), (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
                            noncomputable def PiTensorProduct.mapIncl {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (p : (i : ι) → Submodule R (s i)) :
                            (PiTensorProduct R fun (i : ι) => (p i)) →ₗ[R] PiTensorProduct R fun (i : ι) => s i

                            Given submodules p i ⊆ s i, this is the natural map: ⨂[R] i, p i → ⨂[R] i, s i. This is TensorProduct.mapIncl for an arbitrary family of modules.

                            Equations
                            Instances For
                              theorem PiTensorProduct.map_comp {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} {t' : ιType u_12} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] [(i : ι) → AddCommMonoid (t' i)] [(i : ι) → Module R (t' i)] (g : (i : ι) → t i →ₗ[R] t' i) (f : (i : ι) → s i →ₗ[R] t i) :
                              (PiTensorProduct.map fun (i : ι) => g i ∘ₗ f i) = PiTensorProduct.map g ∘ₗ PiTensorProduct.map f
                              theorem PiTensorProduct.lift_comp_map {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (h : MultilinearMap R t E) :
                              PiTensorProduct.lift h ∘ₗ PiTensorProduct.map f = PiTensorProduct.lift (h.compLinearMap f)
                              @[simp]
                              theorem PiTensorProduct.map_id {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
                              (PiTensorProduct.map fun (i : ι) => LinearMap.id) = LinearMap.id
                              @[simp]
                              theorem PiTensorProduct.map_one {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
                              (PiTensorProduct.map fun (i : ι) => 1) = 1
                              theorem PiTensorProduct.map_mul {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (f₁ : (i : ι) → s i →ₗ[R] s i) (f₂ : (i : ι) → s i →ₗ[R] s i) :
                              (PiTensorProduct.map fun (i : ι) => f₁ i * f₂ i) = PiTensorProduct.map f₁ * PiTensorProduct.map f₂
                              noncomputable def PiTensorProduct.mapMonoidHom {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
                              ((i : ι) → s i →ₗ[R] s i) →* (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] PiTensorProduct R fun (i : ι) => s i

                              Upgrading PiTensorProduct.map to a MonoidHom when s = t.

                              Equations
                              • PiTensorProduct.mapMonoidHom = { toFun := PiTensorProduct.map, map_one' := , map_mul' := }
                              Instances For
                                @[simp]
                                theorem PiTensorProduct.mapMonoidHom_apply {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (f : (i : ι) → s i →ₗ[R] s i) :
                                PiTensorProduct.mapMonoidHom f = PiTensorProduct.map f
                                @[simp]
                                theorem PiTensorProduct.map_pow {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (f : (i : ι) → s i →ₗ[R] s i) (n : ) :
                                theorem PiTensorProduct.map_add {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) [DecidableEq ι] (i : ι) (u : s i →ₗ[R] t i) (v : s i →ₗ[R] t i) :
                                theorem PiTensorProduct.map_smul {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) [DecidableEq ι] (i : ι) (c : R) (u : s i →ₗ[R] t i) :
                                noncomputable def PiTensorProduct.mapMultilinear {ι : Type u_1} (R : Type u_4) [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (t : ιType u_11) [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] :
                                MultilinearMap R (fun (i : ι) => s i →ₗ[R] t i) ((PiTensorProduct R fun (i : ι) => s i) →ₗ[R] PiTensorProduct R fun (i : ι) => t i)

                                The tensor of a family of linear maps from sᵢ to tᵢ, as a multilinear map of the family.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem PiTensorProduct.mapMultilinear_apply {ι : Type u_1} (R : Type u_4) [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (t : ιType u_11) [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) :
                                  noncomputable def PiTensorProduct.piTensorHomMap {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] :
                                  (PiTensorProduct R fun (i : ι) => s i →ₗ[R] t i) →ₗ[R] (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] PiTensorProduct R fun (i : ι) => t i

                                  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.

                                  Equations
                                  • PiTensorProduct.piTensorHomMap = PiTensorProduct.lift ∘ₗ PiTensorProduct.lift (MultilinearMap.piLinearMap (PiTensorProduct.tprod R))
                                  Instances For
                                    @[simp]
                                    theorem PiTensorProduct.piTensorHomMap_tprod_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (x : (i : ι) → s i) :
                                    (PiTensorProduct.piTensorHomMap ((PiTensorProduct.tprod R) f)) ((PiTensorProduct.tprod R) x) = ⨂ₜ[R] (i : ι), (f i) (x i)
                                    theorem PiTensorProduct.piTensorHomMap_tprod_eq_map {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) :
                                    PiTensorProduct.piTensorHomMap ((PiTensorProduct.tprod R) f) = PiTensorProduct.map f
                                    noncomputable def PiTensorProduct.congr {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i ≃ₗ[R] t i) :
                                    (PiTensorProduct R fun (i : ι) => s i) ≃ₗ[R] PiTensorProduct R fun (i : ι) => t i

                                    If s i and t i are linearly equivalent for every i in ι, then ⨂[R] i, s i and ⨂[R] i, t i are linearly equivalent.

                                    This is the n-ary version of TensorProduct.congr

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem PiTensorProduct.congr_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i ≃ₗ[R] t i) (m : (i : ι) → s i) :
                                      (PiTensorProduct.congr f) ((PiTensorProduct.tprod R) m) = ⨂ₜ[R] (i : ι), (f i) (m i)
                                      @[simp]
                                      theorem PiTensorProduct.congr_symm_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i ≃ₗ[R] t i) (p : (i : ι) → t i) :
                                      (PiTensorProduct.congr f).symm ((PiTensorProduct.tprod R) p) = ⨂ₜ[R] (i : ι), (f i).symm (p i)
                                      noncomputable def PiTensorProduct.map₂ {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} {t' : ιType u_12} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] [(i : ι) → AddCommMonoid (t' i)] [(i : ι) → Module R (t' i)] (f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i) :
                                      (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] (PiTensorProduct R fun (i : ι) => t i) →ₗ[R] PiTensorProduct R fun (i : ι) => t' i

                                      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.

                                      Equations
                                      Instances For
                                        theorem PiTensorProduct.map₂_tprod_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} {t' : ιType u_12} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] [(i : ι) → AddCommMonoid (t' i)] [(i : ι) → Module R (t' i)] (f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i) (x : (i : ι) → s i) (y : (i : ι) → t i) :
                                        ((PiTensorProduct.map₂ f) ((PiTensorProduct.tprod R) x)) ((PiTensorProduct.tprod R) y) = ⨂ₜ[R] (i : ι), ((f i) (x i)) (y i)
                                        noncomputable def PiTensorProduct.piTensorHomMapFun₂ {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} {t' : ιType u_12} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] [(i : ι) → AddCommMonoid (t' i)] [(i : ι) → Module R (t' i)] :
                                        (PiTensorProduct R fun (i : ι) => s i →ₗ[R] t i →ₗ[R] t' i)(PiTensorProduct R fun (i : ι) => s i) →ₗ[R] (PiTensorProduct R fun (i : ι) => t i) →ₗ[R] PiTensorProduct R fun (i : ι) => t' i

                                        Let sᵢ, tᵢ and t'ᵢ be families of R-modules. Then there is a function from ⨂ᵢ Hom(sᵢ, Hom(tᵢ, t'ᵢ)) to Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ)) defined by ⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ.

                                        Equations
                                        • φ.piTensorHomMapFun₂ = PiTensorProduct.lift (PiTensorProduct.piTensorHomMap.compMultilinearMap ((PiTensorProduct.lift (MultilinearMap.piLinearMap (PiTensorProduct.tprod R))) φ))
                                        Instances For
                                          theorem PiTensorProduct.piTensorHomMapFun₂_add {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} {t' : ιType u_12} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] [(i : ι) → AddCommMonoid (t' i)] [(i : ι) → Module R (t' i)] (φ : PiTensorProduct R fun (i : ι) => s i →ₗ[R] t i →ₗ[R] t' i) (ψ : PiTensorProduct R fun (i : ι) => s i →ₗ[R] t i →ₗ[R] t' i) :
                                          (φ + ψ).piTensorHomMapFun₂ = φ.piTensorHomMapFun₂ + ψ.piTensorHomMapFun₂
                                          theorem PiTensorProduct.piTensorHomMapFun₂_smul {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} {t' : ιType u_12} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] [(i : ι) → AddCommMonoid (t' i)] [(i : ι) → Module R (t' i)] (r : R) (φ : PiTensorProduct R fun (i : ι) => s i →ₗ[R] t i →ₗ[R] t' i) :
                                          (r φ).piTensorHomMapFun₂ = r φ.piTensorHomMapFun₂
                                          noncomputable def PiTensorProduct.piTensorHomMap₂ {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} {t' : ιType u_12} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] [(i : ι) → AddCommMonoid (t' i)] [(i : ι) → Module R (t' i)] :
                                          (PiTensorProduct R fun (i : ι) => s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] (PiTensorProduct R fun (i : ι) => s i) →ₗ[R] (PiTensorProduct R fun (i : ι) => t i) →ₗ[R] PiTensorProduct R fun (i : ι) => t' i

                                          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.

                                          Equations
                                          • PiTensorProduct.piTensorHomMap₂ = { toFun := PiTensorProduct.piTensorHomMapFun₂, map_add' := , map_smul' := }
                                          Instances For
                                            @[simp]
                                            theorem PiTensorProduct.piTensorHomMap₂_tprod_tprod_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} {t' : ιType u_12} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] [(i : ι) → AddCommMonoid (t' i)] [(i : ι) → Module R (t' i)] (f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i) (a : (i : ι) → s i) (b : (i : ι) → t i) :
                                            ((PiTensorProduct.piTensorHomMap₂ ((PiTensorProduct.tprod R) f)) ((PiTensorProduct.tprod R) a)) ((PiTensorProduct.tprod R) b) = ⨂ₜ[R] (i : ι), ((f i) (a i)) (b i)
                                            noncomputable def PiTensorProduct.reindex {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (e : ι ι₂) :
                                            (PiTensorProduct R fun (i : ι) => s i) ≃ₗ[R] PiTensorProduct R fun (i : ι₂) => s (e.symm i)

                                            Re-index the components of the tensor power by e.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem PiTensorProduct.reindex_tprod {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (e : ι ι₂) (f : (i : ι) → s i) :
                                              (PiTensorProduct.reindex R s e) ((PiTensorProduct.tprod R) f) = (PiTensorProduct.tprod R) fun (i : ι₂) => f (e.symm i)
                                              @[simp]
                                              theorem PiTensorProduct.reindex_comp_tprod {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (e : ι ι₂) :
                                              (↑(PiTensorProduct.reindex R s e)).compMultilinearMap (PiTensorProduct.tprod R) = (MultilinearMap.domDomCongrLinearEquiv' R R s (PiTensorProduct R fun (i : ι₂) => s (e.symm i)) e).symm (PiTensorProduct.tprod R)
                                              theorem PiTensorProduct.lift_comp_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (e : ι ι₂) (φ : MultilinearMap R (fun (i : ι₂) => s (e.symm i)) E) :
                                              PiTensorProduct.lift φ ∘ₗ (PiTensorProduct.reindex R s e) = PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e).symm φ)
                                              @[simp]
                                              theorem PiTensorProduct.lift_comp_reindex_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (e : ι ι₂) (φ : MultilinearMap R s E) :
                                              PiTensorProduct.lift φ ∘ₗ (PiTensorProduct.reindex R s e).symm = PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e) φ)
                                              theorem PiTensorProduct.lift_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (e : ι ι₂) (φ : MultilinearMap R (fun (i : ι₂) => s (e.symm i)) E) (x : PiTensorProduct R fun (i : ι) => s i) :
                                              (PiTensorProduct.lift φ) ((PiTensorProduct.reindex R s e) x) = (PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e).symm φ)) x
                                              @[simp]
                                              theorem PiTensorProduct.lift_reindex_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (e : ι ι₂) (φ : MultilinearMap R s E) (x : PiTensorProduct R fun (i : ι₂) => s (e.symm i)) :
                                              (PiTensorProduct.lift φ) ((PiTensorProduct.reindex R s e).symm x) = (PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e) φ)) x
                                              @[simp]
                                              theorem PiTensorProduct.reindex_trans {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (e : ι ι₂) (e' : ι₂ ι₃) :
                                              PiTensorProduct.reindex R s e ≪≫ₗ PiTensorProduct.reindex R (fun (i : ι₂) => s (e.symm i)) e' = PiTensorProduct.reindex R s (e.trans e')
                                              theorem PiTensorProduct.reindex_reindex {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (e : ι ι₂) (e' : ι₂ ι₃) (x : PiTensorProduct R fun (i : ι) => s i) :
                                              (PiTensorProduct.reindex R (fun (i : ι₂) => s (e.symm i)) e') ((PiTensorProduct.reindex R s e) x) = (PiTensorProduct.reindex R s (e.trans e')) x
                                              @[simp]
                                              theorem PiTensorProduct.reindex_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ι₂) :
                                              (PiTensorProduct.reindex R (fun (x : ι) => M) e).symm = PiTensorProduct.reindex R (fun (x : ι₂) => M) e.symm

                                              This lemma is impractical to state in the dependent case.

                                              @[simp]
                                              theorem PiTensorProduct.reindex_refl {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
                                              theorem PiTensorProduct.map_comp_reindex_eq {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (e : ι ι₂) :
                                              (PiTensorProduct.map fun (i : ι₂) => f (e.symm i)) ∘ₗ (PiTensorProduct.reindex R s e) = (PiTensorProduct.reindex R t e) ∘ₗ PiTensorProduct.map f

                                              Re-indexing the components of the tensor product by an equivalence e is compatible with PiTensorProduct.map.

                                              theorem PiTensorProduct.map_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (e : ι ι₂) (x : PiTensorProduct R fun (i : ι) => s i) :
                                              (PiTensorProduct.map fun (i : ι₂) => f (e.symm i)) ((PiTensorProduct.reindex R s e) x) = (PiTensorProduct.reindex R t e) ((PiTensorProduct.map f) x)
                                              theorem PiTensorProduct.map_comp_reindex_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (e : ι ι₂) :
                                              PiTensorProduct.map f ∘ₗ (PiTensorProduct.reindex R s e).symm = (PiTensorProduct.reindex R t e).symm ∘ₗ PiTensorProduct.map fun (i : ι₂) => f (e.symm i)
                                              theorem PiTensorProduct.map_reindex_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ιType u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (e : ι ι₂) (x : PiTensorProduct R fun (i : ι₂) => s (e.symm i)) :
                                              (PiTensorProduct.map f) ((PiTensorProduct.reindex R s e).symm x) = (PiTensorProduct.reindex R t e).symm ((PiTensorProduct.map fun (i : ι₂) => f (e.symm i)) x)
                                              noncomputable def PiTensorProduct.isEmptyEquiv (ι : Type u_1) {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [IsEmpty ι] :
                                              (PiTensorProduct R fun (i : ι) => s i) ≃ₗ[R] R

                                              The tensor product over an empty index type ι is isomorphic to the base ring.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem PiTensorProduct.isEmptyEquiv_symm_apply (ι : Type u_1) {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [IsEmpty ι] (r : R) :
                                                @[simp]
                                                theorem PiTensorProduct.isEmptyEquiv_apply_tprod (ι : Type u_1) {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [IsEmpty ι] (f : (i : ι) → s i) :
                                                noncomputable def PiTensorProduct.subsingletonEquiv {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [Subsingleton ι] (i₀ : ι) :
                                                (PiTensorProduct R fun (x : ι) => M) ≃ₗ[R] M

                                                Tensor product of M over a singleton set is equivalent to M

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem PiTensorProduct.subsingletonEquiv_symm_apply {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [Subsingleton ι] (i₀ : ι) (m : M) :
                                                  (PiTensorProduct.subsingletonEquiv i₀).symm m = (PiTensorProduct.tprod R) fun (x : ι) => m
                                                  @[simp]
                                                  theorem PiTensorProduct.subsingletonEquiv_apply_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [Subsingleton ι] (i : ι) (f : ιM) :
                                                  noncomputable def PiTensorProduct.tmulEquiv {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] :
                                                  TensorProduct R (PiTensorProduct R fun (x : ι) => M) (PiTensorProduct R fun (x : ι₂) => M) ≃ₗ[R] PiTensorProduct R fun (x : ι ι₂) => M

                                                  Equivalence between a TensorProduct of PiTensorProducts and a single PiTensorProduct indexed by a Sum type.

                                                  For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem PiTensorProduct.tmulEquiv_apply {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] (a : ιM) (b : ι₂M) :
                                                    (PiTensorProduct.tmulEquiv R M) (((PiTensorProduct.tprod R) fun (i : ι) => a i) ⊗ₜ[R] (PiTensorProduct.tprod R) fun (i : ι₂) => b i) = (PiTensorProduct.tprod R) fun (i : ι ι₂) => Sum.elim a b i
                                                    @[simp]
                                                    theorem PiTensorProduct.tmulEquiv_symm_apply {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] (a : ι ι₂M) :
                                                    (PiTensorProduct.tmulEquiv R M).symm ((PiTensorProduct.tprod R) fun (i : ι ι₂) => a i) = ((PiTensorProduct.tprod R) fun (i : ι) => a (Sum.inl i)) ⊗ₜ[R] (PiTensorProduct.tprod R) fun (i : ι₂) => a (Sum.inr i)
                                                    noncomputable instance PiTensorProduct.instAddCommGroup {ι : Type u_1} {R : Type u_2} [CommRing R] {s : ιType u_3} [(i : ι) → AddCommGroup (s i)] [(i : ι) → Module R (s i)] :
                                                    AddCommGroup (PiTensorProduct R fun (i : ι) => s i)
                                                    Equations