Commit 2021-09-26 21:40 996783ce

feat(topology/sheaves/stalks): Generalize from Type to algebraic categories (#9357) Previously, basic lemmas about stalks like germ_exist and section_ext were only available for Type-valued (pre)sheaves. This PR generalizes these to (pre)sheaves valued in any concrete category where the forgetful functor preserves filtered colimits, which includes most algebraic categories like Group and CommRing. For the statements about stalks maps, we additionally assume that the forgetful functor reflects isomorphisms and preserves limits.