mathlib3

8b277a95 - feat(category_theory/filtered): finite diagrams in filtered categories admit cocones (#4026)

feat(category_theory/filtered): finite diagrams in filtered categories admit cocones (#4026) This is only step towards eventual results about filtered colimits commuting with finite limits, `forget CommRing` preserving filtered colimits, and applications to `Scheme`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>