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 PhysLean.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 PhysLean.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 (PiTensorProduct R fun (i : ι1) => s1 i) (TensorProduct R (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 PhysLean.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 PhysLean.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 PhysLean.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 PhysLean.PiTensorProduct.instAddCommMonoidElim_physLean {ι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

• PhysLean.PiTensorProduct.instAddCommMonoidElim_physLean (Sum.inl i_2) = inst1 i_2
• PhysLean.PiTensorProduct.instAddCommMonoidElim_physLean (Sum.inr i_2) = inst2 i_2

instance PhysLean.PiTensorProduct.instModuleElim_physLean {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

• PhysLean.PiTensorProduct.instModuleElim_physLean (Sum.inl i_2) = inst1' i_2
• PhysLean.PiTensorProduct.instModuleElim_physLean (Sum.inr i_2) = inst2' i_2

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

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

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

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

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

• PhysLean.PiTensorProduct.tmulSymm = PiTensorProduct.lift PhysLean.PiTensorProduct.domCoprod

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

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

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

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

@[simp]

theorem PhysLean.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)