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

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 : DirectSum (ι₁ × ι₂) fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)) (y : DirectSum (ι₁ × ι₂) fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)) : ⇑(x + y) = ⇑x + ⇑y

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

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)

Equations

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

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)

Equations

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

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)

Equations

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

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

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)

Equations

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

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 : ι₁, Function.update 0 x_1 (x x_1) = x

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

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)) : (Pi.tensorProj i) ((Pi.tensorOf j) (x j)) = if i = j then x i else 0

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

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)

Equations

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

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

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

theorem directSumTensorToFun.map_mul {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₁ : ι₁) → 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)) (y : TensorProduct R ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) : directSumTensorToFun (x * y) = directSumTensorToFun x * directSumTensorToFun y

theorem directSumTensorToFun.map_one {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₁ : ι₁) → Ring (M₁ i₁)] [(i₂ : ι₂) → Ring (M₂ i₂)] [(i₁ : ι₁) → Algebra R (M₁ i₁)] [(i₂ : ι₂) → Algebra R (M₂ i₂)] : directSumTensorToFun 1 = 1

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)

Equations

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

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

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

theorem Pi.tensor_ext_iff {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 : ι₁) → M₁ i) (z : (i : ι₁) → M₁ i) (y : (i : ι₂) → M₂ i) (w : (i : ι₂) → M₂ i) : x ⊗ₜ[R] y = z ⊗ₜ[R] w ↔ ∀ (i : ι₁) (j : ι₂), x i ⊗ₜ[R] y j = z i ⊗ₜ[R] w j

theorem Pi.tensor_ext {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 : ι₁) → M₁ i} {z : (i : ι₁) → M₁ i} (y : (i : ι₂) → M₂ i) (w : (i : ι₂) → M₂ i) : (∀ (i : ι₁) (j : ι₂), x i ⊗ₜ[R] y j = z i ⊗ₜ[R] w j) → x ⊗ₜ[R] y = z ⊗ₜ[R] w

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

Equations

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

@[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 : ι₂) : (LinearMap.piPiProd R φ ψ S) f j k = f (j, k)

@[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)] (a : (i : ι₁) → (j : ι₂) → φ i →ₗ[R] ψ j) (i : ι₁ × ι₂) : (LinearMap.piPiProd R φ ψ S).symm a i = a i.1 i.2

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

Equations

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

@[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)] (a : (j : ι₂) → (i : ι₁) → φ i →ₗ[R] ψ j) (i : ι₁) (j : ι₂) : (LinearMap.piProdSwap R φ ψ S).symm a i j = a j i

@[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 : ι₁) : (LinearMap.piProdSwap R φ ψ S) f j i = f i j

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

Equations

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

@[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 : ι) : ∀ (a : M), ((LinearMap.rsum R φ S).symm f i) a = f a i

@[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 : ι) : ((LinearMap.rsum R φ S) f) c i = (f i) c

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

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

@[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)] : ∀ (a : (i : ι₁ × ι₂) → φ i.1 →ₗ[R] ψ i.2) (c : (i : ι₁) → φ i) (i : ι₂), ((LinearMap.lrsum R φ ψ S) a) c i = ∑ x : ι₁, (a (x, i)) (c x)

@[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 : ι₁ × ι₂) (a_1 : φ i.1), ((LinearMap.lrsum R φ ψ S).symm a i) a_1 = a (Pi.single i.1 a_1) i.2