English
There is a natural correspondence between cones over the diagram S.arrows.diagram.op ⋙ P and sieve-compatible families of elements of P with respect to S, parameterized by E.
Русский
Существует естественное соответствие между конусами над диаграммой S.arrows.diagram.op ⋙ P и семействами элементов, совместимыми с решетом, относительно S.
LaTeX
$$$(S.arrows.diagram.op ⋙ P).cones.obj E \\cong {x : \\mathrm{FamilyOfElements}(P \\circ coyoneda^{\\mathrm{op}} E)(S) \\,\\vert\\ x.SieveCompatible}$$$
Lean4
/-- Cone morphisms from the cone corresponding to a sieve_compatible family to the natural
cone associated to a sieve `S` and a presheaf `P` are in 1-1 correspondence with amalgamations
of the family. -/
def homEquivAmalgamation : (hx.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // x.IsAmalgamation t }
where
toFun l := ⟨l.hom, fun _ f hf => l.w (op ⟨Over.mk f, hf⟩)⟩
invFun t := ⟨t.1, fun f => t.2 f.unop.1.hom f.unop.2⟩
