mathlib

54315218 - refactor(topology/sheaves/sheaf_condition): Generalize unique gluing API (#9002)

refactor(topology/sheaves/sheaf_condition): Generalize unique gluing API (#9002) Previously, the sheaf condition in terms of unique gluings has been defined only for type-valued presheaves. This PR generalizes this to arbitrary concrete categories, whose forgetful functor preserves limits and reflects isomorphisms (e.g. algebraic categories like `CommRing`). As a side effect, this solves a TODO in `structure_sheaf.lean`. Co-authored-by: Johan Commelin <johan@commelin.net>