English
The lemmas assert linearity properties of iteratedFDerivComponent in separately specified arguments, showing how updates to the input coordinates impact the component linearly or via bilinear modifications.
Русский
Леммы устанавливают линейность компонент iteratedFDerivComponent по отдельным аргументам и показывают, как изменения в координатах входа влияют на компоненту линейно или билинейно.
LaTeX
$$$$\text{Properties of } \operatorname{iteratedFDerivComponent}, \quad \text{linearity in outer variables and inner vectors.}$$$$
Lean4
/-- Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module.
Let us denote `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` by `M` and `M'` respectively.
If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear
map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` via `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`.
-/
@[simps!]
def piLinearMap : MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂)
where
toFun g := (LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear
map_add' := by simp
map_smul' := by simp
