ι_basicOpen_preimage — Mathlib

English

The preimage under the basic open immersion ι of a basic open is affine.

Русский

Предобраз вскрытия базовой области через ι афинен.

LaTeX

$$$((X.basicOpen r).\!ι)^{-1}\!U$ is affine$$

Lean4

theorem ι_basicOpen_preimage (r : Γ(X, ⊤)) : IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U) :=
  by
  apply (X.basicOpen r).ι.isAffineOpen_iff_of_isOpenImmersion.mp
  dsimp [Scheme.Hom.opensFunctor, LocallyRingedSpace.IsOpenImmersion.opensFunctor]
  rw [Opens.functor_obj_map_obj, Opens.isOpenEmbedding_obj_top, inf_comm, ←
    Scheme.basicOpen_res _ _ (homOfLE le_top).op]
  exact hU.basicOpen _

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