range_eq_range_of_surjective — Mathlib

English

For any surjective morphism f: X → Y, the same fact holds for the underlying map f_base: |X| → |Y|: its range is all of |Y|.

Русский

Для любого сюръективного морфизма f: X → Y базовое отображение f_base: |X| → |Y| также покрывает все |Y|.

LaTeX

$$$\operatorname{range}(f_{\mathrm{base}}) = |Y|$$$

Lean4

theorem range_eq_range_of_surjective {S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y) [Surjective e]
    (hge : e ≫ g = f) : Set.range f.base = Set.range g.base :=
  by
  rw [← hge]
  simp [Set.range_comp]

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