Imports
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Mathlib.LinearAlgebra.PiTensorProduct.BasicPi 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.
@[expose] public sectioninduction principals for pi tensor products
attribute [local ext] TensorProduct.extlemma induction_tmul {f g : ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) →ₗ[R] M}
(h : ∀ p q, f (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q)
= g (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q)) : f = g := R:Typeι1:Typeι2:TypeM:Typeinst✝²:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)inst✝¹:AddCommMonoid Minst✝:Module R Mf:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) →ₗ[R] Mg:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) →ₗ[R] Mh:∀ (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
R:Typeι1:Typeι2:TypeM:Typeinst✝²:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)inst✝¹:AddCommMonoid Minst✝:Module R Mf:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) →ₗ[R] Mg:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) →ₗ[R] Mh:∀ (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)x✝¹:(i : ι1) → s1 ix✝:(i : ι2) → s2 i⊢ (((((mk R (⨂[R] (i : ι1), s1 i) (⨂[R] (i : ι2), s2 i)).compr₂ₛₗ f).compMultilinearMap (PiTensorProduct.tprod R))
x✝¹).compMultilinearMap
(PiTensorProduct.tprod R))
x✝ =
(((((mk R (⨂[R] (i : ι1), s1 i) (⨂[R] (i : ι2), s2 i)).compr₂ₛₗ g).compMultilinearMap (PiTensorProduct.tprod R))
x✝¹).compMultilinearMap
(PiTensorProduct.tprod R))
x✝
All goals completed! 🐙lemma induction_assoc
{f g : ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i) ⊗[R] (⨂[R] i : ι3, s3 i)) →ₗ[R] M}
(h : ∀ p q m, 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 := R:Typeι1:Typeι2:Typeι3:TypeM:Typeinst✝²:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝¹:AddCommMonoid Minst✝:Module R Mf:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) ⊗[R] (⨂[R] (i : ι3), s3 i) →ₗ[R] Mg:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) ⊗[R] (⨂[R] (i : ι3), s3 i) →ₗ[R] Mh:∀ (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
R:Typeι1:Typeι2:Typeι3:TypeM:Typeinst✝²:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝¹:AddCommMonoid Minst✝:Module R Mf:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) ⊗[R] (⨂[R] (i : ι3), s3 i) →ₗ[R] Mg:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) ⊗[R] (⨂[R] (i : ι3), s3 i) →ₗ[R] Mh:∀ (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)x✝²:(i : ι1) → s1 ix✝¹:(i : ι2) → s2 ix✝:(i : ι3) → s3 i⊢ (((((((mk R (⨂[R] (i : ι1), s1 i) (⨂[R] (i : ι2), s2 i)).compr₂ₛₗ
((mk R ((⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i)) (⨂[R] (i : ι3), s3 i)).compr₂ₛₗ
f)).compMultilinearMap
(PiTensorProduct.tprod R))
x✝²).compMultilinearMap
(PiTensorProduct.tprod R))
x✝¹).compMultilinearMap
(PiTensorProduct.tprod R))
x✝ =
(((((((mk R (⨂[R] (i : ι1), s1 i) (⨂[R] (i : ι2), s2 i)).compr₂ₛₗ
((mk R ((⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i)) (⨂[R] (i : ι3), s3 i)).compr₂ₛₗ
g)).compMultilinearMap
(PiTensorProduct.tprod R))
x✝²).compMultilinearMap
(PiTensorProduct.tprod R))
x✝¹).compMultilinearMap
(PiTensorProduct.tprod R))
x✝
All goals completed! 🐙lemma induction_assoc'
{f g : (((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) ⊗[R] (⨂[R] i : ι3, s3 i)) →ₗ[R] M}
(h : ∀ p q m, 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 := R:Typeι1:Typeι2:Typeι3:TypeM:Typeinst✝²:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝¹:AddCommMonoid Minst✝:Module R Mf:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) ⊗[R] (⨂[R] (i : ι3), s3 i) →ₗ[R] Mg:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) ⊗[R] (⨂[R] (i : ι3), s3 i) →ₗ[R] Mh:∀ (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
R:Typeι1:Typeι2:Typeι3:TypeM:Typeinst✝²:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝¹:AddCommMonoid Minst✝:Module R Mf:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) ⊗[R] (⨂[R] (i : ι3), s3 i) →ₗ[R] Mg:(⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i) ⊗[R] (⨂[R] (i : ι3), s3 i) →ₗ[R] Mh:∀ (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)x✝²:(i : ι1) → s1 ix✝¹:(i : ι2) → s2 ix✝:(i : ι3) → s3 i⊢ (((((((mk R (⨂[R] (i : ι1), s1 i) (⨂[R] (i : ι2), s2 i)).compr₂ₛₗ
((mk R ((⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i)) (⨂[R] (i : ι3), s3 i)).compr₂ₛₗ
f)).compMultilinearMap
(PiTensorProduct.tprod R))
x✝²).compMultilinearMap
(PiTensorProduct.tprod R))
x✝¹).compMultilinearMap
(PiTensorProduct.tprod R))
x✝ =
(((((((mk R (⨂[R] (i : ι1), s1 i) (⨂[R] (i : ι2), s2 i)).compr₂ₛₗ
((mk R ((⨂[R] (i : ι1), s1 i) ⊗[R] (⨂[R] (i : ι2), s2 i)) (⨂[R] (i : ι3), s3 i)).compr₂ₛₗ
g)).compMultilinearMap
(PiTensorProduct.tprod R))
x✝²).compMultilinearMap
(PiTensorProduct.tprod R))
x✝¹).compMultilinearMap
(PiTensorProduct.tprod R))
x✝
All goals completed! 🐙lemma induction_tmul_mod
{f g : ((⨂[R] i : ι1, s1 i) ⊗[R] N) →ₗ[R] M}
(h : ∀ p m, f (PiTensorProduct.tprod R p ⊗ₜ[R] m) = g (PiTensorProduct.tprod R p ⊗ₜ[R] m)) :
f = g := R:Typeι1:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Nf:(⨂[R] (i : ι1), s1 i) ⊗[R] N →ₗ[R] Mg:(⨂[R] (i : ι1), s1 i) ⊗[R] N →ₗ[R] Mh:∀ (p : (i : ι1) → s1 i) (m : N), f ((PiTensorProduct.tprod R) p ⊗ₜ[R] m) = g ((PiTensorProduct.tprod R) p ⊗ₜ[R] m)⊢ f = g
R:Typeι1:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Nf:(⨂[R] (i : ι1), s1 i) ⊗[R] N →ₗ[R] Mg:(⨂[R] (i : ι1), s1 i) ⊗[R] N →ₗ[R] Mh:∀ (p : (i : ι1) → s1 i) (m : N), f ((PiTensorProduct.tprod R) p ⊗ₜ[R] m) = g ((PiTensorProduct.tprod R) p ⊗ₜ[R] m)x✝¹:(i : ι1) → s1 ix✝:N⊢ ((((mk R (⨂[R] (i : ι1), s1 i) N).compr₂ₛₗ f).compMultilinearMap (PiTensorProduct.tprod R)) x✝¹) x✝ =
((((mk R (⨂[R] (i : ι1), s1 i) N).compr₂ₛₗ g).compMultilinearMap (PiTensorProduct.tprod R)) x✝¹) x✝
All goals completed! 🐙lemma induction_mod_tmul
{f g : (N ⊗[R] (⨂[R] i : ι1, s1 i)) →ₗ[R] M}
(h : ∀ m p, f (m ⊗ₜ[R] PiTensorProduct.tprod R p) = g (m ⊗ₜ[R] PiTensorProduct.tprod R p)) :
f = g := R:Typeι1:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Nf:N ⊗[R] (⨂[R] (i : ι1), s1 i) →ₗ[R] Mg:N ⊗[R] (⨂[R] (i : ι1), s1 i) →ₗ[R] Mh:∀ (m : N) (p : (i : ι1) → s1 i), f (m ⊗ₜ[R] (PiTensorProduct.tprod R) p) = g (m ⊗ₜ[R] (PiTensorProduct.tprod R) p)⊢ f = g
R:Typeι1:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Nf:N ⊗[R] (⨂[R] (i : ι1), s1 i) →ₗ[R] Mg:N ⊗[R] (⨂[R] (i : ι1), s1 i) →ₗ[R] Mh:∀ (m : N) (p : (i : ι1) → s1 i), f (m ⊗ₜ[R] (PiTensorProduct.tprod R) p) = g (m ⊗ₜ[R] (PiTensorProduct.tprod R) p)x✝¹:Nx✝:(i : ι1) → s1 i⊢ ((((mk R N (⨂[R] (i : ι1), s1 i)).compr₂ₛₗ f) x✝¹).compMultilinearMap (PiTensorProduct.tprod R)) x✝ =
((((mk R N (⨂[R] (i : ι1), s1 i)).compr₂ₛₗ g) x✝¹).compMultilinearMap (PiTensorProduct.tprod R)) x✝
All goals completed! 🐙Dependent type version of PiTensorProduct.tmulEquiv
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.
instance : (i : ι1 ⊕ ι2) → AddCommMonoid ((fun i => Sum.elim s1 s2 i) i) := fun i =>
match i with
| Sum.inl i => inst1 i
| Sum.inr i => inst2 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.
instance : (i : ι1 ⊕ ι2) → Module R ((fun i => Sum.elim s1 s2 i) i) := fun i =>
match i with
| Sum.inl i => inst1' i
| Sum.inr i => inst2' i
Takes a map (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i to the underlying map (i : ι1) → s1 i .
def pureInl (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) : (i : ι1) → s1 i :=
fun i => f (Sum.inl i)
Takes a map (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i to the underlying map (i : ι2) → s2 i .
def pureInr (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) : (i : ι2) → s2 i :=
fun i => f (Sum.inr i)omit inst1 inst2lemma pureInl_update_left [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 := ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v1:s1 x⊢ pureInl (Function.update f (Sum.inl x) v1) = Function.update (pureInl f) x v1
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v1:s1 xy:ι1⊢ pureInl (Function.update f (Sum.inl x) v1) y = Function.update (pureInl f) x v1 y
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v1:s1 xy:ι1⊢ (if h : y = x then ⋯ ▸ v1 else f (Sum.inl y)) = if h : y = x then ⋯ ▸ v1 else f (Sum.inl y)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v1:s1 xy:ι1h✝:y = x⊢ ⋯ ▸ v1 = ⋯ ▸ v1ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v1:s1 xy:ι1h✝:¬y = x⊢ f (Sum.inl y) = f (Sum.inl y)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v1:s1 xy:ι1h✝:y = x⊢ ⋯ ▸ v1 = ⋯ ▸ v1 ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v1:s1 xy:ι1h:y = x⊢ ⋯ ▸ v1 = ⋯ ▸ v1
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 iy:ι1v1:s1 y⊢ ⋯ ▸ v1 = ⋯ ▸ v1
All goals completed! 🐙
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι1f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v1:s1 xy:ι1h✝:¬y = x⊢ f (Sum.inl y) = f (Sum.inl y) All goals completed! 🐙lemma pureInr_update_left (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι1)
(v2 : s1 x) :
pureInr (Function.update f (Sum.inl x) v2) = (pureInr f) := ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v2:s1 x⊢ pureInr (Function.update f (Sum.inl x) v2) = pureInr f
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1v2:s1 xy:ι2⊢ pureInr (Function.update f (Sum.inl x) v2) y = pureInr f y
All goals completed! 🐙lemma pureInr_update_right [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 := ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v2:s2 x⊢ pureInr (Function.update f (Sum.inr x) v2) = Function.update (pureInr f) x v2
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v2:s2 xy:ι2⊢ pureInr (Function.update f (Sum.inr x) v2) y = Function.update (pureInr f) x v2 y
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v2:s2 xy:ι2⊢ (if h : y = x then ⋯ ▸ v2 else f (Sum.inr y)) = if h : y = x then ⋯ ▸ v2 else f (Sum.inr y)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v2:s2 xy:ι2h✝:y = x⊢ ⋯ ▸ v2 = ⋯ ▸ v2ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v2:s2 xy:ι2h✝:¬y = x⊢ f (Sum.inr y) = f (Sum.inr y)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v2:s2 xy:ι2h✝:y = x⊢ ⋯ ▸ v2 = ⋯ ▸ v2 ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v2:s2 xy:ι2h:y = x⊢ ⋯ ▸ v2 = ⋯ ▸ v2
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 iy:ι2v2:s2 y⊢ ⋯ ▸ v2 = ⋯ ▸ v2
All goals completed! 🐙
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq (ι1 ⊕ ι2)inst✝:DecidableEq ι2f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v2:s2 xy:ι2h✝:¬y = x⊢ f (Sum.inr y) = f (Sum.inr y) All goals completed! 🐙lemma pureInl_update_right (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι2)
(v1 : s2 x) :
pureInl (Function.update f (Sum.inr x) v1) = (pureInl f) := ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v1:s2 x⊢ pureInl (Function.update f (Sum.inr x) v1) = pureInl f
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι2v1:s2 xy:ι1⊢ pureInl (Function.update f (Sum.inr x) v1) y = pureInl f y
All goals completed! 🐙
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.
set_option backward.isDefEq.respectTransparency false indef domCoprod :
MultilinearMap R (Sum.elim s1 s2) ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) where
toFun f := (PiTensorProduct.tprod R (pureInl f)) ⊗ₜ
(PiTensorProduct.tprod R (pureInr f))
map_update_add' f xy v1 v2 := R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2v1:Sum.elim s1 s2 xyv2:Sum.elim s1 s2 xy⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f xy (v1 + v2))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy (v1 + v2))) =
(PiTensorProduct.tprod R) (pureInl (Function.update f xy v1)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy v1)) +
(PiTensorProduct.tprod R) (pureInl (Function.update f xy v2)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy v2))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2v1:Sum.elim s1 s2 xyv2:Sum.elim s1 s2 xythis:DecidableEq (ι1 ⊕ ι2)⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f xy (v1 + v2))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy (v1 + v2))) =
(PiTensorProduct.tprod R) (pureInl (Function.update f xy v1)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy v1)) +
(PiTensorProduct.tprod R) (pureInl (Function.update f xy v2)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy v2))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2v1:Sum.elim s1 s2 xyv2:Sum.elim s1 s2 xythis✝:DecidableEq (ι1 ⊕ ι2)this:DecidableEq ι1⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f xy (v1 + v2))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy (v1 + v2))) =
(PiTensorProduct.tprod R) (pureInl (Function.update f xy v1)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy v1)) +
(PiTensorProduct.tprod R) (pureInl (Function.update f xy v2)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy v2))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2v1:Sum.elim s1 s2 xyv2:Sum.elim s1 s2 xythis✝¹:DecidableEq (ι1 ⊕ ι2)this✝:DecidableEq ι1this:DecidableEq ι2⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f xy (v1 + v2))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy (v1 + v2))) =
(PiTensorProduct.tprod R) (pureInl (Function.update f xy v1)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy v1)) +
(PiTensorProduct.tprod R) (pureInl (Function.update f xy v2)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy v2))
match xy with
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy✝:ι1 ⊕ ι2this✝¹:DecidableEq (ι1 ⊕ ι2)this✝:DecidableEq ι1this:DecidableEq ι2xy:ι1v1:Sum.elim s1 s2 (Sum.inl xy)v2:Sum.elim s1 s2 (Sum.inl xy)⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inl xy) (v1 + v2))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inl xy) (v1 + v2))) =
(PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inl xy) v1)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inl xy) v1)) +
(PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inl xy) v2)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inl xy) v2))
All goals completed! 🐙
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy✝:ι1 ⊕ ι2this✝¹:DecidableEq (ι1 ⊕ ι2)this✝:DecidableEq ι1this:DecidableEq ι2xy:ι2v1:Sum.elim s1 s2 (Sum.inr xy)v2:Sum.elim s1 s2 (Sum.inr xy)⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inr xy) (v1 + v2))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inr xy) (v1 + v2))) =
(PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inr xy) v1)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inr xy) v1)) +
(PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inr xy) v2)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inr xy) v2))
All goals completed! 🐙
map_update_smul' f xy r p := R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2r:Rp:Sum.elim s1 s2 xy⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f xy (r • p))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy (r • p))) =
r •
(PiTensorProduct.tprod R) (pureInl (Function.update f xy p)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy p))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2r:Rp:Sum.elim s1 s2 xythis:DecidableEq (ι1 ⊕ ι2)⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f xy (r • p))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy (r • p))) =
r •
(PiTensorProduct.tprod R) (pureInl (Function.update f xy p)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy p))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2r:Rp:Sum.elim s1 s2 xythis✝:DecidableEq (ι1 ⊕ ι2)this:DecidableEq ι1⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f xy (r • p))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy (r • p))) =
r •
(PiTensorProduct.tprod R) (pureInl (Function.update f xy p)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy p))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2r:Rp:Sum.elim s1 s2 xythis✝¹:DecidableEq (ι1 ⊕ ι2)this✝:DecidableEq ι1this:DecidableEq ι2⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f xy (r • p))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy (r • p))) =
r •
(PiTensorProduct.tprod R) (pureInl (Function.update f xy p)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f xy p))
match xy with
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2r:Rthis✝¹:DecidableEq (ι1 ⊕ ι2)this✝:DecidableEq ι1this:DecidableEq ι2x:ι1p:Sum.elim s1 s2 (Sum.inl x)⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inl x) (r • p))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inl x) (r • p))) =
r •
(PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inl x) p)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inl x) p))
All goals completed! 🐙
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq (ι1 ⊕ ι2)f:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ixy:ι1 ⊕ ι2r:Rthis✝¹:DecidableEq (ι1 ⊕ ι2)this✝:DecidableEq ι1this:DecidableEq ι2y:ι2p:Sum.elim s1 s2 (Sum.inr y)⊢ (PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inr y) (r • p))) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inr y) (r • p))) =
r •
(PiTensorProduct.tprod R) (pureInl (Function.update f (Sum.inr y) p)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (Function.update f (Sum.inr y) p))
All goals completed! 🐙
Expand PiTensorProduct on sums into a TensorProduct of two factors.
def tmulSymm : (⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i) →ₗ[R]
((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) := PiTensorProduct.lift domCoprod
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.
def elimPureTensor (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i) : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i :=
fun x =>
match x with
| Sum.inl x => p x
| Sum.inr x => q xomit inst1 inst2lemma elimPureTensor_update_right (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 := ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 y⊢ elimPureTensor p (Function.update q y r) = Function.update (elimPureTensor p q) (Sum.inr y) r
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx:ι1 ⊕ ι2⊢ elimPureTensor p (Function.update q y r) x = Function.update (elimPureTensor p q) (Sum.inr y) r x
match x with
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι1⊢ elimPureTensor p (Function.update q y r) (Sum.inl x) = Function.update (elimPureTensor p q) (Sum.inr y) r (Sum.inl x)
All goals completed! 🐙
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι2⊢ elimPureTensor p (Function.update q y r) (Sum.inr x) = Function.update (elimPureTensor p q) (Sum.inr y) r (Sum.inr x)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι2⊢ Function.update q y r x = Function.update (elimPureTensor p q) (Sum.inr y) r (Sum.inr x)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι2⊢ (if h : x = y then ⋯ ▸ r else q x) = if h : x = y then ⋯ ▸ r else elimPureTensor p q (Sum.inr x)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι2h✝:x = y⊢ ⋯ ▸ r = ⋯ ▸ rι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι2h✝:¬x = y⊢ q x = elimPureTensor p q (Sum.inr x)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι2h✝:x = y⊢ ⋯ ▸ r = ⋯ ▸ r ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι2h:x = y⊢ ⋯ ▸ r = ⋯ ▸ r
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix✝:ι1 ⊕ ι2x:ι2r:s2 x⊢ ⋯ ▸ r = ⋯ ▸ r
All goals completed! 🐙
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy:ι2r:s2 yx✝:ι1 ⊕ ι2x:ι2h✝:¬x = y⊢ q x = elimPureTensor p q (Sum.inr x) All goals completed! 🐙@[simp]
lemma elimPureTensor_update_left (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 := ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 x⊢ elimPureTensor (Function.update p x r) q = Function.update (elimPureTensor p q) (Sum.inl x) r
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy:ι1 ⊕ ι2⊢ elimPureTensor (Function.update p x r) q y = Function.update (elimPureTensor p q) (Sum.inl x) r y
match y with
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι1⊢ elimPureTensor (Function.update p x r) q (Sum.inl y) = Function.update (elimPureTensor p q) (Sum.inl x) r (Sum.inl y)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι1⊢ Function.update p x r y = Function.update (elimPureTensor p q) (Sum.inl x) r (Sum.inl y)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι1⊢ (if h : y = x then ⋯ ▸ r else p y) = if h : y = x then ⋯ ▸ r else elimPureTensor p q (Sum.inl y)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι1h✝:y = x⊢ ⋯ ▸ r = ⋯ ▸ rι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι1h✝:¬y = x⊢ p y = elimPureTensor p q (Sum.inl y)
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι1h✝:y = x⊢ ⋯ ▸ r = ⋯ ▸ r ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι1h:y = x⊢ ⋯ ▸ r = ⋯ ▸ r
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 iy✝:ι1 ⊕ ι2y:ι1r:s1 y⊢ ⋯ ▸ r = ⋯ ▸ r
All goals completed! 🐙
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι1h✝:¬y = x⊢ p y = elimPureTensor p q (Sum.inl y) All goals completed! 🐙
ι1:Typeι2:Types1:ι1 → Types2:ι2 → Typeinst✝¹:DecidableEq ι1inst✝:DecidableEq ι2p:(i : ι1) → s1 iq:(i : ι2) → s2 ix:ι1r:s1 xy✝:ι1 ⊕ ι2y:ι2⊢ elimPureTensor (Function.update p x r) q (Sum.inr y) = Function.update (elimPureTensor p q) (Sum.inl x) r (Sum.inr y)
All goals completed! 🐙
The multilinear map valued in multilinear maps defined by combining
(i : ι1) → s1 i and q : (i : ι2) → s2 i into a PiTensorProduct.
set_option backward.isDefEq.respectTransparency false indef elimPureTensorMulLin : MultilinearMap R s1
(MultilinearMap R s2 (⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i)) where
toFun p := {
toFun := fun q => PiTensorProduct.tprod R (elimPureTensor p q)
map_update_add' := fun m x v1 v2 => R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Np:(i : ι1) → s1 iinst✝:DecidableEq ι2m:(i : ι2) → s2 ix:ι2v1:s2 xv2:s2 x⊢ (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x (v1 + v2))) =
(PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v1)) +
(PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v2))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Np:(i : ι1) → s1 iinst✝:DecidableEq ι2m:(i : ι2) → s2 ix:ι2v1:s2 xv2:s2 xthis:DecidableEq ι2⊢ (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x (v1 + v2))) =
(PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v1)) +
(PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v2))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Np:(i : ι1) → s1 iinst✝:DecidableEq ι2m:(i : ι2) → s2 ix:ι2v1:s2 xv2:s2 xthis✝:DecidableEq ι2this:DecidableEq ι1⊢ (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x (v1 + v2))) =
(PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v1)) +
(PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v2))
All goals completed! 🐙
map_update_smul' := fun m x r v => R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Np:(i : ι1) → s1 iinst✝:DecidableEq ι2m:(i : ι2) → s2 ix:ι2r:Rv:s2 x⊢ (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x (r • v))) =
r • (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Np:(i : ι1) → s1 iinst✝:DecidableEq ι2m:(i : ι2) → s2 ix:ι2r:Rv:s2 xthis:DecidableEq ι2⊢ (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x (r • v))) =
r • (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v))
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Np:(i : ι1) → s1 iinst✝:DecidableEq ι2m:(i : ι2) → s2 ix:ι2r:Rv:s2 xthis✝:DecidableEq ι2this:DecidableEq ι1⊢ (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x (r • v))) =
r • (PiTensorProduct.tprod R) (elimPureTensor p (Function.update m x v))
All goals completed! 🐙}
map_update_add' p x v1 v2 := R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1v1:s1 xv2:s1 x⊢ { toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (v1 + v2)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } =
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v1) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } +
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v2) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1v1:s1 xv2:s1 xthis:DecidableEq ι1⊢ { toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (v1 + v2)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } =
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v1) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } +
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v2) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1v1:s1 xv2:s1 xthis✝:DecidableEq ι1this:DecidableEq ι2⊢ { toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (v1 + v2)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } =
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v1) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } +
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v2) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1v1:s1 xv2:s1 xthis✝:DecidableEq ι1this:DecidableEq ι2⊢ ∀ (x_1 : (i : ι2) → s2 i),
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (v1 + v2)) q),
map_update_add' := ⋯, map_update_smul' := ⋯ }
x_1 =
({ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v1) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } +
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v2) q), map_update_add' := ⋯,
map_update_smul' := ⋯ })
x_1
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1v1:s1 xv2:s1 xthis✝:DecidableEq ι1this:DecidableEq ι2y:(i : ι2) → s2 i⊢ { toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (v1 + v2)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
y =
({ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v1) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } +
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v2) q), map_update_add' := ⋯,
map_update_smul' := ⋯ })
y
All goals completed! 🐙
map_update_smul' p x r v := R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1r:Rv:s1 x⊢ { toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (r • v)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } =
r •
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1r:Rv:s1 xthis:DecidableEq ι1⊢ { toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (r • v)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } =
r •
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1r:Rv:s1 xthis✝:DecidableEq ι1this:DecidableEq ι2⊢ { toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (r • v)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ } =
r •
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1r:Rv:s1 xthis✝:DecidableEq ι1this:DecidableEq ι2⊢ ∀ (x_1 : (i : ι2) → s2 i),
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (r • v)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
x_1 =
(r •
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v) q), map_update_add' := ⋯,
map_update_smul' := ⋯ })
x_1
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁵:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝⁴:AddCommMonoid Minst✝³:Module R Minst✝²:AddCommMonoid Ninst✝¹:Module R Ninst✝:DecidableEq ι1p:(i : ι1) → s1 ix:ι1r:Rv:s1 xthis✝:DecidableEq ι1this:DecidableEq ι2y:(i : ι2) → s2 i⊢ { toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x (r • v)) q), map_update_add' := ⋯,
map_update_smul' := ⋯ }
y =
(r •
{ toFun := fun q => (PiTensorProduct.tprod R) (elimPureTensor (Function.update p x v) q), map_update_add' := ⋯,
map_update_smul' := ⋯ })
y
All goals completed! 🐙
Collapse a TensorProduct of PiTensorProduct into a PiTensorProduct.
def tmul : ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) →ₗ[R]
⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i := TensorProduct.lift {
toFun := fun a ↦
PiTensorProduct.lift <|
PiTensorProduct.lift elimPureTensorMulLin a,
map_add' := fun a b ↦ R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Na:⨂[R] (i : ι1), s1 ib:⨂[R] (i : ι1), s1 i⊢ PiTensorProduct.lift ((PiTensorProduct.lift elimPureTensorMulLin) (a + b)) =
PiTensorProduct.lift ((PiTensorProduct.lift elimPureTensorMulLin) a) +
PiTensorProduct.lift ((PiTensorProduct.lift elimPureTensorMulLin) b) All goals completed! 🐙
map_smul' := fun r a ↦ R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Nr:Ra:⨂[R] (i : ι1), s1 i⊢ PiTensorProduct.lift ((PiTensorProduct.lift elimPureTensorMulLin) (r • a)) =
(RingHom.id R) r • PiTensorProduct.lift ((PiTensorProduct.lift elimPureTensorMulLin) a) All goals completed! 🐙}
The equivalence formed by combining a TensorProduct into a PiTensorProduct.
def tmulEquiv : ((⨂[R] i : ι1, s1 i) ⊗[R] (⨂[R] i : ι2, s2 i)) ≃ₗ[R]
⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i :=
LinearEquiv.ofLinear tmul tmulSymm
(R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R N⊢ tmul ∘ₗ tmulSymm = LinearMap.id
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R N⊢ (tmul ∘ₗ tmulSymm).compMultilinearMap (PiTensorProduct.tprod R) =
LinearMap.id.compMultilinearMap (PiTensorProduct.tprod R)
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R N⊢ ∀ (x : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i),
((tmul ∘ₗ tmulSymm).compMultilinearMap (PiTensorProduct.tprod R)) x =
(LinearMap.id.compMultilinearMap (PiTensorProduct.tprod R)) x
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 i⊢ ((tmul ∘ₗ tmulSymm).compMultilinearMap (PiTensorProduct.tprod R)) p =
(LinearMap.id.compMultilinearMap (PiTensorProduct.tprod R)) p
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 i⊢ (elimPureTensorMulLin (pureInl p)) (pureInr p) = LinearMap.id ((PiTensorProduct.tprod R) p)
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 i⊢ (PiTensorProduct.tprod R) (elimPureTensor (pureInl p) (pureInr p)) = (PiTensorProduct.tprod R) p
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 i⊢ elimPureTensor (pureInl p) (pureInr p) = p
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix:ι1 ⊕ ι2⊢ elimPureTensor (pureInl p) (pureInr p) x = p x
match x with
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix✝:ι1 ⊕ ι2x:ι1⊢ elimPureTensor (pureInl p) (pureInr p) (Sum.inl x) = p (Sum.inl x) All goals completed! 🐙
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1 ⊕ ι2) → Sum.elim s1 s2 ix✝:ι1 ⊕ ι2x:ι2⊢ elimPureTensor (pureInl p) (pureInr p) (Sum.inr x) = p (Sum.inr x) All goals completed! 🐙)
(R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R N⊢ tmulSymm ∘ₗ tmul = LinearMap.id
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R N⊢ ∀ (p : (i : ι1) → s1 i) (q : (i : ι2) → s2 i),
(tmulSymm ∘ₗ tmul) ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) =
LinearMap.id ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q)
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1) → s1 iq:(i : ι2) → s2 i⊢ (tmulSymm ∘ₗ tmul) ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) =
LinearMap.id ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q)
R:Typeι1:Typeι2:Typeι3:TypeM:TypeN:Typeinst✝⁴:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)s3:ι3 → Typeinst3:(i : ι3) → AddCommMonoid (s3 i)inst3':(i : ι3) → Module R (s3 i)inst✝³:AddCommMonoid Minst✝²:Module R Minst✝¹:AddCommMonoid Ninst✝:Module R Np:(i : ι1) → s1 iq:(i : ι2) → s2 i⊢ (PiTensorProduct.tprod R) (pureInl (elimPureTensor p q)) ⊗ₜ[R]
(PiTensorProduct.tprod R) (pureInr (elimPureTensor p q)) =
(PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q
All goals completed! 🐙)@[simp]
lemma tmulEquiv_tmul_tprod (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) := R:Typeι1:Typeι2:Typeinst✝:CommSemiring Rs1:ι1 → Typeinst1:(i : ι1) → AddCommMonoid (s1 i)inst1':(i : ι1) → Module R (s1 i)s2:ι2 → Typeinst2:(i : ι2) → AddCommMonoid (s2 i)inst2':(i : ι2) → Module R (s2 i)p:(i : ι1) → s1 iq:(i : ι2) → s2 i⊢ tmulEquiv ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) =
(PiTensorProduct.tprod R) (elimPureTensor p q)
All goals completed! 🐙