Interactions between finitely-supported functions and multilinear maps

Main definitions

• MultilinearMap.dfinsupp_ext

• MultilinearMap.dfinsuppFamily, which satisfies dfinsuppFamily f x p = f p (fun i => x i (p i)).

  This is the finitely-supported version of MultilinearMap.piFamily.

  This is useful because all the intermediate results are bundled:

  • MultilinearMap.dfinsuppFamily f x is a DFinsupp supported by families of indices p.
  • MultilinearMap.dfinsuppFamily f is a MultilinearMap operating on finitely-supported functions x.
  • MultilinearMap.dfinsuppFamilyₗ is a LinearMap, linear in the family of multilinear maps f.

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

theorem MultilinearMap.dfinsupp_ext {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [Finite ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [AddCommMonoid N] [(i : ι) → (k : κ i) → Module R (M i k)] [Module R N] [(i : ι) → DecidableEq (κ i)] ⦃f g : MultilinearMap R (fun (i : ι) => Π₀ (j : κ i), M i j) N⦄ (h : ∀ (p : (i : ι) → κ i), (f.compLinearMap fun (i : ι) => DFinsupp.lsingle (p i)) = g.compLinearMap fun (i : ι) => DFinsupp.lsingle (p i)) : f = g

Two multilinear maps from finitely supported functions are equal if they agree on the generators.

This is a multilinear version of DFinsupp.lhom_ext'.

theorem MultilinearMap.dfinsupp_ext_iff {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [Finite ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [AddCommMonoid N] [(i : ι) → (k : κ i) → Module R (M i k)] [Module R N] [(i : ι) → DecidableEq (κ i)] {f g : MultilinearMap R (fun (i : ι) => Π₀ (j : κ i), M i j) N} : f = g ↔ ∀ (p : (i : ι) → κ i), (f.compLinearMap fun (i : ι) => DFinsupp.lsingle (p i)) = g.compLinearMap fun (i : ι) => DFinsupp.lsingle (p i)

def MultilinearMap.dfinsuppFamily {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) : MultilinearMap R (fun (i : ι) => Π₀ (j : κ i), M i j) (Π₀ (t : (i : ι) → κ i), N t)

Given a family of indices κ and a multilinear map f p for each way p to select one index from each family, dfinsuppFamily f maps a family of finitely-supported functions (one for each domain κ i) into a finitely-supported function from each selection of indices (with domain Π i, κ i).

Strictly this doesn't need multilinearity, only the fact that f p m = 0 whenever m i = 0 for some i.

This is the DFinsupp version of MultilinearMap.piFamily.

@[simp]

theorem MultilinearMap.dfinsuppFamily_apply_toFun {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) (x : (i : ι) → Π₀ (j : κ i), M i j) (p : (i : ι) → κ i) : ((dfinsuppFamily f) x) p = (f p) fun (i : ι) => (x i) (p i)

@[simp]

theorem MultilinearMap.dfinsuppFamily_apply_support' {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) (x : (i : ι) → Π₀ (j : κ i), M i j) : ((dfinsuppFamily f) x).support' = Trunc.map (fun (s : (i : ι) → { s : Multiset (κ i) // ∀ (i_1 : κ i), i_1 ∈ s ∨ (x i).toFun i_1 = 0 }) => ⟨Multiset.map (fun (f : (a : ι) → a ∈ Finset.univ.val → κ a) (i : ι) => f i ⋯) (Finset.univ.val.pi fun (i : ι) => ↑(s i)), ⋯⟩) (Trunc.finChoice fun (i : ι) => (x i).support')

theorem MultilinearMap.support_dfinsuppFamily_subset {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] [(i : ι) → DecidableEq (κ i)] [(i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)] [(i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) (x : (i : ι) → Π₀ (j : κ i), M i j) : ((dfinsuppFamily f) x).support ⊆ Fintype.piFinset fun (i : ι) => (x i).support

@[simp]

theorem MultilinearMap.dfinsuppFamily_single {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] [(i : ι) → DecidableEq (κ i)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) (p : (i : ι) → κ i) (m : (i : ι) → M i (p i)) : ((dfinsuppFamily f) fun (i : ι) => fun₀ | p i => m i) = fun₀ | p => (f p) m

When applied to a family of finitely-supported functions each supported on a single element, dfinsuppFamily is itself supported on a single element, with value equal to the map f applied at that point.

@[simp]

theorem MultilinearMap.dfinsuppFamily_single_left_apply {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] [(i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (f : MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) (x : (i : ι) → Π₀ (j : κ i), M i j) : (dfinsuppFamily (Pi.single p f)) x = fun₀ | p => f fun (i : ι) => (x i) (p i)

When only one member of the family of multilinear maps is nonzero, the result consists only of the component from that member.

theorem MultilinearMap.dfinsuppFamily_single_left {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] [(i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (f : MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) : dfinsuppFamily (Pi.single p f) = (DFinsupp.lsingle p).compMultilinearMap (f.compLinearMap fun (i : ι) => DFinsupp.lapply (p i))

@[simp]

theorem MultilinearMap.dfinsuppFamily_compLinearMap_lsingle {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] [(i : ι) → DecidableEq (κ i)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) (p : (i : ι) → κ i) : ((dfinsuppFamily f).compLinearMap fun (i : ι) => DFinsupp.lsingle (p i)) = (DFinsupp.lsingle p).compMultilinearMap (f p)

@[simp]

theorem MultilinearMap.dfinsuppFamily_zero {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] : dfinsuppFamily 0 = 0

@[simp]

theorem MultilinearMap.dfinsuppFamily_add {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] (f g : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) : dfinsuppFamily (f + g) = dfinsuppFamily f + dfinsuppFamily g

@[simp]

theorem MultilinearMap.dfinsuppFamily_smul {ι : Type uι} {κ : ι → Type uκ} {S : Type uS} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [Semiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] [Monoid S] [(p : (i : ι) → κ i) → DistribMulAction S (N p)] [∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)] (s : S) (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) : dfinsuppFamily (s • f) = s • dfinsuppFamily f

def MultilinearMap.dfinsuppFamilyₗ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] : ((p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) →ₗ[R] MultilinearMap R (fun (i : ι) => Π₀ (j : κ i), M i j) (Π₀ (t : (i : ι) → κ i), N t)

MultilinearMap.dfinsuppFamily as a linear map.

@[simp]

theorem MultilinearMap.dfinsuppFamilyₗ_apply {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(p : (i : ι) → κ i) → AddCommMonoid (N p)] [(i : ι) → (k : κ i) → Module R (M i k)] [(p : (i : ι) → κ i) → Module R (N p)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) : dfinsuppFamilyₗ f = dfinsuppFamily f

def MultilinearMap.fromDFinsuppEquiv {ι : Type uι} (κ : ι → Type uκ) (R : Type uR) {M : (i : ι) → κ i → Type uM} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(i : ι) → (k : κ i) → Module R (M i k)] {N : Type u_1} [AddCommMonoid N] [Module R N] [(i : ι) → DecidableEq (κ i)] : ((p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) N) ≃ₗ[R] MultilinearMap R (fun (i : ι) => Π₀ (j : κ i), M i j) N

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.

@[simp]

theorem MultilinearMap.fromDFinsuppEquiv_single {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(i : ι) → (k : κ i) → Module R (M i k)] {N : Type u_1} [AddCommMonoid N] [Module R N] [(i : ι) → DecidableEq (κ i)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) N) (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)) : (((fromDFinsuppEquiv κ R) f) fun (i : ι) => fun₀ | p i => x i) = (f p) x

theorem MultilinearMap.fromDFinsuppEquiv_apply {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(i : ι) → (k : κ i) → Module R (M i k)] {N : Type u_1} [AddCommMonoid N] [Module R N] [(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)) N) (x : (i : ι) → Π₀ (j : κ i), M i j) : ((fromDFinsuppEquiv κ R) f) x = ∑ p ∈ Fintype.piFinset fun (i : ι) => (x i).support, (f p) fun (i : ι) => (x i) (p i)

@[simp]

theorem MultilinearMap.fromDFinsuppEquiv_symm_apply {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → (k : κ i) → AddCommMonoid (M i k)] [(i : ι) → (k : κ i) → Module R (M i k)] {N : Type u_1} [AddCommMonoid N] [Module R N] [(i : ι) → DecidableEq (κ i)] (f : MultilinearMap R (fun (i : ι) => Π₀ (j : κ i), M i j) N) (p : (i : ι) → κ i) : (fromDFinsuppEquiv κ R).symm f p = f.compLinearMap fun (i : ι) => DFinsupp.lsingle (p i)

def MultilinearMap.freeDFinsuppEquiv {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {ι' : Type u_1} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] : (Π₀ (x : ((i : ι) → κ i) × ι'), R) ≃ₗ[R] MultilinearMap R (fun (i : ι) => Π₀ (x : κ i), R) (Π₀ (x : ι'), 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 dependent, finitely supported maps from (Π i, κ i) × ι' into R.

theorem MultilinearMap.freeDFinsuppEquiv_def {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {ι' : Type u_1} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] (f : Π₀ (x : ((i : ι) → κ i) × ι'), R) : freeDFinsuppEquiv f = (fromDFinsuppEquiv κ R) ((LinearEquiv.piCongrRight fun (x : (i : ι) → κ i) => MultilinearMap.piRingEquiv) (DFinsupp.linearEquivFunOnFintype (DFinsupp.sigmaCurryLEquiv ((DFinsupp.domLCongr (Equiv.sigmaEquivProd ((i : ι) → κ i) ι').symm) f))))

@[simp]

theorem MultilinearMap.freeDFinsuppEquiv_single {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {ι' : Type u_1} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] [DecidableEq ι'] (p : ((i : ι) → κ i) × ι') (r : R) (x : (i : ι) → Π₀ (x : κ i), R) : (freeDFinsuppEquiv fun₀ | p => r) x = r • fun₀ | p.2 => ∏ i : ι, (x i) (p.1 i)

When freeDFinsuppEquiv is applied to a map with a single value of one 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.freeDFinsuppEquiv_apply {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {ι' : Type u_1} [DecidableEq ι] [Fintype ι] [CommSemiring R] [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] [DecidableEq ι'] [Fintype ι'] (f : Π₀ (x : ((i : ι) → κ i) × ι'), R) (x : (i : ι) → Π₀ (x : κ i), R) : (freeDFinsuppEquiv f) x = ∑ p : ((i : ι) → κ i) × ι', f p • fun₀ | p.2 => ∏ i : ι, (x i) (p.1 i)