English
Under HasMultiequalizer assumptions, IsSheaf J P is equivalent to IsIso of each S.toMultiequalizer P.
Русский
При предпосылках HasMultiequalizer равносильно IsSheaf J P то IsIso каждого S.toMultiequalizer P.
LaTeX
$$$\\text{IsSheaf } J P \\iff \\forall X,S,\\; \\text{IsIso}(S.toMultiequalizer P).$$$
Lean4
theorem isSheaf_iff_multifork : IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P)) :=
by
refine ⟨fun hP X S => ⟨isLimitOfIsSheaf _ _ _ hP⟩, ?_⟩
intro h E X S hS x hx
let T : J.Cover X := ⟨S, hS⟩
obtain ⟨hh⟩ := h _ T
let K : Multifork (T.index P) := Multifork.ofι _ E (fun I => x I.f I.hf) (fun I => hx _ _ _ _ I.r.w)
use hh.lift K
dsimp; constructor
· intro Y f hf
apply hh.fac K (WalkingMulticospan.left ⟨Y, f, hf⟩)
· intro e he
apply hh.uniq K
rintro (a | b)
· apply he
· rw [← K.w (WalkingMulticospan.Hom.fst b), ← (T.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]
congr 1
apply he
