English
Let E be a module over a ring and p ⊆ E a submodule. The canonical inclusion of p into E, viewed as a linear map p → E, coincides with the linear map obtained from the subtype structure of p; i.e., the inclusion map is the same whether viewed via the subtype or directly as a linear map.
Русский
Пусть E — модуль над кольцом, p ⊆ E — подмодуль. Каноническое включение p в E, рассматриваемое как линейное отображение p → E, совпадает с линейным отображением, полученным через структуру подмодуля p; то есть включение одинаково воспринимается через т. н. подпроявление subtype и напрямую как линейное отображение.
LaTeX
$$$ i_p^{\\mathrm{lin}} = i_p, \\quad \\text{где } i_p: p \\hookrightarrow E \\text{ есть включение}$$$
Lean4
@[simp]
theorem subtypeₗᵢ_toLinearMap : p.subtypeₗᵢ.toLinearMap = p.subtype :=
rfl
