theorem AlgebraicGeometry.eq_of_agree_on_nonempty_open {X Y : Scheme} [IrreducibleSpace ↥X] [IsReduced X] [Y.IsSeparated] {f g : X ⟶ Y} (U : X.Opens) (hU_ne : (↑U).Nonempty) (h_agree : CategoryTheory.CategoryStruct.comp U.ι f = CategoryTheory.CategoryStruct.comp U.ι g) : f = g

Uniqueness of morphisms to a separated scheme: two maps f, g : X → Y from an irreducible reduced scheme X into a separated scheme Y that agree on a nonempty open subscheme are equal.

theorem AlgebraicGeometry.eq_of_agree_on_nonempty_open_over_base {X Y S : Scheme} [IrreducibleSpace ↥X] [IsReduced X] {s : Y ⟶ S} [IsSeparated s] {g h : X ⟶ Y} (hs : CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.comp h s) (U : X.Opens) (hU_ne : (↑U).Nonempty) (h_agree : CategoryTheory.CategoryStruct.comp U.ι g = CategoryTheory.CategoryStruct.comp U.ι h) : g = h

Relative version of uniqueness: two S-morphisms g, h : X → Y from an irreducible reduced scheme X that agree on a nonempty open subscheme are equal, provided Y → S is separated.