English
There exists a canonical R-linear inclusion i_inr: A → Unitization(R, A) given by a ↦ inr(a); this inclusion is R-linear, i.e., i_inr(r · a) = r · i_inr(a) and i_inr(a + b) = i_inr(a) + i_inr(b).
Русский
Существуют каноническое R-линейное включение i_inr: A → Unitization(R, A), заданное i_inr(a) = inr(a); линейность означает i_inr(r · a) = r · i_inr(a) и i_inr(a + b) = i_inr(a) + i_inr(b).
LaTeX
$$$\exists i: A \to_{R} Unitization(R,A),\ i(a) = \mathrm{inr}(a)\quad\text{для всех } a \in A.$$$
Lean4
/-- The canonical `R`-linear inclusion `A → Unitization R A`. -/
@[simps apply]
def inrHom [Semiring R] [AddCommMonoid A] [Module R A] : A →ₗ[R] Unitization R A :=
{ LinearMap.inr R R A with toFun := (↑) }
