isAffineOpen_of_isAffineOpen_basicOpen

English

Definition of the preimage of an affine open as an affine opens element.

Русский

Определение прообраза аффинного открытого множества как элемента aффинных opens.

LaTeX

$$$\\text{def affinePreimage} (f) (U) : X.\\text{affineOpens} := f^{-1}_{\\text{op}} U$$$

Lean4

/-- If `s` is a spanning set of `Γ(X, U)`, such that each `X.basicOpen i` is affine, then `U` is also
affine.
-/
theorem isAffineOpen_of_isAffineOpen_basicOpen (U) (s : Set Γ(X, U)) (hs : Ideal.span s = ⊤)
    (hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)) : IsAffineOpen U :=
  by
  apply isAffine_of_isAffineOpen_basicOpen (U.topIso.inv '' s)
  · rw [← Ideal.map_span U.topIso.inv.hom, hs, Ideal.map_top]
  · rintro _ ⟨j, hj, rfl⟩
    rw [← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion, Scheme.image_basicOpen]
    simpa [Scheme.Opens.toScheme_presheaf_obj] using hs₂ j hj

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