freeDesc — Mathlib

English

Given a map f : X → M from a set X into an R-module M, there is a canonical R-linear map from the free X to M extending f.

Русский

Для отображения f: X → M существует каноническое R-Линейное отображение из свободного X в M, расширяющее f.

LaTeX

$$$\mathrm{freeDesc}: (X \to M) \to ((\mathrm{Free}(R)\!\cdot X) \to M)$$$

Lean4

/-- The morphism of modules `(free R).obj X ⟶ M` corresponding
to a map `f : X ⟶ M`. -/
noncomputable def freeDesc {X : Type u} {M : ModuleCat.{u} R} (f : X ⟶ M) : (free R).obj X ⟶ M :=
  ofHom <| Finsupp.lift M R X f

Похожие утверждения