English
For a singleton sieve on f: X → Y, IsSheafFor P is characterized by a compatibility condition on all Z, plus existence/uniqueness of a Y-element y with P.map f^op y = x.
Русский
Для одиночной решётки на f: X → Y IsSheafFor P характеризуется совместимостью на всех Z и существованием уникального элемента y в P(Y), такого что P.map f^op y = x.
LaTeX
$$$\text{IsSheafFor}(P, \{f\}) \iff \forall x: P(X), (\forall Z, p_1,p_2: Z→X, p_1 f = p_2 f → P.map p_1^op x = P.map p_2^op x) → ∃! y, P.map f^op y = x$$$
Lean4
theorem isSheafFor_singleton {X Y : C} {f : X ⟶ Y} :
Presieve.IsSheafFor P (.singleton f) ↔
∀ (x : P.obj (op X)),
(∀ {Z : C} (p₁ p₂ : Z ⟶ X), p₁ ≫ f = p₂ ≫ f → P.map p₁.op x = P.map p₂.op x) → ∃! y, P.map f.op y = x :=
by
rw [IsSheafFor, Equiv.forall_congr_left (Presieve.FamilyOfElements.singletonEquiv P f)]
simp_rw [FamilyOfElements.compatible_singleton_iff, FamilyOfElements.isAmalgamation_singleton_iff,
FamilyOfElements.singletonEquiv_symm_apply_self]
