Commit 2022-11-09 03:23 85d6221dView on Github →
refactor(topology/sheaf_condition): remove redundant constructions (#17378)
The constructions used to prove
is_sheaf_iff_is_sheaf_equalizer_products in sites.lean is redundant because the equivalence can now be achieved via
is_sheaf (site version) ↔ opens_le_cover ↔ pairwise_intersections ↔ equalizer_products. Refactoring the proof of this equivalence after removal of these constructions, however, requires rearranging the import chain and moving things around, explaining the large diff.
The author @justus-springer of the constructions has previously approved the removal in #11706.
The universe levels in equalizer_products.lean are also fixed and generalized (a cover of a space should be indexed by a type in the same universe), leading to the addition of a few universe ascriptions.
- depends on: #17361