English
If M has a presentation and there is a solution in another module N, there is a canonical induced linear map M → N defined by composing the inverse presentation map with the solution map.
Русский
Если M имеет презентацию и существует решение в модуле N, то существует каноническое индуцированное линейное отображение M → N, задаваемое составлением инверсии линейного эквивалента презентации с решением.
LaTeX
$$$$ \\mathrm{desc}_s = s.fromQuotient \\circ h.linearEquiv^{-1} : M \\to N $$$$
Lean4
/-- If `M` admits a presentation by generators and relations, and we have a solution of the
same equations in a module `N`, then this is the canonical induced linear map `M →ₗ[A] N`. -/
noncomputable def desc (s : relations.Solution N) : M →ₗ[A] N :=
s.fromQuotient.comp h.linearEquiv.symm.toLinearMap
