English
The sheaf condition for a singleton sieve is equivalent to the associated fork being a limit.
Русский
Условие сшиваемости для единичной сита эквивалентно тому, что соответствующая вилка является пределом.
LaTeX
$$$\text{Presieve.IsSheafFor } F (.singleton f) \iff \exists \! IsLimit (Fork.ofι (F.map f.op) (pullback.fst.op) (pullback.snd.op) (proof))$$$
Lean4
/-- The sheaf condition for a single morphism is the same as the canonical fork diagram being
limiting. -/
theorem isSheafFor_singleton_iff {F : Cᵒᵖ ⥤ Type*} {X Y : C} {f : X ⟶ Y} (c : PullbackCone f f) (hc : IsLimit c) :
Presieve.IsSheafFor F (.singleton f) ↔
Nonempty
(IsLimit
(Fork.ofι (F.map f.op) (f := F.map c.fst.op) (g := F.map c.snd.op)
(by simp [← Functor.map_comp, ← op_comp, c.condition]))) :=
by
have h (x : F.obj (op X)) :
(∀ {Z : C} (p₁ p₂ : Z ⟶ X), p₁ ≫ f = p₂ ≫ f → F.map p₁.op x = F.map p₂.op x) ↔
F.map c.fst.op x = F.map c.snd.op x :=
by
refine ⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩
rw [← PullbackCone.IsLimit.lift_fst hc _ _ h, op_comp, FunctorToTypes.map_comp_apply, H]
simp [← FunctorToTypes.map_comp_apply, ← op_comp]
rw [Types.type_equalizer_iff_unique, Presieve.isSheafFor_singleton]
simp_rw [h]
