English
Two multilinear maps from finitely supported families are equal if they agree on all elementary generators obtained by applying the maps to singletons in each coordinate. This is the DFinsupp analogue of a standard extensionality principle.
Русский
Две мультилейные отображения из семейств с конечной опорой равны, если они совпадают на всех элементарных порождениях, получаемых применением отображений к единичным векторам в каждой координате. Это DFinsupp-аналог ext-взаимности.
LaTeX
$$$\forall p,\ f\circ\mathrm{lsingle}(p) = g\circ\mathrm{lsingle}(p) \Rightarrow f = g,$$$
Lean4
/-- Two multilinear maps from finitely supported functions are equal if they agree on the
generators.
This is a multilinear version of `DFinsupp.lhom_ext'`. -/
@[ext]
theorem dfinsupp_ext [∀ 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 := by
ext x
change f (fun i ↦ x i) = g (fun i ↦ x i)
classical
cases nonempty_fintype ι
rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]
simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]
congr! 1 with p
simp_rw [MultilinearMap.ext_iff] at h
exact h _ _
