instSurjectiveCompScheme — Mathlib

English

If f: X → Y and g: Y → Z are surjective morphisms of schemes, then their composition f ≫ g is surjective on the underlying topological spaces.

Русский

Если f: X → Y и g: Y → Z — сюръективные морфизмы схем, то композиция f ≫ g сюръективна на подлежащих пространствах.

LaTeX

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

Lean4

instance [Surjective f] [Surjective g] : Surjective (f ≫ g) :=
  ⟨g.surjective.comp f.surjective⟩

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