liftAlgHom_unique

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.liftAlgHom_unique

← MathLib Explorer

English

Same as 33559, formalized for the specialized AlgHom lift.

Русский

То же, что и 33559, специально для сопоставления AlgHom.

LaTeX

$$$\\text{liftAlgHom_unique}$ ( повторение )$$

Lean4

theorem liftAlgHom_unique (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y) (g : RingQuot s →ₐ[S] B)
    (h : g.comp (mkAlgHom S s) = f) : g = liftAlgHom S ⟨f, w⟩ :=
  by
  ext
  simp [h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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