instLocallyDirectedIsOpenImmersionDirectedAffineCover

English

Let X be a scheme. The directed affine cover X.directedAffineCover provides a locally directed open cover of X.

Русский

Пусть X — схема. Направленное аффинное покрытие X.directedAffineCover образует локально-направленное открытое покрытие X.

LaTeX

$$$$ \operatorname{LocallyDirected}(X.directedAffineCover) $$$$

Lean4

instance : Scheme.Cover.LocallyDirected X.directedAffineCover :=
  .ofIsBasisOpensRange (by simp) <| by
    convert isBasis_affine_open X
    simp

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