Commit 2025-01-02 12:06 5d3e2fcb

feat(CategoryTheory/Sites): helper definitions for sieves (#19517) For (pre)sieves constructed with bind, we introduce a structure BindStruct which contains the data and properties we may get when a morphism belongs to Presieve.bind S R. Similarly, we introduce definitions and lemmas Sieve.ofArrows.i, Sieve.ofArrows.h, Sieve.ofArrows.fac which provide a choice of factorization of a morphism which belong to a sieve generated by a family of arrows. This shall be necessary in #19444 as we sometimes need to choose such data in order to perform some other constructions.