mathlib

68060507 - feat(category_theory/sites/adjunction): Adjunctions between categories of sheaves. (#10541)

feat(category_theory/sites/adjunction): Adjunctions between categories of sheaves. (#10541) We construct adjunctions between categories of sheaves obtained by composition (and sheafification) with functors which form a given adjunction. Will be used in LTE. Co-authored-by: Johan Commelin <johan@commelin.net>