mathlib3

6756d47c - feat(category_theory): Mon_.forget reflects isos (#4131)

feat(category_theory): Mon_.forget reflects isos (#4131) A step along the way to `sheaf X (Mon_ C) ~ Mon_ (sheaf X C)`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>