Commit 2021-09-07 00:33 54315218

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.