exists_isAffineOpen_mem_and_subset

English

For any x in an open neighborhood U of a scheme X, there exists an affine open W containing x with W ⊆ U.

Русский

Для любой точки x в открытом окрестности U схемы X найдётся аффинное открытое W, содержащее x и включённое в U.

LaTeX

$$$$ \forall X:\text{Scheme},\forall x:\ X,\forall U:\ X.\mathrm{Opens},\ x\in U \Rightarrow \exists W:\ X.\mathrmOpens,\ \mathrmIsAffineOpen(W)\land x\in W\land W\subseteq U. $$$$

Lean4

theorem exists_isAffineOpen_mem_and_subset {X : Scheme.{u}} {x : X} {U : X.Opens} (hxU : x ∈ U) :
    ∃ W : X.Opens, IsAffineOpen W ∧ x ∈ W ∧ W.1 ⊆ U :=
  by
  obtain ⟨R, f, hf⟩ := AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset hxU
  exact ⟨Scheme.Hom.opensRange f (H := hf.1), ⟨AlgebraicGeometry.isAffineOpen_opensRange f (H := hf.1), hf.2.1, hf.2.2⟩⟩

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