of_openCover — Mathlib

English

If 𝒰 is an open cover of Y by affine opens and Q holds for all pullbacks 𝒰.pullbackHom f i, then P f holds.

Русский

Пусть 𝒰 — открытое покрытие Y на аффинных открытых подмножеств; если для всех pullback Hom 𝒰 f i выполняется Q, то P f.

LaTeX

$$$\forall i,\; Q(\mathcal{U}.pullbackHom f i) \Rightarrow P f$$$

Lean4

theorem of_openCover (𝒰 : Y.OpenCover) [∀ i, IsAffine (𝒰.X i)] (h𝒰 : ∀ i, Q (𝒰.pullbackHom f i)) : P f :=
  letI := isLocal_affineProperty P
  of_iSup_eq_top (fun i ↦ ⟨_, isAffineOpen_opensRange (𝒰.f i)⟩) 𝒰.iSup_opensRange
    (fun i ↦ (Q.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h𝒰 i))

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