Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 08:10 6a6b4d05

View on Github →

feat(category_theory/sites/*): Cover-lifting functors on sites (#9431) This PR defines cover-liftings functors between sites, and proves that Ran F.op maps sheaves to sheaves for cover-lifting functors F. This will probably be needed when we want to glue B-sheaves into sheaves.

Estimated changes