topObj

Mathlib.AlgebraicGeometry.Spec

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Spec.topObj

Lean4

/-- The spectrum of a commutative ring, as a topological space.
-/
def topObj (R : CommRingCat.{u}) : TopCat :=
  TopCat.of (PrimeSpectrum R)

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

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

Разделы

Аффилиация

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