reduce_to_affine_nbhd — Mathlib

English

If a property P holds for all points in every affine neighborhood Spec R and is preserved by open immersions, then P holds for every point of every scheme.

Русский

Если свойство P верно для каждого точки в каждом аффинном окрестности Spec R и сохраняется при открытых вложениях, то P верно для каждой точки любой схемы.

LaTeX

$$$\forall X, \forall x \in X, \ P(X, x)$, при условии двух условий аналогично reduce_to_affine_nbhd$$

Lean4

theorem reduce_to_affine_nbhd (P : ∀ (X : Scheme) (_ : X), Prop) (h₁ : ∀ R x, P (Spec R) x)
    (h₂ : ∀ {X Y} (f : X ⟶ Y) [IsOpenImmersion f] (x : X), P X x → P Y (f.base x)) : ∀ (X : Scheme) (x : X), P X x :=
  by
  intro X x
  obtain ⟨y, e⟩ := X.affineCover.covers x
  convert h₂ (X.affineCover.f (X.affineCover.idx x)) y _
  · rw [e]
  apply h₁

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