LeanPool.Monlib4.LinearAlgebra.PiDirectSum #

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.PiDirectSum.

theorem DirectSum.tensor_coe_zero {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] :

⇑0 = 0

source

theorem DirectSum.tensor_coe_add {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (x y : DirectSum (ι₁ × ι₂) fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)) :

⇑(x + y) = ⇑x + ⇑y

source

theorem DirectSum.tensor_coe_smul {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : DirectSum (ι₁ × ι₂) fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)) (r : R) :

⇑(r • x) = r • ⇑x

source

noncomputable def Pi.tensorOf {R : Type u_1} [CommSemiring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (i : ι₁ × ι₂) :

TensorProduct R (M₁ i.1) (M₂ i.2) →ₗ[R] TensorProduct R ((j : ι₁) → M₁ j) ((j : ι₂) → M₂ j)

Include one coordinate tensor factor into the tensor product of dependent function spaces.

Equations

Pi.tensorOf i = TensorProduct.map (LinearMap.single R M₁ i.1) (LinearMap.single R M₂ i.2)

Instances For

source

noncomputable def Pi.tensorProj {R : Type u_1} [CommSemiring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (i : ι₁ × ι₂) :

TensorProduct R ((j : ι₁) → M₁ j) ((j : ι₂) → M₂ j) →ₗ[R] TensorProduct R (M₁ i.1) (M₂ i.2)

Project the tensor product of dependent function spaces onto one coordinate tensor factor.

Equations

Pi.tensorProj i = TensorProduct.map (LinearMap.proj i.1) (LinearMap.proj i.2)

Instances For

source

noncomputable def directSumTensorToFun {R : Type u_1} [CommSemiring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] :

TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i) →ₗ[R] (i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)

The coordinatewise map from a tensor product of dependent functions to tensor factors.

Equations

directSumTensorToFun = { toFun := fun (x : TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) (i : ι₁ × ι₂) => (Pi.tensorProj i) x, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

theorem directSumTensorToFun_apply {R : Type u_1} [CommSemiring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : (i : ι₁) → M₁ i) (y : (i : ι₂) → M₂ i) (i : ι₁ × ι₂) :

directSumTensorToFun (x ⊗ₜ[R] y) i = x i.1 ⊗ₜ[R] y i.2

source

noncomputable def directSumTensorInvFun {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] :

((i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)) →ₗ[R] TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)

The finite-sum inverse to directSumTensorToFun.

Equations

directSumTensorInvFun = { toFun := fun (x : (i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)) => ∑ i : ι₁ × ι₂, (Pi.tensorOf i) (x i), map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

theorem Function.sum_update_eq_self {ι₁ : Type u_1} [DecidableEq ι₁] [Fintype ι₁] {M₁ : ι₁ → Type u_2} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] (x : (i : ι₁) → M₁ i) :

∑ x_1 : ι₁, update 0 x_1 (x x_1) = x

source

theorem directSumTensorInvFun_apply_to_fun {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) :

directSumTensorInvFun (directSumTensorToFun x) = x

source

theorem Pi.tensorProj_apply_pi_tensorOf {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (i j : ι₁ × ι₂) (x : (i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)) :

(tensorProj i) ((tensorOf j) (x j)) = if i = j then x i else 0

source

theorem directSumTensorToFun_apply_inv_fun {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : (i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)) :

directSumTensorToFun (directSumTensorInvFun x) = x

source

noncomputable def directSumTensor {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] :

TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i) ≃ₗ[R] (i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)

Linear equivalence between tensor products of finite dependent products and products of tensor factors.

Equations

directSumTensor = { toFun := ⇑directSumTensorToFun, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑directSumTensorInvFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem directSumTensor_symm_apply {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (a : (i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)) :

directSumTensor.symm a = directSumTensorInvFun a

source

@[simp]

theorem directSumTensor_apply {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (a : TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) (i : ι₁ × ι₂) :

directSumTensor a i = directSumTensorToFun a i

source

theorem directSumTensorToFun.map_mul {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → Ring (M₁ i₁)] [(i₂ : ι₂) → Ring (M₂ i₂)] [(i₁ : ι₁) → Algebra R (M₁ i₁)] [(i₂ : ι₂) → Algebra R (M₂ i₂)] (x y : TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) :

directSumTensorToFun (x * y) = directSumTensorToFun x * directSumTensorToFun y

source

theorem directSumTensorToFun.map_one {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → Ring (M₁ i₁)] [(i₂ : ι₂) → Ring (M₂ i₂)] [(i₁ : ι₁) → Algebra R (M₁ i₁)] [(i₂ : ι₂) → Algebra R (M₂ i₂)] :

directSumTensorToFun 1 = 1

source

noncomputable def directSumTensorAlgEquiv (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [CommRing R] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type u_4) (M₂ : ι₂ → Type u_5) [(i₁ : ι₁) → Ring (M₁ i₁)] [(i₂ : ι₂) → Ring (M₂ i₂)] [(i₁ : ι₁) → Algebra R (M₁ i₁)] [(i₂ : ι₂) → Algebra R (M₂ i₂)] :

TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i) ≃ₐ[R] (i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)

Algebra equivalence induced by directSumTensor for finite dependent products.

Equations

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

Instances For

source

@[simp]

theorem directSumTensorAlgEquiv_symm_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [CommRing R] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type u_4) (M₂ : ι₂ → Type u_5) [(i₁ : ι₁) → Ring (M₁ i₁)] [(i₂ : ι₂) → Ring (M₂ i₂)] [(i₁ : ι₁) → Algebra R (M₁ i₁)] [(i₂ : ι₂) → Algebra R (M₂ i₂)] (x : (i : ι₁ × ι₂) → TensorProduct R (M₁ i.1) (M₂ i.2)) :

(directSumTensorAlgEquiv R M₁ M₂).symm x = directSumTensorInvFun x

source

@[simp]

theorem directSumTensorAlgEquiv_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [CommRing R] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type u_4) (M₂ : ι₂ → Type u_5) [(i₁ : ι₁) → Ring (M₁ i₁)] [(i₂ : ι₂) → Ring (M₂ i₂)] [(i₁ : ι₁) → Algebra R (M₁ i₁)] [(i₂ : ι₂) → Algebra R (M₂ i₂)] (x : TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) (i : ι₁ × ι₂) :

(directSumTensorAlgEquiv R M₁ M₂) x i = directSumTensorToFun x i

source

theorem Pi.tensor_ext_iff {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [Finite ι₁] [Finite ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (x z : (i : ι₁) → M₁ i) (y w : (i : ι₂) → M₂ i) :

x ⊗ₜ[R] y = z ⊗ₜ[R] w ↔ ∀ (i : ι₁) (j : ι₂), x i ⊗ₜ[R] y j = z i ⊗ₜ[R] w j

source

theorem Pi.tensor_ext {R : Type u_1} [CommRing R] {ι₁ : Type u_2} {ι₂ : Type u_3} [Finite ι₁] [Finite ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] {x z : (i : ι₁) → M₁ i} (y w : (i : ι₂) → M₂ i) :

(∀ (i : ι₁) (j : ι₂), x i ⊗ₜ[R] y j = z i ⊗ₜ[R] w j) → x ⊗ₜ[R] y = z ⊗ₜ[R] w

source

def LinearMap.piPiProd (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] :

((i : ι₁ × ι₂) → φ i.1 →ₗ[R] ψ i.2) ≃ₗ[S] (i : ι₁) → (j : ι₂) → φ i →ₗ[R] ψ j

Reindex linear maps out of a product-shaped dependent family.

Equations

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

Instances For

source

@[simp]

theorem LinearMap.piPiProd_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] (f : (i : ι₁ × ι₂) → φ i.1 →ₗ[R] ψ i.2) (j : ι₁) (k : ι₂) :

(piPiProd R φ ψ S) f j k = f (j, k)

source

@[simp]

theorem LinearMap.piPiProd_symm_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] (f : (i : ι₁) → (j : ι₂) → φ i →ₗ[R] ψ j) (i : ι₁ × ι₂) :

(piPiProd R φ ψ S).symm f i = f i.1 i.2

source

def LinearMap.piProdSwap (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] :

((i : ι₁) → (j : ι₂) → φ i →ₗ[R] ψ j) ≃ₗ[S] (j : ι₂) → (i : ι₁) → φ i →ₗ[R] ψ j

Swap the two function arguments in a doubly-indexed family of linear maps.

Equations

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

Instances For

source

@[simp]

theorem LinearMap.piProdSwap_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] (f : (i : ι₁) → (j : ι₂) → φ i →ₗ[R] ψ j) (j : ι₂) (i : ι₁) :

