English
For a presieve R with grothendieck topology membership, there is an equivalence between IsLimit for the opensLeCover cocone and IsLimit for the sieve generated by R.
Русский
Для пресивея R с принадлежностью к топологии Гротендий существуют эквивалентности между предельностями для кокона opensLeCover и для порождаемого решеткой пучка.
LaTeX
$$\\[ IsLimit( F.mapCone( opensLeCoverCocone Y R ).op ) \\equiv IsLimit( F.mapCone ( Sieve.generate R ).arrows.cocone.op ) \]$$
Lean4
/-- Given a presheaf `F` on the topological space `X` and a family of opens `U` of `X`,
the natural cone associated to `F` and `U` used in the definition of
`F.IsSheafOpensLeCover` is a limit cone iff the natural cone associated to `F`
and the sieve generated by the presieve associated to `U` is a limit cone. -/
def isLimitOpensLeEquivGenerate₁ (hY : Y = iSup U) :
IsLimit (F.mapCone (opensLeCoverCocone U).op) ≃
IsLimit (F.mapCone (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op) :=
(IsLimit.whiskerEquivalenceEquiv (generateEquivalenceOpensLe U hY).op).trans
(IsLimit.equivIsoLimit (whiskerIsoMapGenerateCocone F U hY))
