English
Given a multilinear map f on n variables and a finite set s of indices, there is a restricted multilinear map on |s| variables obtained by fixing the remaining variables to a fixed value z; the restricted map is multilinear in the remaining coordinates.
Русский
Дано мультилейное отображение f на n переменных и конечное множество индексов s; существует ограниченное мультилейное отображение на |s| переменных, получаемое фиксацией остальных координат к значению z; ограниченное отображение сохраняет линейность в оставшихся координатах.
LaTeX
$$$\text{restr}(f,s,hk,z): MultilinearMap R (\fun x => M') M_2$ с описанием фиксации координат$$
Lean4
/-- Given a multilinear map `f` on `n` variables (parameterized by `Fin n`) and a subset `s` of `k`
of these variables, one gets a new multilinear map on `Fin k` by varying these variables, and fixing
the other ones equal to a given value `z`. It is denoted by `f.restr s hk z`, where `hk` is a
proof that the cardinality of `s` is `k`. The implicit identification between `Fin k` and `s` that
we use is the canonical (increasing) bijection. -/
def restr {k n : ℕ} (f : MultilinearMap R (fun _ : Fin n => M') M₂) (s : Finset (Fin n)) (hk : #s = k) (z : M') :
MultilinearMap R (fun _ : Fin k => M') M₂
where
toFun v := f fun j => if h : j ∈ s then v ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z
map_update_add' v i x
y :=
by
erw [dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv, dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv,
dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv]
simp
map_update_smul' v i c
x :=
by
erw [dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv, dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv]
simp
