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

• 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.
• tprod R f with f : ∀ i, s i is the tensor product of the vectors f i over all i : ι. This is bundled as a multilinear map from ∀ i, s i to ⨂[R] i, s i.
• liftAddHom constructs an AddMonoidHom from (⨂[R] i, s i) to some space F from a function φ : (R × ∀ i, s i) → F with the appropriate properties.
• lift φ with φ : MultilinearMap R s E is the corresponding linear map (⨂[R] i, s i) →ₗ[R] E. This is bundled as a linear equivalence.
• PiTensorProduct.reindex e re-indexes the components of ⨂[R] i : ι, M along e : ι ≃ ι₂.
• PiTensorProduct.tmulEquiv equivalence between a TensorProduct of PiTensorProducts and a single PiTensorProduct.

Notations

• ⨂[R] i, s i is defined as localized notation in locale TensorProduct.
• ⨂ₜ[R] i, f i with f : ∀ i, f i is defined globally as the tensor product of all the f i's.

Implementation notes

• We define it via FreeAddMonoid (R × ∀ i, s i) with the R representing a "hidden" tensor factor, rather than FreeAddMonoid (∀ i, s i) to ensure that, if ι is an empty type, the space is isomorphic to the base ring R.
• We have not restricted the index type ι to be a Fintype, as nothing we do here strictly requires it. However, problems may arise in the case where ι is infinite; use at your own caution.
• Instead of requiring DecidableEq ι as an argument to PiTensorProduct itself, we include it as an argument in the constructors of the relation. A decidability instance still has to come from somewhere due to the use of Function.update, but this hides it from the downstream user. See the implementation notes for MultilinearMap for an extended discussion of this choice.

TODO

• Define tensor powers, symmetric subspace, etc.
• API for the various ways ι can be split into subsets; connect this with the binary tensor product.
• Include connection with holors.
• Port more of the API from the binary tensor product over to this case.

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

• of_zero: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, f)) 0
• of_zero_scalar: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (f : (i : ι) → s i), PiTensorProduct.Eqv R s (FreeAddMonoid.of (0, f)) 0
• of_add: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (x : DecidableEq ι) (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i), PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, Function.update f i m₁) + FreeAddMonoid.of (r, Function.update f i m₂)) (FreeAddMonoid.of (r, Function.update f i (m₁ + m₂)))
• of_add_scalar: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (r r' : R) (f : (i : ι) → s i), PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, f) + FreeAddMonoid.of (r', f)) (FreeAddMonoid.of (r + r', f))
• of_smul: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (x : DecidableEq ι) (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, Function.update f i (r' • f i))) (FreeAddMonoid.of (r' * r, f))
• add_comm: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (x y : FreeAddMonoid (R × ((i : ι) → s i))), PiTensorProduct.Eqv R s (x + y) (y + x)

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

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.

def «term⨂[_]_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

def «term⨂[_]_,_» : Lean.ParserDescr

notation for tensor product over some indexed type

instance PiTensorProduct.instAddCommMonoidPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] (s : ι → Type u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] : AddCommMonoid (⨂[R] (i : ι), s i)

instance PiTensorProduct.instInhabitedPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] (s : ι → Type u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] : Inhabited (⨂[R] (i : ι), s i)

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) : ⨂[R] (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.

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) : PiTensorProduct.tprodCoeff R 0 f = 0

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) : PiTensorProduct.tprodCoeff R z f = 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) : PiTensorProduct.tprodCoeff R z (Function.update f i m₁) + PiTensorProduct.tprodCoeff R z (Function.update f i m₂) = PiTensorProduct.tprodCoeff R z (Function.update f i (m₁ + m₂))

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) : PiTensorProduct.tprodCoeff R z₁ f + PiTensorProduct.tprodCoeff R z₂ f = PiTensorProduct.tprodCoeff R (z₁ + z₂) f

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) : PiTensorProduct.tprodCoeff R z (Function.update f i (r • f i)) = PiTensorProduct.tprodCoeff R (r * z) f

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)] : PiTensorProduct.tprodCoeff R z (Function.update f i (r • f i)) = PiTensorProduct.tprodCoeff R (r • z) f

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)) : (⨂[R] (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.

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)] {C : (⨂[R] (i : ι), s i) → Prop} (z : ⨂[R] (i : ι), s i) (C1 : {r : R} → {f : (i : ι) → s i} → C (PiTensorProduct.tprodCoeff R r f)) (Cp : {x y : ⨂[R] (i : ι), s i} → C x → C y → C (x + y)) : C z

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₁ (⨂[R] (i : ι), s i)

