English
If a predicate P on affine opens satisfies closure under basic opens and finite-span unions, and holds for an affine cover, then P holds for every affine open.
Русский
Если свойство P на аффинных открытых замкнуто относительно базисных открытых и объединений с конечной линзой, и если P выполняется на аффинном покрытии, тогда P выполняется для любого аффинного открытого.
LaTeX
$$IsAffineOpen.of_affine_open_cover$$
Lean4
/-- Let `P` be a predicate on the affine open sets of `X` satisfying
1. If `P` holds on `U`, then `P` holds on the basic open set of every section on `U`.
2. If `P` holds for a family of basic open sets covering `U`, then `P` holds for `U`.
3. There exists an affine open cover of `X` each satisfying `P`.
Then `P` holds for every affine open of `X`.
This is also known as the **Affine communication lemma** in [*The rising sea*][RisingSea]. -/
@[elab_as_elim]
theorem of_affine_open_cover {X : Scheme} {P : X.affineOpens → Prop} {ι} (U : ι → X.affineOpens)
(iSup_U : (⨆ i, U i : X.Opens) = ⊤) (V : X.affineOpens)
(basicOpen : ∀ (U : X.affineOpens) (f : Γ(X, U)), P U → P (X.affineBasicOpen f))
(openCover :
∀ (U : X.affineOpens) (s : Finset (Γ(X, U))) (_ : Ideal.span (s : Set (Γ(X, U))) = ⊤),
(∀ f : s, P (X.affineBasicOpen f.1)) → P U)
(hU : ∀ i, P (U i)) : P V := by
classical
have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) :=
by
intro x
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (show x.1 ∈ (⨆ i, U i : X.Opens) from iSup_U ▸ trivial)
obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
refine ⟨f, hf, ?_⟩
convert basicOpen _ g (hU i) using 1
ext1
exact e
choose f hf₁ hf₂ using this
suffices Ideal.span (Set.range f) = ⊤
by
obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
apply openCover V t ht₂
rintro ⟨i, hi⟩
obtain ⟨x, rfl⟩ := ht₁ hi
exact hf₂ x
rw [← V.prop.self_le_basicOpen_union_iff]
intro x hx
rw [iSup_range', SetLike.mem_coe, Opens.mem_iSup]
exact ⟨_, hf₁ ⟨x, hx⟩⟩
