English
For any f : (Σ i, η i) →₀ N, applying the sigmaFinsuppEquivDFinsupp yields the same object as splitting f.
Русский
Для любого f: (Σ i, η i) →₀ N применение sigmaFinsuppEquivDFinsupp эквивалентно разбиению f на составляющие (split).
LaTeX
$$$\\bigl(\\sigmaFinsuppEquivDFinsupp f\\bigr) = Finsupp.split f$$$
Lean4
/-- `Finsupp.split` is an equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
def sigmaFinsuppEquivDFinsupp [Zero N] : ((Σ i, η i) →₀ N) ≃ Π₀ i, η i →₀ N
where
toFun
f :=
⟨split f,
Trunc.mk
⟨(splitSupport f : Finset ι).val, fun i =>
by
rw [← Finset.mem_def, mem_splitSupport_iff_nonzero]
exact (em _).symm⟩⟩
invFun
f := by
haveI := Classical.decEq ι
haveI := fun i => Classical.decEq (η i →₀ N)
refine
onFinset (Finset.sigma f.support fun j => (f j).support) (fun ji => f ji.1 ji.2) fun g hg =>
Finset.mem_sigma.mpr ⟨?_, mem_support_iff.mpr hg⟩
simp only [Ne, DFinsupp.mem_support_toFun]
intro h
dsimp at hg
rw [h] at hg
simp only [coe_zero, Pi.zero_apply, not_true] at hg
left_inv f := by ext; simp [split]
right_inv f := by ext; simp [split]
