Lean4
/-- If `E` is a cone of shape `K` of sheaves, which is a limit on the level of presheaves,
this definition shows that the limit presheaf satisfies the multifork variant of the sheaf
condition, at a given covering `W`.
This is used below in `isSheaf_of_isLimit` to show that the limit presheaf is indeed a sheaf.
-/
def isLimitMultiforkOfIsLimit (F : K ⥤ Sheaf J D) (E : Cone (F ⋙ sheafToPresheaf J D)) (hE : IsLimit E) (X : C)
(W : J.Cover X) : IsLimit (W.multifork E.pt) :=
Multifork.IsLimit.mk _
(fun S => (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift <| multiforkEvaluationCone F E X W S)
(by
intro S i
apply (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op i.Y)) hE).hom_ext
intro k
dsimp [Multifork.ofι]
erw [Category.assoc, (E.π.app k).naturality]
dsimp
rw [← Category.assoc]
erw [(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).fac (multiforkEvaluationCone F E X W S)]
dsimp [multiforkEvaluationCone, Presheaf.isLimitOfIsSheaf]
rw [Presheaf.IsSheaf.amalgamate_map]
rfl)
(by
intro S m hm
apply (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).hom_ext
intro k
dsimp
erw [(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).fac]
apply Presheaf.IsSheaf.hom_ext (F.obj k).2 W
intro i
dsimp only [multiforkEvaluationCone, Presheaf.isLimitOfIsSheaf]
rw [(F.obj k).cond.amalgamate_map]
dsimp [Multifork.ofι]
change _ = S.ι i ≫ _
erw [← hm, Category.assoc, ← (E.π.app k).naturality, Category.assoc]
rfl)
