exists_eq_pow_mul_of_isAffineOpen

English

Let X be a scheme, U an affine open, hU an IsAffineOpen, and f ∈ Γ(X, U), x ∈ Γ(X, X.basicOpen f). Then there exist n and y ∈ Γ(X, U) such that y restricted to X.basicOpen f equals f restricted to X.basicOpen f raised to n times x.

Русский

Пусть X — схема, U — аффинное открытое подмножество, hU, f и x как указано; существует n и y на U с равенством restricted, как в формуле.

LaTeX

$$$\\exists n, \\exists y\\in \\Gamma(X,U),\\; y|_{X.BasOpen(f)}=(f|_{X.BasOpen(f)})^{n} \\cdot x.$$$

Lean4

theorem exists_eq_pow_mul_of_isAffineOpen (X : Scheme) (U : X.Opens) (hU : IsAffineOpen U) (f : Γ(X, U))
    (x : Γ(X, X.basicOpen f)) : ∃ (n : ℕ) (y : Γ(X, U)), y |_ X.basicOpen f = (f |_ X.basicOpen f) ^ n * x :=
  by
  have := (hU.isLocalization_basicOpen f).2
  obtain ⟨⟨y, _, n, rfl⟩, d⟩ := this x
  use n, y
  simpa [mul_comm x] using d.symm

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