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, s 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

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

• 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)

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

• PiTensorProduct R s = AddCon.Quotient (addConGen (PiTensorProduct.Eqv R s))

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

Pretty printer defined by notation3 command.

Equations

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

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

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.

noncomputable 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 (PiTensorProduct R fun (i : ι) => s i)

Equations

• PiTensorProduct.instAddCommMonoidPiTensorProduct s = let __src := AddCon.addMonoid (addConGen (PiTensorProduct.Eqv R s)); AddCommMonoid.mk ⋯

noncomputable 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 (PiTensorProduct R fun (i : ι) => s i)

Equations

• PiTensorProduct.instInhabitedPiTensorProduct s = { default := 0 }

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

• PiTensorProduct.tprodCoeff R r f = (AddCon.mk' (addConGen (PiTensorProduct.Eqv R fun (i : ι) => s i))) (FreeAddMonoid.of (r, f))

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

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

• PiTensorProduct.liftAddHom φ C0 C0' C_add C_add_scalar C_smul = AddCon.lift (addConGen (PiTensorProduct.Eqv R s)) (FreeAddMonoid.lift φ) ⋯

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 x → motive y → motive (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

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

noncomputable 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 (PiTensorProduct R fun (i : ι) => s i)

Equations

• PiTensorProduct.instSMulPiTensorProduct = 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) : 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 : 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

• PiTensorProduct.distribMulAction' = DistribMulAction.mk ⋯ ⋯

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

• PiTensorProduct.module' = let __src := PiTensorProduct.distribMulAction'; Module.mk ⋯ ⋯

noncomputable 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 (PiTensorProduct R fun (i : ι) => s i)

Equations

• PiTensorProduct.instModulePiTensorProductToSemiringInstAddCommMonoidPiTensorProduct = PiTensorProduct.module'

noncomputable 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 (PiTensorProduct R fun (i : ι) => s i)

Equations

• ⋯ = ⋯

noncomputable 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 (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

• PiTensorProduct.tprod R = { toFun := PiTensorProduct.tprodCoeff R 1, map_add' := ⋯, map_smul' := ⋯ }

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

Pretty printer defined by notation3 command.

Equations

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

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

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.

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)] {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 x → motive y → motive (x + y)) : motive z

Induct using scaled versions of PiTensorProduct.tprod.

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 : LinearMap.compMultilinearMap φ₁ (PiTensorProduct.tprod R) = LinearMap.compMultilinearMap φ₂ (PiTensorProduct.tprod R)) : φ₁ = φ₂

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

• PiTensorProduct.liftAux φ = PiTensorProduct.liftAddHom (fun (p : R × ((i : ι) → s i)) => p.1 • φ p.2) ⋯ ⋯ ⋯ ⋯ ⋯

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 : PiTensorProduct R fun (i : ι) => s i) : (PiTensorProduct.liftAux φ) (r • x) = r • (PiTensorProduct.liftAux φ) x

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.

@[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 : 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} {φ' : (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) : (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

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

• PiTensorProduct.map f = PiTensorProduct.lift (MultilinearMap.compLinearMap (PiTensorProduct.tprod R) f)

@[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)

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 = LinearMap.comp (↑PiTensorProduct.lift) (PiTensorProduct.lift (MultilinearMap.piLinearMap (PiTensorProduct.tprod R)))

@[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.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

• PiTensorProduct.map₂ f = PiTensorProduct.lift (LinearMap.compMultilinearMap PiTensorProduct.piTensorHomMap (MultilinearMap.compLinearMap (PiTensorProduct.tprod R) f))

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

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

@[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.

@[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 : ι ≃ ι₂) : LinearMap.compMultilinearMap (↑(PiTensorProduct.reindex R s e)) (PiTensorProduct.tprod R) = (LinearEquiv.symm (MultilinearMap.domDomCongrLinearEquiv' R R s (PiTensorProduct R fun (i : ι₂) => s (e.symm i)) e)) (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 ((LinearEquiv.symm (MultilinearMap.domDomCongrLinearEquiv' R R s E e)) φ)

@[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 φ ∘ₗ ↑(LinearEquiv.symm (PiTensorProduct.reindex R s e)) = 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 ((LinearEquiv.symm (MultilinearMap.domDomCongrLinearEquiv' R R s E e)) φ)) 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 φ) ((LinearEquiv.symm (PiTensorProduct.reindex R s e)) 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 : ι ≃ ι₂) : LinearEquiv.symm (PiTensorProduct.reindex R (fun (x : ι) => M) e) = 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)] : PiTensorProduct.reindex R s (Equiv.refl ι) = LinearEquiv.refl R (PiTensorProduct R fun (i : ι) => s i)

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.

@[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) : (LinearEquiv.symm (PiTensorProduct.isEmptyEquiv ι)) r = r • (PiTensorProduct.tprod R) isEmptyElim

@[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) : (PiTensorProduct.isEmptyEquiv ι) ((PiTensorProduct.tprod R) f) = 1

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.

@[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 = (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) : (PiTensorProduct.subsingletonEquiv i) ((PiTensorProduct.tprod R) f) = f i

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

• PiTensorProduct.tmulEquiv R M = LinearEquiv.ofLinear PiTensorProduct.tmul PiTensorProduct.tmulSymm ⋯ ⋯

@[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) : (LinearEquiv.symm (PiTensorProduct.tmulEquiv R M)) ((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.instAddCommGroupPiTensorProductToCommSemiringToAddCommMonoid {ι : 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

• PiTensorProduct.instAddCommGroupPiTensorProductToCommSemiringToAddCommMonoid = Module.addCommMonoidToAddCommGroup R