mathlib

996783ce - feat(topology/sheaves/stalks): Generalize from Type to algebraic categories (#9357)

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.