isAffineOpen_iff_of_isOpenImmersion

English

For a morphism f: X ⟶ Y that is an open immersion, IsAffineOpen of f.opensFunctor.obj U is equivalent to IsAffineOpen U for any open U ⊆ X.

Русский

Для морфизма f: X ⟶ Y, являющегося открытым вложением, IsAffineOpen (f.opensFunctor.obj U) эквивалентно IsAffineOpen U для любого открытого U ⊆ X.

LaTeX

$$IsAffineOpen (f.opensFunctor.obj U) ↔ IsAffineOpen U$$

Lean4

theorem _root_.AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion (f : AlgebraicGeometry.Scheme.Hom X Y)
    [H : IsOpenImmersion f] {U : X.Opens} : IsAffineOpen (f ''ᵁ U) ↔ IsAffineOpen U
    where
  mp
    hU :=
    by
    refine
      .of_isIso (IsOpenImmersion.isoOfRangeEq (X.ofRestrict U.isOpenEmbedding ≫ f) (Y.ofRestrict _) ?_).hom (h := hU)
    rw [Scheme.comp_base, TopCat.coe_comp, Set.range_comp]
    dsimp [Opens.coe_inclusion', Scheme.restrict]
    rw [Subtype.range_coe, Subtype.range_coe]
    rfl
  mpr hU := hU.image_of_isOpenImmersion f

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