Interactions between (dependent) functions and multilinear maps

Main definitions

• MultilinearMap.pi_ext, a multilinear version of LinearMap.pi_ext

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

  This is useful because all the intermediate results are bundled:

  • MultilinearMap.piFamily f is a MultilinearMap operating on functions x.
  • MultilinearMap.piFamilyₗ is a LinearMap, linear in the family of multilinear maps f.

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

Two multilinear maps from finite families are equal if they agree on the generators.

This is a multilinear version of LinearMap.pi_ext.

def MultilinearMap.piFamily {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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, piFamily f maps a family of functions (one for each domain κ i) into a function from each selection of indices (with domain Π i, κ i).

Equations

• MultilinearMap.piFamily f = { toFun := fun (x : (i : ι) → (j : κ i) → M i j) (p : (i : ι) → κ i) => (f p) fun (i : ι) => x i (p i), map_update_add' := ⋯, map_update_smul' := ⋯ }

@[simp]

theorem MultilinearMap.piFamily_apply {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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.piFamily f) x p = (f p) fun (i : ι) => x i (p i)

@[simp]

theorem MultilinearMap.piFamily_single {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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)] [Fintype ι] [(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.piFamily f) fun (i : ι) => Pi.single (p i) (m i)) = Pi.single p ((f p) m)

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

@[simp]

theorem MultilinearMap.piFamily_single_left_apply {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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)] [Fintype ι] [(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.piFamily (Pi.single p f)) x = Pi.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.piFamily_single_left {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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)] [Fintype ι] [(i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (f : MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) : MultilinearMap.piFamily (Pi.single p f) = (LinearMap.single R N p).compMultilinearMap (f.compLinearMap fun (i : ι) => LinearMap.proj (p i))

@[simp]

theorem MultilinearMap.piFamily_compLinearMap_lsingle {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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)] [Fintype ι] [(i : ι) → DecidableEq (κ i)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) (p : (i : ι) → κ i) : ((MultilinearMap.piFamily f).compLinearMap fun (i : ι) => LinearMap.single R (M i) (p i)) = (LinearMap.single R N p).compMultilinearMap (f p)

@[simp]

theorem MultilinearMap.piFamily_zero {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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.piFamily 0 = 0

@[simp]

theorem MultilinearMap.piFamily_add {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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.piFamily (f + g) = MultilinearMap.piFamily f + MultilinearMap.piFamily g

@[simp]

theorem MultilinearMap.piFamily_smul {ι : Type uι} {κ : ι → Type uκ} {S : Type uS} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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.piFamily (s • f) = s • MultilinearMap.piFamily f

def MultilinearMap.piFamilyₗ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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.piFamily as a linear map.

Equations

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

@[simp]

theorem MultilinearMap.piFamilyₗ_apply {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN} [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.piFamilyₗ f = MultilinearMap.piFamily f