instRespectsIsoSchemeSurjective — Mathlib

English

A surjectivity property is preserved under isomorphisms of schemes: if f is an isomorphism, then f is surjective.

Русский

Сюръективность сохраняется при изоморфизма схем: если f является изоморфизмом, то f сюръективен.

LaTeX

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

Lean4

instance : MorphismProperty.RespectsIso @Surjective :=
  surjective_eq_topologically ▸ topologically_respectsIso _ (fun e ↦ e.surjective) (fun _ _ hf hg ↦ hg.comp hf)

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