affineOpensRestrict — Mathlib

English

There is a natural equivalence between the affine opens of the open subscheme U ⊆ X and the affine opens of X that lie inside U.

Русский

Существует естественное эквивалентное соответствие аффинных открытых подмножеств открытого подсхемы U ⊆ X и аффинных открытых подмножеств X, лежащих внутри U.

LaTeX

$$IsOpenImmersion.affineOpensEquiv (U.ι)$$

Lean4

/-- The affine open sets of an open subscheme
corresponds to the affine open sets containing in the subset. -/
@[simps! apply_coe_coe]
def _root_.AlgebraicGeometry.affineOpensRestrict {X : Scheme.{u}} (U : X.Opens) :
    U.toScheme.affineOpens ≃ { V : X.affineOpens // V ≤ U } :=
  (IsOpenImmersion.affineOpensEquiv U.ι).trans (Equiv.subtypeEquivProp (by simp))

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