English
The piFamily of Pi.single p f equals LinearMap.single p composed with the projection maps applied to f.
Русский
piFamily от Pi.single p f эквивалентно LinearMap.single p, композиция с проекциями на f.
LaTeX
$$$\piFamily (\Pi.single p f) = (\mathrm{LinearMap.single}\ R\ N\ p) \circ_{\text{multilinear}} (f \circ_{\text{lin}} \mathrm{proj} (p i)).$$$
Lean4
/-- Given a family of indices `κ` and a multilinear map `f p` for each way `p` to select one index from
each family, `piFamily f` maps a family of functions (one for each domain `κ i`) into a function
from each selection of indices (with domain `Π i, κ i`).
-/
@[simps]
def piFamily (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
MultilinearMap R (fun i => Π j : κ i, M i j) (Π t : Π i, κ i, N t)
where
toFun x := fun p => f p (fun i => x i (p i))
map_update_add' {dec} m i x
y :=
funext fun p => by
dsimp
simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.add_apply, (f p).map_update_add]
map_update_smul' {dec} m i c
x :=
funext fun p => by
dsimp
simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.smul_apply, (f p).map_update_smul]
