instSurjectiveOfIsIsoScheme — Mathlib

English

If f: X → Y is an isomorphism of schemes, then the base map f_base: |X| → |Y| is surjective (indeed a homeomorphism).

Русский

Если морфизм f: X → Y является изоморфизмом схем, тогда базовое отображение f_base: |X| → |Y| сюръективно (фактически это гомеоморфизм).

LaTeX

$$$\mathrm{Surjective}(f_{\mathrm{base}})$$$

Lean4

instance (priority := 100) [IsIso f] : Surjective f :=
  ⟨f.homeomorph.surjective⟩

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