instCategory

Mathlib.Topology.Category.TopCommRingCat

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

Lean4

instance : Category TopCommRingCat.{u}
    where
  Hom R S := { f : R →+* S // Continuous f }
  id R := ⟨RingHom.id R, by rw [RingHom.id]; continuity⟩
  comp f
    g :=
    ⟨g.val.comp f.val, by
      -- TODO automate

      cases f
      cases g
      continuity⟩

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

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

Разделы

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

Аффилиация

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