English
The pi-construction on a family of alternating maps corresponds to the pi-map of the corresponding multilinear maps; i.e., (pi f) equals MultilinearMap.pi (a ↦ (f a).toMultilinearMap).
Русский
П-образующее построение для семейства чередующихся отображений равно п-образному отображению соответствующих много-линейных карт: (pi f) = MultilinearMap.pi (a ↦ (f a).toMultilinearMap).
LaTeX
$$$ (\pi f) = \operatorname{MultilinearMap}.pi (\lambda a. (f(a)).toMultilinearMap). $$$
Lean4
/-- Combine a family of alternating maps with the same domain and codomains `N i` into an
alternating map taking values in the space of functions `Π i, N i`. -/
@[simps!]
def pi {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)] (f : ∀ i, M [⋀^ι]→ₗ[R] N i) :
M [⋀^ι]→ₗ[R] (∀ i, N i) :=
{ MultilinearMap.pi fun a => (f a).toMultilinearMap with
map_eq_zero_of_eq' := fun _ _ _ h hne => funext fun a => (f a).map_eq_zero_of_eq _ h hne }
