instPreorderCarrierCarrierCommRingCat

English

We equip schemes with the specialization preorder, where x specializes to y if y lies in the closure of {x}.

Русский

Мы вводим у схем специализацию как предопределённое отношение: точка x специализируется на точке y, если y лежит в замыкании {x}.

LaTeX

$$$\text{preorder } X = \text{specializationPreorder}(X)$$$

Lean4

/-- We give schemes the specialization preorder by default.
-/
instance {X : Scheme.{u}} : Preorder X :=
  specializationPreorder X

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