English
Two partial maps from a reduced X to a separated Y are equivalent if their restrictions to the intersection of their domains are equal.
Русский
Две частичные карты от редуцированной схемы X в разделимую Y эквивалентны, если их ограничения к пересечению областей совпадают.
LaTeX
$$$f:\ X.PartialMap Y,\ g:\ X.PartialMap Y,\ f.domain = g.domain\Rightarrow\ f\equiv g\iff f|_{f.domain} = g|_{g.domain}$$$
Lean4
/-- Two partial maps from reduced schemes to separated schemes are equivalent if and only if
they are equal on the intersection of the domains. -/
theorem equiv_iff_of_isSeparated [X.Over S] [Y.Over S] [IsReduced X] [IsSeparated (Y ↘ S)] {f g : X.PartialMap Y}
[f.IsOver S] [g.IsOver S] :
f.equiv g ↔
(f.restrict _ (f.2.inter_of_isOpen_left g.2 f.domain.2) inf_le_left).hom =
(g.restrict _ (f.2.inter_of_isOpen_left g.2 f.domain.2) inf_le_right).hom :=
equiv_iff_of_isSeparated_of_le (S := S) _ _ _
