Multilinear maps from direct sums

This file describes multilinear maps on direct sums.

Main results

• MultilinearMap.fromDirectSumEquiv : If ι is a Fintype, κ i is a family of types indexed by ι and we are given an R-module M i j for every i : ι and j : κ i, this is the linear equivalence between Π p : (i : ι) → κ i, MultilinearMap R (fun i ↦ M i (p i)) M' and MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M'.

theorem MultilinearMap.directSum_ext {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [AddCommMonoid M'] [Module R M'] [Finite ι] [(i : ι) → DecidableEq (κ i)] ⦃f g : MultilinearMap R (fun (i : ι) => DirectSum (κ i) fun (j : κ i) => M i j) M'⦄ (h : ∀ (p : (i : ι) → κ i), (f.compLinearMap fun (i : ι) => DirectSum.lof R (κ i) (M i) (p i)) = g.compLinearMap fun (i : ι) => DirectSum.lof R (κ i) (M i) (p i)) : f = g

Two multilinear maps from direct sums are equal if they agree on the generators.

theorem MultilinearMap.directSum_ext_iff {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [AddCommMonoid M'] [Module R M'] [Finite ι] [(i : ι) → DecidableEq (κ i)] {f g : MultilinearMap R (fun (i : ι) => DirectSum (κ i) fun (j : κ i) => M i j) M'} : f = g ↔ ∀ (p : (i : ι) → κ i), (f.compLinearMap fun (i : ι) => DirectSum.lof R (κ i) (M i) (p i)) = g.compLinearMap fun (i : ι) => DirectSum.lof R (κ i) (M i) (p i)

noncomputable def MultilinearMap.fromDirectSumEquiv {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [AddCommMonoid M'] [Module R M'] [DecidableEq ι] [Finite ι] : ((p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) M') ≃ₗ[R] MultilinearMap R (fun (i : ι) => DirectSum (κ i) fun (j : κ i) => M i j) M'

The linear equivalence between families indexed by p : Π i : ι, κ i of multilinear maps on the fun i ↦ M i (p i) and the space of multilinear map on fun i ↦ ⨁ j : κ i, M i j.

Equations

• MultilinearMap.fromDirectSumEquiv = MultilinearMap.fromDFinsuppEquiv κ R

@[simp]

theorem MultilinearMap.fromDirectSumEquiv_lof {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [AddCommMonoid M'] [Module R M'] [DecidableEq ι] [Finite ι] [(i : ι) → DecidableEq (κ i)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) M') (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)) : ((fromDirectSumEquiv f) fun (i : ι) => (DirectSum.lof R (κ i) (M i) (p i)) (x i)) = (f p) x

theorem MultilinearMap.fromDirectSumEquiv_apply {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [AddCommMonoid M'] [Module R M'] [DecidableEq ι] [Fintype ι] [(i : ι) → DecidableEq (κ i)] [(i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) M') (x : DirectSum ι fun (i : ι) => DirectSum (κ i) fun (j : κ i) => M i j) : (fromDirectSumEquiv f) ⇑x = ∑ p ∈ Fintype.piFinset fun (i : ι) => DFinsupp.support (x i), (f p) fun (i : ι) => (x i) (p i)

Prefer using fromDirectSumEquiv_lof where possible.

@[simp]

theorem MultilinearMap.fromDirectSumEquiv_symm_apply {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [AddCommMonoid M'] [Module R M'] [DecidableEq ι] [Finite ι] [(i : ι) → DecidableEq (κ i)] (f : MultilinearMap R (fun (i : ι) => DirectSum (κ i) fun (j : κ i) => M i j) M') (p : (i : ι) → κ i) : fromDirectSumEquiv.symm f p = f.compLinearMap fun (i : ι) => DirectSum.lof R (κ i) (M i) (p i)