Documentation

Mathlib.LinearAlgebra.Multilinear.DFinsupp

Interactions between finitely-supported functions and multilinear maps #

Main definitions #

theorem MultilinearMap.dfinsupp_ext_iff {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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 : MultilinearMap R (fun (i : ι) => Π₀ (j : κ i), M i j) N} {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)
theorem MultilinearMap.dfinsupp_ext {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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 : MultilinearMap R (fun (i : ι) => Π₀ (j : κ i), M i j) N ⦃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'.

@[simp]
theorem MultilinearMap.dfinsuppFamily_apply_toFun {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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} {R : Type uR} {M : (i : ι) → κ iType 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')
def MultilinearMap.dfinsuppFamily {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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.
Instances For
    theorem MultilinearMap.support_dfinsuppFamily_subset {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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} {R : Type uR} {M : (i : ι) → κ iType 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_compLinearMap_lsingle {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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} {R : Type uR} {M : (i : ι) → κ iType 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)] :
    @[simp]
    theorem MultilinearMap.dfinsuppFamily_add {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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)) (g : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) => M i (p i)) (N p)) :
    @[simp]
    theorem MultilinearMap.dfinsuppFamily_smul {ι : Type uι} {κ : ιType} {S : Type uS} {R : Type uR} {M : (i : ι) → κ iType 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)) :
    @[simp]
    theorem MultilinearMap.dfinsuppFamilyₗ_apply {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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
    def MultilinearMap.dfinsuppFamilyₗ {ι : Type uι} {κ : ιType} {R : Type uR} {M : (i : ι) → κ iType 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' := }
    Instances For