top — Mathlib

English

The topology on Proj is the topology induced by the projective spectrum 𝒜.

Русский

Топология на Proj есть топология, индуцированная проектным спектром 𝒜.

LaTeX

$$$ \text{top}(\mathcal{A}) = \mathrm{TopCat}.of(\mathrm{ProjectiveSpectrum}(\mathcal{A})) $$$

Lean4

/-- The underlying topology of `Proj` is the projective spectrum of graded ring `A`. -/
def top : TopCat :=
  TopCat.of (ProjectiveSpectrum 𝒜)

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