English
There is a natural equivalence between the opens of X and the opens of Y that contain the image f(X); concretely, X.Opens ≃ { U ⊆ Y.opens | U ≤ f.opensRange } via U ↦ ⟨f''ᵁU, image_subset⟩ and its inverse U ↦ f⁻¹ᵁU.
Русский
Существует естественное эквивалентность множеств открытых подмножеств X и открытых подмножеств Y, содержащих образ X, через U ↦ ⟨образ U, условие⟩ и обратное.
LaTeX
$$$$ \text{opensEquiv}(f): X.emptyset \simeq \{U:\, Y.Opens \mid U \le f.opensRange\} $$$$
Lean4
/-- The open sets of an open subscheme corresponds to the open sets containing in the image. -/
@[simps]
def opensEquiv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] : X.Opens ≃ { U : Y.Opens // U ≤ f.opensRange }
where
toFun U := ⟨f ''ᵁ U, Set.image_subset_range _ _⟩
invFun U := f ⁻¹ᵁ U
left_inv _ := Opens.ext (Set.preimage_image_eq _ f.isOpenEmbedding.injective)
right_inv U := Subtype.ext (Opens.ext (Set.image_preimage_eq_of_subset U.2))
