exists_of_res_eq_of_qcqs — Mathlib

English

If two global sections f and g agree on a basic open, then there exists an exponent n and a witness y such that the localized equalities hold as powers of the common restriction.

Русский

Если две секции согласованы на базовом открытом, тогда существует n и свидетель y such, что локализации равны как степени от общего ограничения.

LaTeX

$$$$\\exists n, y \\;:\\; y|_{X.basicOpen(f)}=(f|_{X.basicOpen(f)})^{n} \\cdot x$$$$

Lean4

theorem exists_of_res_eq_of_qcqs {X : Scheme.{u}} {U : TopologicalSpace.Opens X} (hU : IsCompact U.carrier)
    (hU' : IsQuasiSeparated U.carrier) {f g s : Γ(X, U)} (hfg : f |_ X.basicOpen s = g |_ X.basicOpen s) :
    ∃ n, s ^ n * f = s ^ n * g :=
  by
  obtain ⟨n, hc⟩ := (isLocalization_basicOpen_of_qcqs hU hU' s).exists_of_eq s hfg
  use n

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