Presieve: set or predicate?

Stream: mathlib4

[Yury G. Kudryashov]

The next one is docs#CategoryTheory.Presieve. It's defined using Set, then most of the file treats it as a predicate. @Bhavik Mehta @Edward Ayers should I change the definition or the lemmas?

[Bhavik Mehta]

I think the lemmas should be changed, my opinion is that we should be using \in throughout; the original version of the PR adding that used \in but it was changed based on review comments at the time. If I remember correctly, there was some other improvement that was suggested which broke the set notation. I'd hope that these days we can recover the set way of thinking about sieves without losing the other benefits (eg SetLike didn't exist back then!)

[Yury G. Kudryashov]

OK, I'll fix it and ask you to review the PR.

[Yury G. Kudryashov]

Note that I may fail to have Y implicit.

[Bhavik Mehta]

For me, that's okay, and matches what's done on paper. But folks like @Joël Riou and @Christian Merten work on these more than me recently so I'd like to hear their opinion too.

[Joël Riou]

Bhavik Mehta said:

For me, that's okay, and matches what's done on paper. But folks like Joël Riou and Christian Merten work on these more than me recently so I'd like to hear their opinion too.

For related definitons ObjectProperty/MorphismProperty, we use predicates (and #30269 refactors parts of mathlib where Set was used). Here, I would prefer we use Prop rather than Set in the definition of presieves: this is the way we have been using the API, and basically only the definition would have to be changed.

[Yury G. Kudryashov]

I'll wait for you to agree on this.

[Yury G. Kudryashov]

#35799 redefines Presieve using predicates. @Joël Riou Could you please fix the docstrings?

[Christian Merten]

Yury G. Kudryashov said:

#35799 redefines Presieve using predicates. Joël Riou Could you please fix the docstrings?

Fixed the docstrings.

[Yury G. Kudryashov]

@Joël Riou Related question: should docs#GrothendieckTopology.sieves be a family of sets or a family of predicates? It's defined as a family of sets, then many constructors give a family of predicates.

[Joël Riou]

I would think we got used to writing _ ∈ J X for Grothendieck topologies/(pre)coverages. We should probably insert a certain number of setOf in the constructors (this may have been overlooked when we started to chase the defeq abuse between Set and predicates some time ago). Still, I think @Christian Merten should make the decision as he has been the main developer on this part of mathlib.

[Yury G. Kudryashov]

One more data point: docs#CategoryTheory.Sieve.generateSingleton and other definitions in that file use setOf to construct Presieves. I'll move this discussion to a new thread.

[Christian Merten]

Joël Riou said:

I would think we got used to writing _ ∈ J X for Grothendieck topologies/(pre)coverages. We should probably insert a certain number of setOf in the constructors (this may have been overlooked when we started to chase the defeq abuse between Set and predicates some time ago). Still, I think Christian Merten should make the decision as he has been the main developer on this part of mathlib.

I agree, I strongly prefer keeping _ ∈ J X and there should be less issues with this than with presieves where there is an implicit argument which gets in the way.

[Yury G. Kudryashov]

So, I should use setOf for docs#GrothendieckTopology.sieves, but I should change docs#CategoryTheory.Sieve.generateSingleton etc in the opposite direction, right?

[Christian Merten]

Yes, exactly.