isomorphisms_eq_isOpenImmersion_inf_surjective

English

The class of isomorphisms of schemes equals the intersection of open immersions with surjective morphisms.

Русский

Класс изоморфизмов схем равен пересечению открытых вложений и сюръективных отображений.

LaTeX

$$isomorphisms Scheme = (IsOpenImmersion ⊓ Surjective)$$

Lean4

theorem isomorphisms_eq_isOpenImmersion_inf_surjective :
    isomorphisms Scheme = (@IsOpenImmersion ⊓ @Surjective : MorphismProperty Scheme) :=
  by
  ext
  exact
    (isIso_iff_isOpenImmersion _).trans
      (and_congr Iff.rfl ((TopCat.epi_iff_surjective _).trans (surjective_iff _).symm))

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