mapHom_id — Mathlib

English

For the identity algebra homomorphism id_R,A, the induced map on submodules is the identity map.

Русский

Для тождестенного алгебраического гомоморфизма id_R A индуцированное отображение на подмодулях есть тождественное отображение.

LaTeX

$$$\mathrm{mapHom}(\mathrm{id}_{R,A}) = \mathrm{id}_{\mathrm{Submodule}(R,A)}$$$

Lean4

theorem mapHom_id : mapHom (.id R A) = .id _ :=
  RingHom.ext map_id

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