English
The map f preserves the left inclusion: applying map to an element coming from the left embedding inl yields the same left embedding of f's image.
Русский
Отображение сохраняет левое вложение: применение map к элементу, полученному из левого внедрения inl, даёт такое же левое вложение изображения f.
LaTeX
$$$\\mathrm{map}\\ f \\ (\\mathrm{inl}\\ r) = \\mathrm{inl}\\ r$$$
Lean4
/-- Functoriality of `TrivSqZeroExt` when the ring is commutative: a linear map
`f : M →ₗ[R'] N` induces a morphism of `R'`-algebras from `TrivSqZeroExt R' M` to
`TrivSqZeroExt R' N`.
Note that we cannot neatly state the non-commutative case, as we do not have morphisms of bimodules.
-/
def map (f : M →ₗ[R'] N) : TrivSqZeroExt R' M →ₐ[R'] TrivSqZeroExt R' N :=
liftEquivOfComm ⟨inrHom R' N ∘ₗ f, fun _ _ => inr_mul_inr _ _ _⟩
