opensRestrict — Mathlib

English

Open sets of the restricted scheme U correspond to opens V in X contained in U.

Русский

Открытые множества ограниченной схемы U соответствуют открытым множествам V в X, содержащимся в U.

LaTeX

$$$ opens(U) \\cong \\{ V \\in opens(X) \\mid V \\le U \\}$$$

Lean4

/-- The open sets of an open subscheme corresponds to the open sets containing in the subset. -/
@[simps!]
def opensRestrict : Scheme.Opens U ≃ { V : X.Opens // V ≤ U } :=
  (IsOpenImmersion.opensEquiv (U.ι)).trans (Equiv.subtypeEquivProp (by simp))

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