English
Two partial maps X ⇒ Y over S are equivalent if there exists a dense open subset W of X contained in both domains on which the two maps agree. In particular, the relation defined by this restriction equality is an equivalence relation.
Русский
Два частичных отображения X ⟶ Y над S эквивалентны тогда и только тогда, когда существует плотная открытая подмножество W ⊆ X, содержащееся в обеих областях определения, на котором отображения совпадают. Относительно такое отношение ограничений образует эквивалентность.
LaTeX
$$$\forall X,Y,S$ schemes over $S$, the relation $\sim$ on $X\!\PartMap\,Y$ defined by: $f \sim g$ iff ∃ $W$ open in $X$ with $Dense(W)$, $W \le f.domain$, $W \le g.domain$ and $(f|W) = (g|W)$ (i.e. $(f.restrict W \; hW \; hWl).hom = (g.restrict W \; hW \; hWr).hom$) is an equivalence relation.$$
Lean4
theorem equivalence_rel : Equivalence (@Scheme.PartialMap.equiv X Y)
where
refl f := ⟨f.domain, f.dense_domain, by simp⟩
symm
{f g} := by
intro ⟨W, hW, hWl, hWr, e⟩
exact ⟨W, hW, hWr, hWl, e.symm⟩
trans
{f g h} := by
intro ⟨W₁, hW₁, hW₁l, hW₁r, e₁⟩ ⟨W₂, hW₂, hW₂l, hW₂r, e₂⟩
refine ⟨W₁ ⊓ W₂, hW₁.inter_of_isOpen_left hW₂ W₁.2, inf_le_left.trans hW₁l, inf_le_right.trans hW₂r, ?_⟩
dsimp at e₁ e₂
simp only [restrict_domain, restrict_hom, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_left hW₁l, Category.assoc, e₁,
← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_right hW₂r, ← e₂]
simp only [homOfLE_homOfLE_assoc]
