English
The isSheaf_iff_isSheaf_of_type theorem states that for presheaves valued in Type, the sheaf condition is equivalent to the sieve-based notion.
Русский
Теорема isSheaf_iff_isSheaf_of_type утверждает, что для прешейфов, значащихся в Type, условие шейфа эквивалентно основанному на сиде концепту шейфа.
LaTeX
$$$\\mathrm{IsSheaf}\\; J\\; P \\iff \\mathrm{Presieve.IsSheaf}(J)\\; P$ для P : C^{op} \\to \\mathrm{Type}.$$$
Lean4
theorem isSheaf_iff_isSheaf_of_type (P : Cᵒᵖ ⥤ Type w) : Presheaf.IsSheaf J P ↔ Presieve.IsSheaf J P :=
by
constructor
· intro hP
refine Presieve.isSheaf_iso J ?_ (hP PUnit)
exact Functor.isoWhiskerLeft _ Coyoneda.punitIso ≪≫ P.rightUnitor
· intro hP X Y S hS z hz
refine ⟨fun x => (hP S hS).amalgamate (fun Z f hf => z f hf x) ?_, ?_, ?_⟩
· intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h
exact congr_fun (hz g₁ g₂ hf₁ hf₂ h) x
· intro Z f hf
funext x
apply Presieve.IsSheafFor.valid_glue
· intro y hy
funext x
apply (hP S hS).isSeparatedFor.ext
intro Y' f hf
rw [Presieve.IsSheafFor.valid_glue _ _ _ hf, ← hy _ hf]
rfl
