English
The map that takes a family of linear maps and returns a multilinear map by composing with a fixed multilinear map is multilinear in the arguments.
Русский
Отображение, принимающее семью линейных отображений и возвращающее мультилинейное отображение через композицию с фиксированным мультилейнерным отображением, является мультилинейарным по аргументам.
LaTeX
$$$$\text{CompLinearMapMultilinear}(f, g) = g \circ f, \quad \text{multilinear in the coordinates.}$$$$
Lean4
/-- If `f` is a collection of linear maps, then the construction `MultilinearMap.compLinearMap`
sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g` and multilinear in
`f₁, ..., fₙ`. -/
@[simps]
def compLinearMapMultilinear :
@MultilinearMap R ι (fun i ↦ M₁ i →ₗ[R] M₁' i) ((MultilinearMap R M₁' M₂) →ₗ[R] MultilinearMap R M₁ M₂) _ _ _
(fun _ ↦ LinearMap.module) _
where
toFun := MultilinearMap.compLinearMapₗ
map_update_add' := by
intro _ f i f₁ f₂
ext g x
change
(g fun j ↦ update f i (f₁ + f₂) j <| x j) = (g fun j ↦ update f i f₁ j <| x j) + g fun j ↦ update f i f₂ j (x j)
let c : Π (i : ι), (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f ↦ f (x i)
convert g.map_update_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i)) with j j j
· exact Function.apply_update c f i (f₁ + f₂) j
· exact Function.apply_update c f i f₁ j
· exact Function.apply_update c f i f₂ j
map_update_smul' := by
intro _ f i a f₀
ext g x
change (g fun j ↦ update f i (a • f₀) j <| x j) = a • g fun j ↦ update f i f₀ j (x j)
let c : Π (i : ι), (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f ↦ f (x i)
convert g.map_update_smul (fun j ↦ f j (x j)) i a (f₀ (x i)) with j j j
· exact Function.apply_update c f i (a • f₀) j
· exact Function.apply_update c f i f₀ j
