liftAlgHom_toRingHom

Mathlib.RingTheory.Localization.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalization.liftAlgHom_toRingHom

English

There is an algebra homomorphism lifting from S to P through IsLocalization.

Русский

Существует алгебраическое отображение, поднимающее из S в P через IsLocalization.

LaTeX

$$$\\mathrm{liftAlgHom}: S \\to\\_{} P$$$

Lean4

theorem liftAlgHom_toRingHom : (liftAlgHom hf : S →ₐ[A] P).toRingHom = lift hf :=
  rfl

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

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

Разделы

Аффилиация

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