instance PiTensorProduct.instSMulPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] : SMul R (⨂[R] (i : ι), s i)

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) : r • PiTensorProduct.tprodCoeff R z f = PiTensorProduct.tprodCoeff R (r • z) f

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 : ⨂[R] (i : ι), s i) (y : ⨂[R] (i : ι), s i) : r • (x + y) = r • x + r • y

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₁ (⨂[R] (i : ι), s i)

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₂ (⨂[R] (i : ι), s i)

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₂ (⨂[R] (i : ι), s i)

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₁ (⨂[R] (i : ι), s i)

instance PiTensorProduct.instModulePiTensorProductToSemiringInstAddCommMonoidPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] : Module R (⨂[R] (i : ι), s i)

instance PiTensorProduct.instSMulCommClassPiTensorProductInstSMulPiTensorProduct {ι : 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 (⨂[R] (i : ι), s i)

instance PiTensorProduct.instIsScalarTowerPiTensorProductToSMulToSemiringIdInstSMulPiTensorProduct {ι : 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 (⨂[R] (i : ι), s i)

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 (⨂[R] (i : ι), s i)

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

def PiTensorProduct.«term⨂ₜ[_]_,_» : Lean.ParserDescr

pure tensor in tensor product over some index type

def PiTensorProduct.«term⨂ₜ[_]_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

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)] : ↑(PiTensorProduct.tprod R) = PiTensorProduct.tprodCoeff R 1

