[Merged by Bors] - feat: generalize sheaf condition to only the relevant pullbacks existing

[dagurtomas]

We define a predicate Presieve.hasPullbacks which says that the pullback of every pair of arrows in the presieve exists. This allows to generalize Equalizer.Presieve.sheaf_condition to categories that don't necessarily have all pullbacks (such as Stonean).

Co-authored-by: Riccardo Brasca @riccardobrasca riccardo.brasca@gmail.com
Co-authored-by: Filippo A E Nuccio @faenuccio filippo.nuccio@univ-st-etienne.fr

---

[dagurtomas]

Presieve.hasPullbacks was https://github.com/adamtopaz/CopenhagenMasterclass2023/blob/master/Sieves/isSheafForPullbackSieve.lean#L13-L15

[dagurtomas]

Instead of doing all the primed versions of the definitions and theorems in the Copenhagen repo, I provided an instance [R.hasPullbacks] given [HasPullbacks C] and generalized the existing versions.

[dagurtomas]

It's a bit annoying that Lean doesn't automatically find an instance for HasPullback f g given (hf : R f), (hg : R g) and [R.hasPullbacks]. Is there a way to fix this?

[dagurtomas]

It's a bit annoying that Lean doesn't automatically find an instance for HasPullback f g given (hf : R f), (hg : R g) and [R.hasPullbacks]. Is there a way to fix this?

And now the linter complains that there are unnecessary have statements...

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style