instCategory

Mathlib.Algebra.Category.ModuleCat.Topology.Basic

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

English

TopModuleCat(R) is equipped with a category structure.

Русский

TopModuleCat(R) обладает структурой категории.

LaTeX

$$$\mathrm{Category}(\mathrm{TopModuleCat}(R))$$$

Lean4

instance : Category (TopModuleCat R) where
  Hom := Hom
  id M := ⟨ContinuousLinearMap.id R M⟩
  comp φ ψ := ⟨ψ.hom' ∘L φ.hom'⟩

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

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

Разделы

Аффилиация

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