(piProdSwap R φ ψ S) f j i = f i j

source

@[simp]

theorem LinearMap.piProdSwap_symm_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] (f : (j : ι₂) → (i : ι₁) → φ i →ₗ[R] ψ j) (i : ι₁) (j : ι₂) :

(piProdSwap R φ ψ S).symm f i j = f j i

source

def LinearMap.rsum (R : Type u_1) {M : Type u_2} {ι : Type u_3} [Semiring R] (φ : ι → Type u_4) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (S : Type u_5) [AddCommMonoid M] [Module R M] [Semiring S] [(i : ι) → Module S (φ i)] [∀ (i : ι), SMulCommClass R S (φ i)] :

((i : ι) → M →ₗ[R] φ i) ≃ₗ[S] M →ₗ[R] (i : ι) → φ i

Linear equivalence between maps into a dependent product and dependent products of maps.

Equations

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

Instances For

source

@[simp]

theorem LinearMap.rsum_apply_apply (R : Type u_1) {M : Type u_2} {ι : Type u_3} [Semiring R] (φ : ι → Type u_4) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (S : Type u_5) [AddCommMonoid M] [Module R M] [Semiring S] [(i : ι) → Module S (φ i)] [∀ (i : ι), SMulCommClass R S (φ i)] (f : (i : ι) → M →ₗ[R] φ i) (c : M) (i : ι) :

