preimage_basicOpen_top — Mathlib

English

For a morphism f: X ⟶ Y and a basic open Y.basicOpen r, the preimage under f is the basic open X.basicOpen of the pulled-back section f.app r.

Русский

Для гомоморфизма f: X ⟶ Y и базового открытого Y.basicOpen r прообразом по f является X.basicOpen от вытянутой секции f.app r.

LaTeX

$$$f^{-1}(Y.basicOpen r) = X.basicOpen\\left(f.app U r\\right)$$$

Lean4

theorem preimage_basicOpen_top {X Y : Scheme.{u}} (f : X ⟶ Y) (r : Γ(Y, ⊤)) :
    f ⁻¹ᵁ (Y.basicOpen r) = X.basicOpen (f.appTop r) :=
  preimage_basicOpen ..

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