affineLocally_iff_affineOpens_le — Mathlib

English

Under suitable hypotheses, the localizability of a property over affine opens yields a local property on morphisms.

Русский

При подходящих условиях локализуемость свойства по аффинным открытым множествам задаёт локальное свойство для морфингов.

LaTeX

$$(SourceAffineLocally P).IsLocal$$

Lean4

theorem affineLocally_iff_affineOpens_le {X Y : Scheme.{u}} (f : X ⟶ Y) :
    affineLocally.{u} P f ↔ ∀ (U : Y.affineOpens) (V : X.affineOpens) (e : V.1 ≤ f ⁻¹ᵁ U.1), P (f.appLE U V e).hom :=
  forall_congr' fun U ↦ sourceAffineLocally_morphismRestrict P f U U.2

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