Theorems · Definition · linear algebra

MultilinearMap.dfinsuppFamily

{ι : Type uι} →
  {κ : ι → Type uκ} →
    {R : Type uR} →
      {M : (i : ι) → κ i → Type uM} →
        {N : ((i : ι) → κ i) → Type uN} →
          [DecidableEq ι] →
            [Fintype ι] →
              [inst : Semiring R] →
                [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] →
                  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] →
                    [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] →
                      [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] →
                        ((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.

Defined in

Mathlib.LinearAlgebra.Multilinear.DFinsupp

Cited by

13 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeSemiringAddCommMonoidAddCommMonoidModuleModule