English
The pi construction combines a family of alternating maps into an alternating map valued in a function space; the value at input a is the function i ↦ f_i(a).
Русский
П-конструирование объединяет семейство чередующихся отображений в чередующее отображение со значениями в пространство функций; значение на входе a равно функциямi ↦ f_i(a).
LaTeX
$$$ \text{pi} : (\forall i,\operatorname{AlternatingMap}(R,M,N_i) ) \to \operatorname{AlternatingMap}(R,M,\prod_i N_i,\iota). $$$
Lean4
instance instAdd : Add (M [⋀^ι]→ₗ[R] N) where
add a
b :=
{ (a + b : MultilinearMap R (fun _ : ι => M) N) with
map_eq_zero_of_eq' := fun v i j h hij => by simp [a.map_eq_zero_of_eq v h hij, b.map_eq_zero_of_eq v h hij] }
