fromSpec_preimage_basicOpen' — Mathlib

English

The preimage of a basic open under fromSpec corresponds to the basic open in the Γ-side after the ΓSpecIso translation.

Русский

Предобраз базовой ограниченной области под fromSpec соответствует базовой области на стороне Γ после перевода через ΓSpecIso.

LaTeX

$$$h_U.fromSpec^{-1}\!X.basicOpen f = \mathrm{Spec}\Gamma(X,U).basicOpen( (\mathrm{ΓSpecIso}(X,U)^{-1})f)$$$

Lean4

theorem fromSpec_preimage_basicOpen' :
    hU.fromSpec ⁻¹ᵁ X.basicOpen f = (Spec Γ(X, U)).basicOpen ((Scheme.ΓSpecIso Γ(X, U)).inv f) :=
  by
  rw [Scheme.preimage_basicOpen, hU.fromSpec_app_self]
  exact Scheme.basicOpen_res_eq _ _ (eqToHom hU.fromSpec_preimage_self).op

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