((rsum R φ S) f) c i = (f i) c

source

@[simp]

theorem LinearMap.rsum_symm_apply_apply (R : Type u_1) {M : Type u_2} {ι : Type u_3} [Semiring R] (φ : ι → Type u_4) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (S : Type u_5) [AddCommMonoid M] [Module R M] [Semiring S] [(i : ι) → Module S (φ i)] [∀ (i : ι), SMulCommClass R S (φ i)] (f : M →ₗ[R] (i : ι) → φ i) (i : ι) (x : M) :

((rsum R φ S).symm f i) x = f x i

source

def LinearMap.lrsum (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Fintype ι₁] [DecidableEq ι₁] [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] :

((i : ι₁ × ι₂) → φ i.1 →ₗ[R] ψ i.2) ≃ₗ[S] ((i : ι₁) → φ i) →ₗ[R] (i : ι₂) → ψ i

Combine piPiProd, piProdSwap, lsum, and rsum into a two-sided reindexing equivalence.

Equations

LinearMap.lrsum R φ ψ S = (LinearMap.piPiProd R φ ψ S ≪≫ₗ LinearMap.piProdSwap R φ ψ S ≪≫ₗ LinearEquiv.piCongrRight fun (j : ι₂) => LinearMap.lsum R φ S) ≪≫ₗ LinearMap.rsum R ψ S

Instances For

source

@[simp]

theorem LinearMap.lrsum_apply_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Fintype ι₁] [DecidableEq ι₁] [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] (x : (i : ι₁ × ι₂) → φ i.1 →ₗ[R] ψ i.2) (c : (i : ι₁) → φ i) (i : ι₂) :

((lrsum R φ ψ S) x) c i = ∑ x_1 : ι₁, (x (x_1, i)) (c x_1)

source

@[simp]

theorem LinearMap.lrsum_symm_apply_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [Semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [(i : ι₁) → AddCommMonoid (φ i)] [(i : ι₁) → Module R (φ i)] [(i : ι₂) → AddCommMonoid (ψ i)] [(i : ι₂) → Module R (ψ i)] (S : Type u_6) [Fintype ι₁] [DecidableEq ι₁] [Semiring S] [(i : ι₂) → Module S (ψ i)] [∀ (i : ι₂), SMulCommClass R S (ψ i)] (a✝ : ((i : ι₁) → φ i) →ₗ[R] (i : ι₂) → ψ i) (i : ι₁ × ι₂) (x : φ i.1) :

((lrsum R φ ψ S).symm a✝ i) x = a✝ (Pi.single i.1 x) i.2