English
Let hk and hl encode the sizes of a finite subset s of Fin n and its complement, and let f be a multilinear map with two blocks of arguments corresponding to Fin k and Fin l. Then applying the inverse curry map to f on two constant inputs x yields the same result as applying f to the two constant inputs x and x in the corresponding blocks. In other words, the currying/un-currying identified mapping respects constant directions.
Русский
Пусть hk и hl кодируют размеры конечного подмножества s ⊆ Fin n и его дополнения. Тогда для двух-блоковой многолинейной карты f и константного элемента x, применение обратного карриования к f на двух константных входах x дает тот же результат, что и применение f к константным входам x в соответствующих блоках.
LaTeX
$$$\left(\mathrm{curryFinFinset} \; R \; M_2 \; M' \ hk \ hl\right)^{-1} f \, (\lambda _{\_} . x) = f\, (\lambda _{\_} . x)\, (\lambda _{\_} . x),$$$
Lean4
@[simp]
theorem curryFinFinset_symm_apply_const {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
(f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂)) (x : M') :
((curryFinFinset R M₂ M' hk hl).symm f fun _ => x) = f (fun _ => x) fun _ => x :=
rfl
