monlib / linear_algebra.pi_direct_sum

source

theorem direct_sum.tensor_coe_zero {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] :

⇑0 = 0

source

theorem direct_sum.tensor_coe_add {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (x y : direct_sum (ι₁ × ι₂) (λ (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd))) :

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

source

theorem direct_sum.tensor_coe_smul {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (x : direct_sum (ι₁ × ι₂) (λ (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd))) (r : R) :

⇑(r • x) = r • ⇑x

source

def pi.tensor_of {R : Type u_1} [comm_semiring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (i : ι₁ × ι₂) :

tensor_product R (M₁ i.fst) (M₂ i.snd) →ₗ[R] tensor_product R (Π (j : ι₁), M₁ j) (Π (j : ι₂), M₂ j)

Equations

pi.tensor_of i = tensor_product.map (linear_map.single i.fst) (linear_map.single i.snd)

source

def pi.tensor_proj {R : Type u_1} [comm_semiring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (i : ι₁ × ι₂) :

tensor_product R (Π (j : ι₁), M₁ j) (Π (j : ι₂), M₂ j) →ₗ[R] tensor_product R (M₁ i.fst) (M₂ i.snd)

Equations

pi.tensor_proj i = tensor_product.map (linear_map.proj i.fst) (linear_map.proj i.snd)

source

def direct_sum_tensor_to_fun {R : Type u_1} [comm_semiring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] :

tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i) →ₗ[R] Π (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)

Equations

direct_sum_tensor_to_fun = {to_fun := λ (x : tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i)) (i : ι₁ × ι₂), ⇑(pi.tensor_proj i) x, map_add' := _, map_smul' := _}

source

theorem direct_sum_tensor_to_fun_apply {R : Type u_1} [comm_semiring R] {ι₁ : Type u_2} {ι₂ : Type u_3} {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (x : Π (i : ι₁), M₁ i) (y : Π (i : ι₂), M₂ i) (i : ι₁ × ι₂) :

⇑direct_sum_tensor_to_fun (x ⊗ₜ[R] y) i = x i.fst ⊗ₜ[R] y i.snd

source

def direct_sum_tensor_inv_fun {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [fintype ι₁] [fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] :

(Π (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)) →ₗ[R] tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i)

Equations

direct_sum_tensor_inv_fun = {to_fun := λ (x : Π (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)), finset.univ.sum (λ (i : ι₁ × ι₂), ⇑(pi.tensor_of i) (x i)), map_add' := _, map_smul' := _}

source

theorem function.sum_update_eq_self {ι₁ : Type u_1} [decidable_eq ι₁] [fintype ι₁] {M₁ : ι₁ → Type u_2} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] (x : Π (i : ι₁), M₁ i) :

finset.univ.sum (λ (x_1 : ι₁), function.update 0 x_1 (x x_1)) = x

source

theorem direct_sum_tensor_inv_fun_apply_to_fun {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [fintype ι₁] [fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (x : tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i)) :

⇑direct_sum_tensor_inv_fun (⇑direct_sum_tensor_to_fun x) = x

source

theorem pi.tensor_proj_apply_pi_tensor_of {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (i j : ι₁ × ι₂) (x : Π (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)) :

⇑(pi.tensor_proj i) (⇑(pi.tensor_of j) (x j)) = ite (i = j) (x i) 0

source

theorem direct_sum_tensor_to_fun_apply_inv_fun {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [fintype ι₁] [fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (x : Π (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)) :

⇑direct_sum_tensor_to_fun (⇑direct_sum_tensor_inv_fun x) = x

source

def direct_sum_tensor {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [fintype ι₁] [fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] :

tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i) ≃ₗ[R] Π (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)

Equations

direct_sum_tensor = {to_fun := ⇑direct_sum_tensor_to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑direct_sum_tensor_inv_fun, left_inv := _, right_inv := _}

source

theorem direct_sum_tensor_apply {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [fintype ι₁] [fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (x : Π (i : ι₁), M₁ i) (y : Π (i : ι₂), M₂ i) (i : ι₁ × ι₂) :

⇑direct_sum_tensor (x ⊗ₜ[R] y) i = x i.fst ⊗ₜ[R] y i.snd

source

theorem direct_sum_tensor_to_fun.map_mul {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [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 y : tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i)) :

⇑direct_sum_tensor_to_fun (x * y) = ⇑direct_sum_tensor_to_fun x * ⇑direct_sum_tensor_to_fun y

source

@[instance]

def pi_prod_tensor.algebra {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [comm_ring R] {φ : ι₁ → Type u_4} {ψ : ι₂ → Type u_5} [Π (i : ι₁), ring (φ i)] [Π (i : ι₂), ring (ψ i)] [Π (i : ι₂), algebra R (ψ i)] [Π (i : ι₁), algebra R (φ i)] :

algebra R (Π (i : ι₁ × ι₂), tensor_product R (φ i.fst) (ψ i.snd))

Equations

pi_prod_tensor.algebra = pi.algebra (ι₁ × ι₂) (λ (i : ι₁ × ι₂), tensor_product R (φ i.fst) (ψ i.snd))

source

theorem direct_sum_tensor_to_fun.map_one {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [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₂)] :

⇑direct_sum_tensor_to_fun 1 = 1

source

def direct_sum_tensor_alg_equiv (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [comm_ring R] [fintype ι₁] [fintype ι₂] [decidable_eq ι₁] [decidable_eq ι₂] (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₂)] :

tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i) ≃ₐ[R] Π (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)

Equations

direct_sum_tensor_alg_equiv R M₁ M₂ = {to_fun := λ (x : tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i)) (i : ι₁ × ι₂), ⇑direct_sum_tensor_to_fun x i, inv_fun := λ (x : Π (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)), ⇑direct_sum_tensor_inv_fun x, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem direct_sum_tensor_alg_equiv_symm_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [comm_ring R] [fintype ι₁] [fintype ι₂] [decidable_eq ι₁] [decidable_eq ι₂] (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 : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)) :

⇑((direct_sum_tensor_alg_equiv R M₁ M₂).symm) x = ⇑direct_sum_tensor_inv_fun x

source

@[simp]

theorem direct_sum_tensor_alg_equiv_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [comm_ring R] [fintype ι₁] [fintype ι₂] [decidable_eq ι₁] [decidable_eq ι₂] (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 : tensor_product R (Π (i : ι₁), M₁ i) (Π (i : ι₂), M₂ i)) (i : ι₁ × ι₂) :

⇑(direct_sum_tensor_alg_equiv R M₁ M₂) x i = ⇑direct_sum_tensor_to_fun x i

source

theorem pi.tensor_ext_iff {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [fintype ι₁] [fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (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

@[ext]

theorem pi.tensor_ext {R : Type u_1} [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [fintype ι₁] [fintype ι₂] {M₁ : ι₁ → Type u_4} {M₂ : ι₂ → Type u_5} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (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

@[simp]

theorem linear_map.pi_pi_prod_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] (ᾰ : Π (i : ι₁ × ι₂), φ i.fst →ₗ[R] ψ i.snd) (i : ι₁) (j : ι₂) :

⇑(linear_map.pi_pi_prod R φ ψ S) ᾰ i j = ᾰ (i, j)

source

def linear_map.pi_pi_prod (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] :

(Π (i : ι₁ × ι₂), φ i.fst →ₗ[R] ψ i.snd) ≃ₗ[S] Π (i : ι₁) (j : ι₂), φ i →ₗ[R] ψ j

Equations

linear_map.pi_pi_prod R φ ψ S = linear_equiv.of_linear {to_fun := λ (f : Π (i : ι₁ × ι₂), φ i.fst →ₗ[R] ψ i.snd) (j : ι₁) (k : ι₂), f (j, k), map_add' := _, map_smul' := _} {to_fun := λ (f : Π (i : ι₁) (j : ι₂), φ i →ₗ[R] ψ j) (i : ι₁ × ι₂), f i.fst i.snd, map_add' := _, map_smul' := _} _ _

source

@[simp]

theorem linear_map.pi_pi_prod_symm_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] (ᾰ : Π (i : ι₁) (j : ι₂), φ i →ₗ[R] ψ j) (i : ι₁ × ι₂) :

⇑((linear_map.pi_pi_prod R φ ψ S).symm) ᾰ i = ᾰ i.fst i.snd

source

@[simp]

theorem linear_map.pi_prod_swap_symm_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] (ᾰ : Π (j : ι₂) (i : ι₁), φ i →ₗ[R] ψ j) (i : ι₁) (j : ι₂) :

⇑((linear_map.pi_prod_swap R φ ψ S).symm) ᾰ i j = ᾰ j i

source

def linear_map.pi_prod_swap (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] :

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

Equations

linear_map.pi_prod_swap R φ ψ S = linear_equiv.of_linear {to_fun := λ (f : Π (i : ι₁) (j : ι₂), φ i →ₗ[R] ψ j) (j : ι₂) (i : ι₁), f i j, map_add' := _, map_smul' := _} {to_fun := λ (f : Π (j : ι₂) (i : ι₁), φ i →ₗ[R] ψ j) (i : ι₁) (j : ι₂), f j i, map_add' := _, map_smul' := _} _ _

source

@[simp]

theorem linear_map.pi_prod_swap_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] (ᾰ : Π (i : ι₁) (j : ι₂), φ i →ₗ[R] ψ j) (j : ι₂) (i : ι₁) :

⇑(linear_map.pi_prod_swap R φ ψ S) ᾰ j i = ᾰ i j

source

@[simp]

theorem linear_map.rsum_apply (R : Type u_1) {M : Type u_2} {ι : Type u_3} [semiring R] (φ : ι → Type u_4) [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (S : Type u_5) [add_comm_monoid M] [module R M] [semiring S] [Π (i : ι), module S (φ i)] [∀ (i : ι), smul_comm_class R S (φ i)] (f : Π (i : ι), M →ₗ[R] φ i) :

⇑(linear_map.rsum R φ S) f = linear_map.pi f

source

def linear_map.rsum (R : Type u_1) {M : Type u_2} {ι : Type u_3} [semiring R] (φ : ι → Type u_4) [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (S : Type u_5) [add_comm_monoid M] [module R M] [semiring S] [Π (i : ι), module S (φ i)] [∀ (i : ι), smul_comm_class R S (φ i)] :

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

Equations

linear_map.rsum R φ S = {to_fun := λ (f : Π (i : ι), M →ₗ[R] φ i), linear_map.pi f, map_add' := _, map_smul' := _, inv_fun := λ (f : M →ₗ[R] Π (i : ι), φ i) (i : ι), (linear_map.proj i).comp f, left_inv := _, right_inv := _}

source

@[simp]

theorem linear_map.rsum_symm_apply (R : Type u_1) {M : Type u_2} {ι : Type u_3} [semiring R] (φ : ι → Type u_4) [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (S : Type u_5) [add_comm_monoid M] [module R M] [semiring S] [Π (i : ι), module S (φ i)] [∀ (i : ι), smul_comm_class R S (φ i)] (f : M →ₗ[R] Π (i : ι), φ i) (i : ι) :

⇑((linear_map.rsum R φ S).symm) f i = (linear_map.proj i).comp f

source

def linear_map.lrsum (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [fintype ι₁] [decidable_eq ι₁] [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] :

(Π (i : ι₁ × ι₂), φ i.fst →ₗ[R] ψ i.snd) ≃ₗ[S] (Π (i : ι₁), φ i) →ₗ[R] Π (i : ι₂), ψ i

Equations

linear_map.lrsum R φ ψ S = let h₂ : (Π (j : ι₂) (i : ι₁), φ i →ₗ[R] ψ j) ≃ₗ[S] Π (j : ι₂), (Π (i : ι₁), φ i) →ₗ[R] ψ j := linear_equiv.Pi_congr_right (λ (j : ι₂), linear_map.lsum R φ S) in (((linear_map.pi_pi_prod R φ ψ S).trans (linear_map.pi_prod_swap R φ ψ S)).trans h₂).trans (linear_map.rsum R ψ S)

source

@[simp]

theorem linear_map.lrsum_apply_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [fintype ι₁] [decidable_eq ι₁] [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] (ᾰ : Π (i : ι₁ × ι₂), φ i.fst →ₗ[R] ψ i.snd) (c : Π (i : ι₁), φ i) (i : ι₂) :

⇑(⇑(linear_map.lrsum R φ ψ S) ᾰ) c i = finset.univ.sum (λ (x : ι₁), ⇑(ᾰ (x, i)) (c x))

source

@[simp]

theorem linear_map.lrsum_symm_apply_apply (R : Type u_1) {ι₁ : Type u_2} {ι₂ : Type u_3} [semiring R] (φ : ι₁ → Type u_4) (ψ : ι₂ → Type u_5) [Π (i : ι₁), add_comm_monoid (φ i)] [Π (i : ι₁), module R (φ i)] [Π (i : ι₂), add_comm_monoid (ψ i)] [Π (i : ι₂), module R (ψ i)] (S : Type u_6) [fintype ι₁] [decidable_eq ι₁] [semiring S] [Π (i : ι₂), module S (ψ i)] [∀ (i : ι₂), smul_comm_class R S (ψ i)] (ᾰ : (Π (i : ι₁), φ i) →ₗ[R] Π (i : ι₂), ψ i) (i : ι₁ × ι₂) (ᾰ_1 : φ i.fst) :

⇑(⇑((linear_map.lrsum R φ ψ S).symm) ᾰ i) ᾰ_1 = ⇑ᾰ (pi.single i.fst ᾰ_1) i.snd