of_openCover — Mathlib

English

If for every i in a given open cover 𝒰 of X we have P((𝒰.f i) ≫ f), then P f.

Русский

Если для каждого элемента открытого покрытия 𝒰 морфизм P((𝒰.f i) ≫ f) выполняется, то выполняется и P f.

LaTeX

$$$\forall {P : \mathrm{MorphismProperty}(\mathrm{Scheme})} [IsZariskiLocalAtSource P],\; (\forall i, P((\mathcal{U}.f i) \circ f)) \Rightarrow P f.$$$

Lean4

theorem of_openCover (H : ∀ i, P (𝒰.f i ≫ f)) : P f :=
  by
  refine of_iSup_eq_top (fun i ↦ (𝒰.f i).opensRange) 𝒰.iSup_opensRange fun i ↦ ?_
  rw [←
    IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm),
    Category.assoc, P.cancel_left_of_respectsIso]
  exact H i

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