English
There is a linear equivalence between families of linear maps acting entrywise and linear maps from matrices: (m × n → α →ₗ[R] β) ≃ (Matrix m n α →ₗ[R] β).
Русский
Существуют линейные экваленты между семействами отображений, действующих по элементам, и линейными отображениями из матриц: (m × n → α →ₗ[R] β) ≃ (Matrix m n α →ₗ[R] β).
LaTeX
$$$ \\mathrm{liftLinear} : (m \\to n \\to α \\toₗ[R] β) \\simeqₗ[S] (Matrix m n α \\toₗ[R] β) $$$
Lean4
/-- Families of linear maps acting on each element are equivalent to linear maps from a matrix.
This can be thought of as the matrix version of `LinearMap.lsum`. -/
def liftLinear : (m → n → α →ₗ[R] β) ≃ₗ[S] (Matrix m n α →ₗ[R] β) :=
LinearEquiv.piCongrRight (fun _ => LinearMap.lsum R _ S) ≪≫ₗ LinearMap.lsum R _ S ≪≫ₗ
LinearEquiv.congrLeft _ _
(ofLinearEquiv _)
-- not `simp` to let `liftLinear_single` fire instead
