Def category_theory.sites.pullback_pushforward_adjunction

Modification history

2023-03-08 09:51
src/category_theory/sites/cover_preserving.lean
chore(category_theory/sites/pushforward): move pushforwards to own file to reduce imports (#18561) …
Modified category_theory.sites.pullback_pushforward_adjunctionView on Github →
2022-01-06 10:39
src/category_theory/sites/cover_preserving.lean
feat(category_theory/sites): The pushforward pullback adjunction (#11273)
Added category_theory.sites.pullback_pushforward_adjunctionView on Github →