hasForgetToCommRingCat

Mathlib.Topology.Category.TopCommRingCat

URI: https://scilib.ai/kg/mathlib#TopCommRingCat.hasForgetToCommRingCat

← MathLib Explorer

English

There is a forgetful two-sided functor from TopCommRingCat to CommRingCat.

Русский

Существует функтор забывания двухсторонний от TopCommRingCat к CommRingCat.

LaTeX

$$$\\text{HasForget₂ TopCommRingCat CommRingCat}$$$

Lean4

instance hasForgetToCommRingCat : HasForget₂ TopCommRingCat CommRingCat :=
  HasForget₂.mk' (fun R => CommRingCat.of R) (fun _ => rfl) (fun f => CommRingCat.ofHom f.val) HEq.rfl

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

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

Разделы

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

Аффилиация

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