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.

theorem MultilinearMap.dfinsupp_ext {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [DecidableEq ι] [Fintype ι] [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'.

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.

Equations

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

@[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) : ((MultilinearMap.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) : ((MultilinearMap.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) : ((MultilinearMap.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)) : ((MultilinearMap.dfinsuppFamily f) fun (i : ι) => DFinsupp.single (p i) (m i)) = DFinsupp.single 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) : (MultilinearMap.dfinsuppFamily (Pi.single p f)) x = DFinsupp.single 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)) : MultilinearMap.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) : ((MultilinearMap.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)] : MultilinearMap.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)) : MultilinearMap.dfinsuppFamily (f + g) = MultilinearMap.dfinsuppFamily f + MultilinearMap.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)) : MultilinearMap.dfinsuppFamily (s • f) = s • MultilinearMap.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.

Equations

• MultilinearMap.dfinsuppFamilyₗ = { toFun := MultilinearMap.dfinsuppFamily, map_add' := ⋯, map_smul' := ⋯ }

@[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)) : MultilinearMap.dfinsuppFamilyₗ f = MultilinearMap.dfinsuppFamily f