English
If a directed family of affine opens U_i cover Y in the sense that their union is top, and Q holds for all restrictions f|_{U_i}, then P f holds.
Русский
Пусть семейство афинных открытых множеств U_i образует открытое покрытие Y и их объединение даёт верхнюю грань, тогда если Q выполняется для всех ограничений f|_{U_i}, тогда P f выполняется.
LaTeX
$$$\forall U: ι \to Y.prop,\; (\bigcup_i U_i)=\top \Rightarrow (\forall i, Q(f|_{U_i}) ) \Rightarrow P(f)$$$
Lean4
theorem of_iSup_eq_top {ι} (U : ι → Y.affineOpens) (hU : ⨆ i, (U i : Y.Opens) = ⊤) (hU' : ∀ i, Q (f ∣_ U i)) : P f :=
by
letI := isLocal_affineProperty P
rw [eq_targetAffineLocally P]
classical
intro V
induction V using of_affine_open_cover U hU with
| basicOpen U r h =>
haveI : IsAffine _ := U.2
have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
exact (Q.arrow_mk_iso_iff (morphismRestrictRestrictBasicOpen f _ r)).mp this
| openCover U s hs
H =>
apply
AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _ (s.image (Scheme.Opens.topIso _).inv)
(by simp [← Ideal.map_span, hs, Ideal.map_top])
intro ⟨r, hr⟩
obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
exact (Q.arrow_mk_iso_iff (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
| hU i => exact hU' i
