Pi Tensor Products

The purpose of this file is to define some results about Pi tensor products not currently in Mathlib.

At some point these should either be up-streamed to Mathlib or replaced with definitions already in Mathlib.

induction principals for pi tensor products

theorem Physlib.PiTensorProduct.induction_tmul {R ι1 ι2 M : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] [AddCommMonoid M] [Module R M] {f g : TensorProduct R (PiTensorProduct R fun (i : ι1) => s1 i) (PiTensorProduct R fun (i : ι2) => s2 i) →ₗ[R] M} (h : ∀ (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i), f ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) = g ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q)) : f = g

theorem Physlib.PiTensorProduct.induction_assoc {R ι1 ι2 ι3 M : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] {s3 : ι3 → Type} [inst3 : (i : ι3) → AddCommMonoid (s3 i)] [inst3' : (i : ι3) → Module R (s3 i)] [AddCommMonoid M] [Module R M] {f g : TensorProduct R (TensorProduct R (PiTensorProduct R fun (i : ι1) => s1 i) (PiTensorProduct R fun (i : ι2) => s2 i)) (PiTensorProduct R fun (i : ι3) => s3 i) →ₗ[R] M} (h : ∀ (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) (m : (i : ι3) → s3 i), f ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q ⊗ₜ[R] (PiTensorProduct.tprod R) m) = g ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q ⊗ₜ[R] (PiTensorProduct.tprod R) m)) : f = g

theorem Physlib.PiTensorProduct.induction_assoc' {R ι1 ι2 ι3 M : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] {s3 : ι3 → Type} [inst3 : (i : ι3) → AddCommMonoid (s3 i)] [inst3' : (i : ι3) → Module R (s3 i)] [AddCommMonoid M] [Module R M] {f g : TensorProduct R (TensorProduct R (PiTensorProduct R fun (i : ι1) => s1 i) (PiTensorProduct R fun (i : ι2) => s2 i)) (PiTensorProduct R fun (i : ι3) => s3 i) →ₗ[R] M} (h : ∀ (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) (m : (i : ι3) → s3 i), f ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q ⊗ₜ[R] (PiTensorProduct.tprod R) m) = g ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q ⊗ₜ[R] (PiTensorProduct.tprod R) m)) : f = g

theorem Physlib.PiTensorProduct.induction_tmul_mod {R ι1 M N : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f g : TensorProduct R (PiTensorProduct R fun (i : ι1) => s1 i) N →ₗ[R] M} (h : ∀ (p : (i : ι1) → s1 i) (m : N), f ((PiTensorProduct.tprod R) p ⊗ₜ[R] m) = g ((PiTensorProduct.tprod R) p ⊗ₜ[R] m)) : f = g

theorem Physlib.PiTensorProduct.induction_mod_tmul {R ι1 M N : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f g : TensorProduct R N (PiTensorProduct R fun (i : ι1) => s1 i) →ₗ[R] M} (h : ∀ (m : N) (p : (i : ι1) → s1 i), f (m ⊗ₜ[R] (PiTensorProduct.tprod R) p) = g (m ⊗ₜ[R] (PiTensorProduct.tprod R) p)) : f = g

Dependent type version of PiTensorProduct.tmulEquiv

instance Physlib.PiTensorProduct.instAddCommMonoidElim_physlib {ι1 ι2 : Type} {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] (i : ι1 ⊕ ι2) : AddCommMonoid ((fun (i : ι1 ⊕ ι2) => Sum.elim s1 s2 i) i)

Given two maps s1 and s2 whose targets carry an instance of an additive commutative monoid, the target of the sum of these two maps also carry an instance thereof.

Equations

• Physlib.PiTensorProduct.instAddCommMonoidElim_physlib (Sum.inl i_2) = inst1 i_2
• Physlib.PiTensorProduct.instAddCommMonoidElim_physlib (Sum.inr i_2) = inst2 i_2

instance Physlib.PiTensorProduct.instModuleElim_physlib {R ι1 ι2 : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] (i : ι1 ⊕ ι2) : Module R ((fun (i : ι1 ⊕ ι2) => Sum.elim s1 s2 i) i)

Given two maps s1 and s2 whose targets carry an instance of a module over R, the target of the sum of these two maps also carry an instance thereof.

Equations

• Physlib.PiTensorProduct.instModuleElim_physlib (Sum.inl i_2) = inst1' i_2
• Physlib.PiTensorProduct.instModuleElim_physlib (Sum.inr i_2) = inst2' i_2

