preimageIso — Mathlib

English

If f: X → Y is an isomorphism, then for any open U ⊆ Y the preimage f^{-1}(U) is canonically isomorphic to U.

Русский

Если f: X → Y — изоморфизм, то для любого открытого U ⊆ Y его прообраз f^{-1}(U) изоморфен U.

LaTeX

$$(f.preimageIso U) ≅ U$$

Lean4

/-- The restriction of an isomorphism onto an open set. -/
noncomputable def preimageIso {X Y : Scheme.{u}} (f : X.Hom Y) [IsIso (C := Scheme) f] (U : Y.Opens) :
    (f ⁻¹ᵁ U).toScheme ≅ U :=
  by
  apply IsOpenImmersion.isoOfRangeEq (f := (f ⁻¹ᵁ U).ι ≫ f) U.ι _
  dsimp
  rw [Set.range_comp, Opens.range_ι, Opens.range_ι]
  refine @Set.image_preimage_eq _ _ f.base U.1 f.homeomorph.surjective

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