English
Given a family of indices κ and a family of multilinear maps f p for each choice p of indices, dfinsuppFamily translates a family of finitely-supported tuples into a finitely-supported object by evaluating each f p on the corresponding coordinates extracted from the input. This construction is the DFinsupp version of piFamily.
Русский
Для заданного семейства индексов κ и семейства мультилейных отображений f p для каждого выбора p, dfinsuppFamily переводит семействo кортежей с конечной поддержкой в конечное поддерживаемое изделие, вычисляя f p на соответствующих координатах из входа. Это DFinsupp-версия piFamily.
LaTeX
$$$(\dfinsuppFamily f)(x)(p) = f(p)(\lambda i \mapsto x(i)(p(i))).$$$
Lean4
/-- 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`.
-/
@[simps]
def dfinsuppFamily (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)
where
toFun
x :=
{ toFun := fun p => f p (fun i => x i (p i))
support' :=
(Trunc.finChoice fun i => (x i).support').map fun s =>
⟨Finset.univ.val.pi (fun i ↦ (s i).val) |>.map fun f i => f i (Finset.mem_univ _), fun p =>
by
simp only [Multiset.mem_map, Multiset.mem_pi, Finset.mem_val, Finset.mem_univ, forall_true_left]
simp_rw [or_iff_not_imp_right]
intro h
push_neg at h
refine ⟨fun i _ => p i, fun i => (s i).prop _ |>.resolve_right ?_, rfl⟩
exact mt ((f p).map_coord_zero (m := fun i => x i _) i) h⟩ }
map_update_add' {dec} m i x
y :=
DFinsupp.ext fun p => by
dsimp
simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.add_apply, (f p).map_update_add]
map_update_smul' {dec} m i c
x :=
DFinsupp.ext fun p => by
dsimp
simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.smul_apply, (f p).map_update_smul]
