isoImage — Mathlib

English

If f: X → Y is an open immersion, then for any open U ⊆ X, there is a canonical isomorphism U ≅ f^{-1}(U)ᵁ, identifying the open subscheme with the preimage under f.

Русский

Пусть f: X → Y — открытое внедрение; для любого открытого U ⊆ X существует естественное изоморфизм U ≅ f^{-1}(U).

LaTeX

$$$U^{toScheme} \\cong f^{-1}U^\\text{open}$$$

Lean4

/-- If `f : X ⟶ Y` is an open immersion, then for any `U : X.Opens`,
we have the isomorphism `U ≅ f ''ᵁ U`. -/
noncomputable def isoImage {X Y : Scheme.{u}} (f : X.Hom Y) [IsOpenImmersion f] (U : X.Opens) : U.toScheme ≅ f ''ᵁ U :=
  IsOpenImmersion.isoOfRangeEq (Opens.ι _ ≫ f) (Opens.ι _) (by simp [Set.range_comp])

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