feat(CategoryTheory/Sites): the topology is generated by 1-hypercovers

[joelriou]

trafficstars

In this PR, we show that a Grothendieck topology on a category C (with C : Type u and [Category.{v} C]) is (obviously) generated by 1-hypercovers of size max u v.

In order to facilitate this, the type Cover.Relation is repackaged in a slightly different manner. Some proofs have been cleaned up. Several dsimp lemmas which had been manually added have been removed (and replaced by auto-generated ones).

---

• [ ] depends on: #13004

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13004~~ By Dependent Issues (🤖). Happy coding!

[erdOne]

Is this ready for review?

[joelriou]

Is this ready for review?

Yes, now it is!

[github-actions[bot]]

PR summary

Import changes

No significant changes to the import graph

---

Declarations diff

+ Arrow.Relation + Arrow.Relation.base + Arrow.Relation.map + Arrow.precomp + Arrow.precompRelation + Relation.mk' + congr_apply + instance : IsGeneratedByOneHypercovers.{max u v} J + oneHypercover + preOneHypercover + preOneHypercover_sieve₀ + preOneHypercover_sieve₁ - Relation.base - Relation.base_fst - Relation.base_snd - Relation.fst - Relation.map - Relation.map_fst - Relation.map_snd - Relation.snd - multicospanComp_app_left - multicospanComp_app_right - multicospanComp_hom_app_left - multicospanComp_hom_app_right - multicospanComp_hom_inv_left - multicospanComp_hom_inv_right - multicospan_map_fst - multicospan_map_snd - multicospan_obj_left - multicospan_obj_right

You can run this locally as follows

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

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

[erdOne]

Am I correct that @dagurtomas thinks this is good to go?

[dagurtomas]

Yes, I think I already reviewed and approved?

[erdOne]

Okay just making sure. Thanks Joël and Dagur! maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style