@[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) : PiTensorProduct.tprodCoeff R z f = z • ↑(PiTensorProduct.tprod R) f

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)] {C : (⨂[R] (i : ι), s i) → Prop} (z : ⨂[R] (i : ι), s i) (C1 : {r : R} → {f : (i : ι) → s i} → C (r • ↑(PiTensorProduct.tprod R) f)) (Cp : {x y : ⨂[R] (i : ι), s i} → C x → C y → C (x + y)) : C z

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] {φ₁ : (⨂[R] (i : ι), s i) →ₗ[R] E} {φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E} (H : LinearMap.compMultilinearMap φ₁ (PiTensorProduct.tprod R) = LinearMap.compMultilinearMap φ₂ (PiTensorProduct.tprod R)) : φ₁ = φ₂

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) : (⨂[R] (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.

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) : ↑(PiTensorProduct.liftAux φ) (↑(PiTensorProduct.tprod R) f) = ↑φ f

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) : ↑(PiTensorProduct.liftAux φ) (PiTensorProduct.tprodCoeff R z f) = z • ↑φ f

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 : ⨂[R] (i : ι), s i) : ↑(PiTensorProduct.liftAux φ) (r • x) = r • ↑(PiTensorProduct.liftAux φ) x

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] (⨂[R] (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 φ.

@[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} {φ' : (⨂[R] (i : ι), s i) →ₗ[R] E} (H : LinearMap.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} {φ' : (⨂[R] (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] (φ' : (⨂[R] (i : ι), s i) →ₗ[R] E) : ↑(LinearEquiv.symm PiTensorProduct.lift) φ' = LinearMap.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

def PiTensorProduct.reindex {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] (e : ι ≃ ι₂) : (⨂[R] (x : ι), M) ≃ₗ[R] ⨂[R] (x : ι₂), M

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

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

@[simp]

theorem PiTensorProduct.reindex_tprod {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ≃ ι₂) (f : ι → M) : ↑(PiTensorProduct.reindex R M e) (↑(PiTensorProduct.tprod R) f) = ⨂ₜ[R] (i : ι₂), f (↑e.symm i)

@[simp]

theorem PiTensorProduct.reindex_comp_tprod {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ≃ ι₂) : LinearMap.compMultilinearMap (↑(PiTensorProduct.reindex R M e)) (PiTensorProduct.tprod R) = MultilinearMap.domDomCongr e.symm (PiTensorProduct.tprod R)

@[simp]

theorem PiTensorProduct.lift_comp_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] {E : Type u_9} [AddCommMonoid E] [Module R E] (e : ι ≃ ι₂) (φ : MultilinearMap R (fun x => M) E) : LinearMap.comp (↑PiTensorProduct.lift φ) ↑(PiTensorProduct.reindex R M e) = ↑PiTensorProduct.lift (MultilinearMap.domDomCongr e.symm φ)

@[simp]

theorem PiTensorProduct.lift_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] {E : Type u_9} [AddCommMonoid E] [Module R E] (e : ι ≃ ι₂) (φ : MultilinearMap R (fun x => M) E) (x : ⨂[R] (x : ι), M) : ↑(↑PiTensorProduct.lift φ) (↑(PiTensorProduct.reindex R M e) x) = ↑(↑PiTensorProduct.lift (MultilinearMap.domDomCongr e.symm φ)) x

@[simp]

theorem PiTensorProduct.reindex_trans {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) : LinearEquiv.trans (PiTensorProduct.reindex R M e) (PiTensorProduct.reindex R M e') = PiTensorProduct.reindex R M (e.trans e')

@[simp]

theorem PiTensorProduct.reindex_reindex {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) (x : ⨂[R] (x : ι), M) : ↑(PiTensorProduct.reindex R M e') (↑(PiTensorProduct.reindex R M e) x) = ↑(PiTensorProduct.reindex R M (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 : ι ≃ ι₂) : LinearEquiv.symm (PiTensorProduct.reindex R M e) = PiTensorProduct.reindex R M e.symm

@[simp]

theorem PiTensorProduct.reindex_refl {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] : PiTensorProduct.reindex R M (Equiv.refl ι) = LinearEquiv.refl R (⨂[R] (x : ι), M)

@[simp]

theorem PiTensorProduct.isEmptyEquiv_symm_apply (ι : Type u_1) {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [IsEmpty ι] (r : R) : ↑(LinearEquiv.symm (PiTensorProduct.isEmptyEquiv ι)) r = r • ↑(PiTensorProduct.tprod R) isEmptyElim

def PiTensorProduct.isEmptyEquiv (ι : Type u_1) {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [IsEmpty ι] : (⨂[R] (x : ι), M) ≃ₗ[R] R

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

@[simp]

theorem PiTensorProduct.isEmptyEquiv_apply_tprod (ι : Type u_1) {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [IsEmpty ι] (f : ι → M) : ↑(PiTensorProduct.isEmptyEquiv ι) (↑(PiTensorProduct.tprod R) f) = 1

@[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) : ↑(LinearEquiv.symm (PiTensorProduct.subsingletonEquiv i₀)) m = ⨂ₜ[R] (x : ι), m

def PiTensorProduct.subsingletonEquiv {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [Subsingleton ι] (i₀ : ι) : (⨂[R] (x : ι), M) ≃ₗ[R] M

Tensor product of M over a singleton set is equivalent to 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) : ↑(PiTensorProduct.subsingletonEquiv i) (↑(PiTensorProduct.tprod R) f) = f i

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 (⨂[R] (x : ι), M) (⨂[R] (x : ι₂), M) ≃ₗ[R] ⨂[R] (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.

@[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) ((⨂ₜ[R] (i : ι), a i) ⊗ₜ[R] ⨂ₜ[R] (i : ι₂), b i) = ⨂ₜ[R] (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) : ↑(LinearEquiv.symm (PiTensorProduct.tmulEquiv R M)) (⨂ₜ[R] (i : ι ⊕ ι₂), a i) = (⨂ₜ[R] (i : ι), a (Sum.inl i)) ⊗ₜ[R] ⨂ₜ[R] (i : ι₂), a (Sum.inr i)

instance PiTensorProduct.instAddCommGroupPiTensorProductToCommSemiringToAddCommMonoid {ι : Type u_1} {R : Type u_2} [CommRing R] {s : ι → Type u_3} [(i : ι) → AddCommGroup (s i)] [(i : ι) → Module R (s i)] : AddCommGroup (⨂[R] (i : ι), s i)