Markus Himmel

feat(category_theory): compute subobjects of structured arrows

1

One step closer to the Special Adjoint Functor Theorem. --- - [x] depends on: #15494 - [ ] depends on: #16050 [](https://gitpod.io/from-referrer/)

--- Split off from #15912 to reduce merge conflicts with a future PR. [](https://gitpod.io/from-referrer/)

--- [](https://gitpod.io/from-referrer/)

feat(category_theory/limits): has_limits_of_shape J if and only if const J is a left adjoint

1

--- - [x] depends on: #15796 - [x] depends on: #15797 - [x] depends on: #15858 [](https://gitpod.io/from-referrer/)

feat(category_theory/adjunction): complete well-powered category with a coseparating set is cocomplete

1

This corollary of the special adjoint functor theorem immediately implies that Grothendieck categories are complete, which, according to the Wikipedia article on Grothendieck categories, is "a rather deep result". ---...

feat(algebra/category): forgetful functors from modules/abelian groups preserve epis/monos

1

The corresponding `reflects` statements already follow from faithfulness. --- - [x] depends on: #14829 - [x] depends on: #15107 [](https://gitpod.io/from-referrer/)

feat(category_theory/preadditive): inclusion functor from left exact functors to additive functors

1

--- - [x] depends on: #12014 - [x] depends on: #12330 - [x] depends on: #12336 [](https://gitpod.io/from-referrer/)

feat: unbundle array size constraint from hash map bucket array

3

This PR makes sure that the positivity checker is happy with the following construction: ```lean inductive ContainsItselfInHashMapValues where | base | recursive (l : HashMap.Imp Bool ContainsItselfInHashMapValues) ``` Users actually...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...