English
For a presieve of arrows, being a sheaf for P is equivalent to a compatibility condition and the existence/uniqueness of a glueing element t with images matching the x_i.
Русский
Для пресивы стрелок Being a sheaf for P эквивалентно условию совместимости и существованию единственного клея t, удовлетворяющего требованию совпадения изображений x_i.
LaTeX
$$$(\text{ofArrows } X \; \pi).IsSheafFor(P) \iff (\forall x, \text{Compatible } P \pi x \Rightarrow \exists! t, \forall i, P.map(\pi_i).op t = x_i)$$$
Lean4
theorem isSheafFor_arrows_iff :
(ofArrows X π).IsSheafFor P ↔
(∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ i, P.map (π i).op t = x i) :=
by
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
· obtain ⟨t, ht₁, ht₂⟩ := h _ hx.familyOfElements_compatible
refine ⟨t, fun i ↦ ?_, fun t' ht' ↦ ht₂ _ fun _ _ ⟨i⟩ ↦ ?_⟩
· rw [ht₁ _ (ofArrows.mk i), hx.familyOfElements_ofArrows_mk]
· rw [ht', hx.familyOfElements_ofArrows_mk]
· obtain ⟨t, hA, ht⟩ :=
h (fun i ↦ x (π i) (ofArrows.mk _)) (fun i j Z gi gj ↦ hx gi gj (ofArrows.mk _) (ofArrows.mk _))
exact ⟨t, fun Y f ⟨i⟩ ↦ hA i, fun y hy ↦ ht y (fun i ↦ hy (π i) (ofArrows.mk _))⟩
