Interactions between finitely-supported functions and multilinear maps

Main definitions

• freeFinsuppEquiv is an equivalence of multilinear maps over free modules with finitely supported maps.

noncomputable def MultilinearMap.freeFinsuppEquiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {κ : ι → Type u_4} [DecidableEq ι] [Fintype ι] [CommSemiring R] [DecidableEq R] [DecidableEq ι'] [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] : (((i : ι) → κ i) × ι' →₀ R) ≃ₗ[R] MultilinearMap R (fun (i : ι) => κ i →₀ R) (ι' →₀ R)

The linear equivalence of multilinear maps on free modules over R indexed by fun i => κ i on the domain and ι' on the codomain and the finitely supported maps from (Π i, κ i) × ι' into R.

This is the Finsupp version of MultilinearMap.freeDFinsuppEquiv.

theorem MultilinearMap.freeFinsuppEquiv_def {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {κ : ι → Type u_4} [DecidableEq ι] [Fintype ι] [CommSemiring R] [DecidableEq R] [DecidableEq ι'] [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] (f : ((i : ι) → κ i) × ι' →₀ R) : freeFinsuppEquiv f = (LinearEquiv.multilinearMapCongrLeft fun (x : ι) => finsuppLequivDFinsupp R) ((LinearEquiv.multilinearMapCongrRight R (finsuppLequivDFinsupp R)).symm (freeDFinsuppEquiv ((finsuppLequivDFinsupp R) f)))

@[simp]

theorem MultilinearMap.freeFinsuppEquiv_single {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {κ : ι → Type u_4} [DecidableEq ι] [Fintype ι] [CommSemiring R] [DecidableEq R] [DecidableEq ι'] [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] (p : ((i : ι) → κ i) × ι') (r : R) (x : (i : ι) → κ i →₀ R) : (freeFinsuppEquiv fun₀ | p => r) x = r • fun₀ | p.2 => ∏ i : ι, (x i) (p.1 i)

When freeFinsuppEquiv is applied to a map with a single value the resulting multilinear map sends inputs to a single value in the codomain, taking a product over images from each component of the domain.

theorem MultilinearMap.freeFinsuppEquiv_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {κ : ι → Type u_4} [DecidableEq ι] [Fintype ι] [CommSemiring R] [DecidableEq R] [DecidableEq ι'] [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] [Fintype ι'] (f : ((i : ι) → κ i) × ι' →₀ R) (x : (i : ι) → κ i →₀ R) : (freeFinsuppEquiv f) x = ∑ p : ((i : ι) → κ i) × ι', f p • fun₀ | p.2 => ∏ i : ι, (x i) (p.1 i)