English
Two partial maps from a reduced scheme X to a separated scheme Y are equivalent if and only if they agree on every open dense subset W ⊆ X (and the appropriate domain inclusions hold).
Русский
Две частичные карты от редуцированной схемы X к разделимой схеме Y эквивалентны тогда и только тогда, когда они совпадают на любой открытой плотной подмножество W ⊆ X (при выполнении соответствующих вложений областей).
LaTeX
$$$\forall X,Y,S,\ [X\text{ Over }S] [Y\text{ Over }S] [\text{IsReduced}(X)] [\text{IsSeparated}(Y \downarrow S)],\ f,g:X.PartialMap Y,\ W\subseteq X.\Dense(W),\ W\le f.domain, W\le g.domain:\
f.\equiv g \iff (f|_W)_{\hom} = (g|_W)_{\hom} .$$
Lean4
/-- Two partial maps from reduced schemes to separated schemes are equivalent if and only if
they are equal on **any** open dense subset. -/
theorem equiv_iff_of_isSeparated_of_le [X.Over S] [Y.Over S] [IsReduced X] [IsSeparated (Y ↘ S)] {f g : X.PartialMap Y}
[f.IsOver S] [g.IsOver S] {W : X.Opens} (hW : Dense (X := X) W) (hWl : W ≤ f.domain) (hWr : W ≤ g.domain) :
f.equiv g ↔ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom :=
by
refine ⟨fun ⟨V, hV, hVl, hVr, e⟩ ↦ ?_, fun e ↦ ⟨_, _, _, _, e⟩⟩
have : IsDominant (X.homOfLE (inf_le_left : W ⊓ V ≤ W)) := Opens.isDominant_homOfLE (hW.inter_of_isOpen_left hV W.2) _
apply ext_of_isDominant_of_isSeparated' S (X.homOfLE (inf_le_left : W ⊓ V ≤ W))
simpa using congr(X.homOfLE (inf_le_right : W ⊓ V ≤ V) ≫ $e)
