English
There is a canonical linear map (X → M) → (Y → M) associated to any map f: X → Y between finite type domains, defined by precomposition with f and the Finsupp linear structure.
Русский
Существует каноническое линейное отображение (X → M) → (Y → M), связанное с любым отображением f: X → Y между конечными множностями, задающееся с помощью предварительной композиции и линейной структуры FinSupp.
LaTeX
$$$L_f: (X \to M) \to (Y \to M) \quad$ (LinMap) $$
Lean4
/-- The linear map `(X → M) →ₗ[R] (Y → M)` induced by a map `X → Y` between finite types. -/
noncomputable def linearMap [Finite X] [Finite Y] (f : X → Y) : (X → M) →ₗ[R] (Y → M) :=
(((Finsupp.linearEquivFunOnFinite R M Y)).comp (Finsupp.lmapDomain M R f)).comp
(Finsupp.linearEquivFunOnFinite R M X).symm.toLinearMap