def Physlib.PiTensorProduct.pureInl {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (i : ι1) : s1 i

Takes a map (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i to the underlying map (i : ι1) → s1 i .

Equations

• Physlib.PiTensorProduct.pureInl f i = f (Sum.inl i)

def Physlib.PiTensorProduct.pureInr {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (i : ι2) : s2 i

Takes a map (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i to the underlying map (i : ι2) → s2 i .

Equations

• Physlib.PiTensorProduct.pureInr f i = f (Sum.inr i)

theorem Physlib.PiTensorProduct.pureInl_update_left {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} [DecidableEq (ι1 ⊕ ι2)] [DecidableEq ι1] (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι1) (v1 : s1 x) : pureInl (Function.update f (Sum.inl x) v1) = Function.update (pureInl f) x v1

theorem Physlib.PiTensorProduct.pureInr_update_left {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} [DecidableEq (ι1 ⊕ ι2)] (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι1) (v2 : s1 x) : pureInr (Function.update f (Sum.inl x) v2) = pureInr f

theorem Physlib.PiTensorProduct.pureInr_update_right {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} [DecidableEq (ι1 ⊕ ι2)] [DecidableEq ι2] (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι2) (v2 : s2 x) : pureInr (Function.update f (Sum.inr x) v2) = Function.update (pureInr f) x v2

theorem Physlib.PiTensorProduct.pureInl_update_right {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} [DecidableEq (ι1 ⊕ ι2)] (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι2) (v1 : s2 x) : pureInl (Function.update f (Sum.inr x) v1) = pureInl f

def Physlib.PiTensorProduct.domCoprod {R ι1 ι2 : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] : MultilinearMap R (Sum.elim s1 s2) (TensorProduct R (PiTensorProduct R fun (i : ι1) => s1 i) (PiTensorProduct R fun (i : ι2) => s2 i))

The multilinear map from (Sum.elim s1 s2) to ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) defined by splitting elements of (Sum.elim s1 s2) into two parts.

Equations

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

def Physlib.PiTensorProduct.tmulSymm {R ι1 ι2 : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] : (PiTensorProduct R fun (i : ι1 ⊕ ι2) => Sum.elim s1 s2 i) →ₗ[R] TensorProduct R (PiTensorProduct R fun (i : ι1) => s1 i) (PiTensorProduct R fun (i : ι2) => s2 i)

Expand PiTensorProduct on sums into a TensorProduct of two factors.

Equations

• Physlib.PiTensorProduct.tmulSymm = PiTensorProduct.lift Physlib.PiTensorProduct.domCoprod

def Physlib.PiTensorProduct.elimPureTensor {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) (i : ι1 ⊕ ι2) : Sum.elim s1 s2 i

Produces a map (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i from a map (i : ι1) → s1 i and a map q : (i : ι2) → s2 i.

Equations

• Physlib.PiTensorProduct.elimPureTensor p q (Sum.inl i_1) = p i_1
• Physlib.PiTensorProduct.elimPureTensor p q (Sum.inr i_1) = q i_1

theorem Physlib.PiTensorProduct.elimPureTensor_update_right {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} [DecidableEq ι1] [DecidableEq ι2] (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) (y : ι2) (r : s2 y) : elimPureTensor p (Function.update q y r) = Function.update (elimPureTensor p q) (Sum.inr y) r

@[simp]

theorem Physlib.PiTensorProduct.elimPureTensor_update_left {ι1 ι2 : Type} {s1 : ι1 → Type} {s2 : ι2 → Type} [DecidableEq ι1] [DecidableEq ι2] (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) (x : ι1) (r : s1 x) : elimPureTensor (Function.update p x r) q = Function.update (elimPureTensor p q) (Sum.inl x) r

def Physlib.PiTensorProduct.elimPureTensorMulLin {R ι1 ι2 : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] : MultilinearMap R s1 (MultilinearMap R s2 (PiTensorProduct R fun (i : ι1 ⊕ ι2) => Sum.elim s1 s2 i))

The multilinear map valued in multilinear maps defined by combining (i : ι1) → s1 i and q : (i : ι2) → s2 i into a PiTensorProduct.

Equations

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

def Physlib.PiTensorProduct.tmul {R ι1 ι2 : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] : TensorProduct R (PiTensorProduct R fun (i : ι1) => s1 i) (PiTensorProduct R fun (i : ι2) => s2 i) →ₗ[R] PiTensorProduct R fun (i : ι1 ⊕ ι2) => Sum.elim s1 s2 i

Collapse a TensorProduct of PiTensorProduct into a PiTensorProduct.

Equations

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

def Physlib.PiTensorProduct.tmulEquiv {R ι1 ι2 : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] : TensorProduct R (PiTensorProduct R fun (i : ι1) => s1 i) (PiTensorProduct R fun (i : ι2) => s2 i) ≃ₗ[R] PiTensorProduct R fun (i : ι1 ⊕ ι2) => Sum.elim s1 s2 i

The equivalence formed by combining a TensorProduct into a PiTensorProduct.

Equations

• Physlib.PiTensorProduct.tmulEquiv = LinearEquiv.ofLinear Physlib.PiTensorProduct.tmul Physlib.PiTensorProduct.tmulSymm ⋯ ⋯

@[simp]

theorem Physlib.PiTensorProduct.tmulEquiv_tmul_tprod {R ι1 ι2 : Type} [CommSemiring R] {s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)] {s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)] (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) : tmulEquiv ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) = (PiTensorProduct.tprod R) (elimPureTensor p q)