English
Replacing each argument by a linear equivalence yields zero if and only if the original multilinear map is zero.
Русский
Замена каждого аргумента линейным эквивалентом даёт нуль тогда и только тогда, когда исходная мультиленейная карта равна нулю.
LaTeX
$$$ (g.compLinearMap (\\lambda i, (f i) : M_i →ₗ[R] M_i')) = 0 \\\\iff g = 0 $$$
Lean4
/-- If one adds to a vector `m'` another vector `m`, but only for coordinates in a finset `t`, then
the image under a multilinear map `f` is the sum of `f (s.piecewise m m')` along all subsets `s` of
`t`. This is mainly an auxiliary statement to prove the result when `t = univ`, given in
`map_add_univ`, although it can be useful in its own right as it does not require the index set `ι`
to be finite. -/
theorem map_piecewise_add [DecidableEq ι] (m m' : ∀ i, M₁ i) (t : Finset ι) :
f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m') :=
by
revert m'
refine Finset.induction_on t (by simp) ?_
intro i t hit Hrec m'
have A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i) :=
t.piecewise_insert _ _ _
have B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m' :=
by
ext j
by_cases h : j = i
· rw [h]
simp [hit]
· simp [h]
let m'' := update m' i (m i)
have C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m'' :=
by
ext j
by_cases h : j = i
· rw [h]
simp [m'', hit]
· by_cases h' : j ∈ t <;> simp [m'', h, h']
rw [A, f.map_update_add, B, C, Finset.sum_powerset_insert hit, Hrec, Hrec, add_comm (_ : M₂)]
congr 1
refine Finset.sum_congr rfl fun s hs => ?_
have : (insert i s).piecewise m m' = s.piecewise m m'' :=
by
ext j
by_cases h : j = i
· rw [h]
simp [m'', Finset.notMem_of_mem_powerset_of_notMem hs hit]
· by_cases h' : j ∈ s <;> simp [m'', h, h']
rw [this]
