algebraMap_eq_inl

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.algebraMap_eq_inl

English

There is a canonical S-algebra isomorphism between algebra maps and left injections via inlHom.

Русский

Существует каноническое S-алгебраическое изоморство между алгебраическими отображениями и левым внедрением via inlHom.

LaTeX

$$$ algebraMap R' (tsze R' M) = inlHom R' M $$$

Lean4

theorem algebraMap_eq_inl : ⇑(algebraMap R' (tsze R' M)) = inl :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru