English
Let X be an object of a category and Y an object of the over category over X. A sieve S on Y belongs to the Grothendieck topology J over X if and only if the corresponding sieve on Y.left, obtained by transporting S along the standard equivalence between over(X) and the left slice over X, belongs to J on Y.left.
Русский
Пусть X — объект категории, Y — объект в категории над X. Любая сетка S на Y принадлежит топологии Гротендика J над X тогда и только тогда, когда соответствующая сетка S на Y.left, полученная через стандартное эквивалентное отображение между Over(X) и Left, принадлежит J на Y.left.
LaTeX
$$$\\forall X\\,\\forall Y:\\mathrm{Over}\\,X\\,\\forall S:\\mathrm{Sieve}\\,Y:\\; S\\in (J.\\mathrm{over}\\,X)\\,Y \\iff \\mathrm{Sieve}.\\mathrm{overEquiv}\\ _\\,S\\in J\\,Y.\\mathrm{left}$$$
Lean4
theorem mem_over_iff {X : C} {Y : Over X} (S : Sieve Y) : S ∈ (J.over X) Y ↔ Sieve.overEquiv _ S ∈ J Y.left := by rfl
