feat(CategoryTheory): define descent data by presieves

[yuma-mizuno]

---

Addendum: I realized that there is prior work in #24434. Since this PR uses a slightly different definition, I plan to make this PR a follow-up to #24434. Until then, I’ll keep it marked as WIP. See the comment: #29638 (comment)

[github-actions]

PR summary 6b2262238f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Stack.Descent (new file)	485
Mathlib.CategoryTheory.Stack.Basic (new file)	793

---

Declarations diff

+ DescentData
+ Hom
+ Hom.comp
+ Hom.id
+ IsStack
+ PreDescentData
+ associator_eqToIso
+ associator_hom
+ associator_inv
+ canonical
+ eq_eqToHom
+ homPreSheaf
+ instance : Category (DescentData S P)
+ leftUnitor_eqToIso
+ leftUnitor_hom
+ leftUnitor_inv
+ mapCompCat
+ mapComp_comp_left
+ mapComp_comp_left_inv
+ mapComp_comp_right
+ mapComp_comp_right_inv
+ mapComp_eq_left
+ mapComp_eq_right
+ mapIdCat
+ map₂_associator_inv
+ map₂_left_unitor_inv
+ map₂_right_unitor_inv
+ mkCat
+ mkFunctor
+ mkHom
+ rightUnitor_eqToIso
+ rightUnitor_hom
+ rightUnitor_inv

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[chrisflav]

Are you aware of #24434?

[yuma-mizuno]

I hadn’t noticed that. Thank you very much for pointing it out. I should wait for #24434. I’ve only worked on this for a few days, so I’m really glad I caught it now. And now I believe I can help with reviewing #24434.

It seems that there is a technical difference between describing descent data using a family of arrows versus using a presieve directly. These should correspond via Presieve.ofArrows. Since I believe both approaches have their own usefulness, I’d like to treat the descent data in this PR as an "another constructor" in the future, and make it a follow-up to #24434. Until then, I will keep this PR marked as WIP.

[yuma-mizuno]

Perhaps the biggest difference from #24434 is that there the conditions are given by "square diagrams", whereas here the conditions are given by "triangle diagrams" (simple compositions).

[joelriou]

I have added #30177 (prestacks) and #30189 (definition of the category of descent data for a family of morphisms).

[joelriou]

One very important difference with our work with @chrisflav is that we make no use of eqToIso. I introduced mapComp' to have a variant of mapComp where we do not assume compositions are definitional equalities. This makes proofs more straightforward (even though we both struggled to understand how to make this work!): compare https://github.com/yuma-mizuno/mathlib4/blob/e7081a45f2ab07cc5c6d7d62d54d22c868bc9d6b/Mathlib/CategoryTheory/Stack/Descent.lean#L127-L174 and
https://github.com/joelriou/mathlib4/blob/d552db644945825144e806d66d0e8658c0086afd/Mathlib/CategoryTheory/Sites/Descent/DescentData.lean#L119-L129
I believe that (pre)sieves should only appear in the definition of stacks, and the rest of the API should be about (covering) families of morphisms, because families of morphisms are more practical [especially for constructing data] (and a (pre)sieve is a particular case of a family of morphisms: any construction for families of morphisms applies in particular to presieves).
Note also that I have just shown the fact I had mentionned elsewhere that up to an equivalence DescentData only depends on the sieve that is generated by the family of morphisms: https://github.com/joelriou/mathlib4/blob/9d4550972bfb8464a2fcb05609ec971bcc910357/Mathlib/CategoryTheory/Sites/Descent/DescentData.lean#L319 #30190

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.