mathlib
e2e38c00 - chore(category_theory/sites/pushforward): move pushforwards to own file to reduce imports (#18561)

Commit
2 years ago
chore(category_theory/sites/pushforward): move pushforwards to own file to reduce imports (#18561) We had unnecessarily dragged in the development of sheafification to material about [dense subsites](https://tqft.net/mathlib4/2023-03-08/category_theory.sites.dense_subsite.pdf). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading