English
A multifork construction is used to relate cones over diagrams of sheaves to cones over the underlying presheaf objects via evaluation.
Русский
Мультифорковая конструкция связывает конусы над диаграммами шейфов с конусами над несущими объектами пресшофа через оценку.
LaTeX
$$$ \\text{multiforkEvaluationCone} (F,E,X,W) : \\text{Cone}(F \\circ sheafToPresheaf J D \\circ (evaluation X)) $$$
Lean4
/-- An auxiliary definition to be used below.
Whenever `E` is a cone of shape `K` of sheaves, and `S` is the multifork associated to a
covering `W` of an object `X`, with respect to the cone point `E.X`, this provides a cone of
shape `K` of objects in `D`, with cone point `S.X`.
See `isLimitMultiforkOfIsLimit` for more on how this definition is used.
-/
def multiforkEvaluationCone (F : K ⥤ Sheaf J D) (E : Cone (F ⋙ sheafToPresheaf J D)) (X : C) (W : J.Cover X)
(S : Multifork (W.index E.pt)) : Cone (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X))
where
pt := S.pt
π :=
{ app := fun k =>
(Presheaf.isLimitOfIsSheaf J (F.obj k).1 W (F.obj k).2).lift <|
Multifork.ofι _ S.pt (fun i => S.ι i ≫ (E.π.app k).app (op i.Y))
(by
intro i
simp only [Category.assoc]
erw [← (E.π.app k).naturality, ← (E.π.app k).naturality]
dsimp
simp only [← Category.assoc]
congr 1
apply S.condition)
naturality := by
intro i j f
dsimp [Presheaf.isLimitOfIsSheaf]
rw [Category.id_comp]
apply Presheaf.IsSheaf.hom_ext (F.obj j).2 W
intro ii
rw [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← (F.map f).val.naturality, ← Category.assoc,
Presheaf.IsSheaf.amalgamate_map]
dsimp [Multifork.ofι]
erw [Category.assoc, ← E.w f]
cat_disch }
