fix(category_theory/limits): Add some missing instances for special shapes of limits

[TwoFX]

This PR adds fin_category instances for the indexing categories for (co)equalizers, pushouts and pullbacks. This means that we can now correctly derive the existence of these special limits from has_finite_limits and has_finite_colimits.

It also adds missing instance attributes for has_kernels and has_cokernels.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[semorrison]

Why is _root_ needed here?

[TwoFX]

After open walking_parallel_pair, decidable_eq refers to category_theory.limits.walking_parallel_pair.decidable_eq (i.e., the decidable_eq instance derived for walking_parallel_pair).

[semorrison]

Discussed here, and a fix is in the works, so we'll leave this as is for now.

[semorrison]

I would really prefer to see a derive handler that can cope with this. Do you know why the existing one doesn't work here? (I haven't looked at all.)

[TwoFX]

When I put attribute [derive fintype] walking_parallel_pair_hom, I get failed to find a derive handler for 'fintype'. Since even for object types like walking_parallel_pair the fintype instance is implemented manually, I concluded that there simply is no derive handler for fintype. A grep over the mathlib repository seems to support that conclusion.

[semorrison]

It seems the only other successful @[derive fintype] is in archive/sensitivity.lean, where delta_instance is all that's required to get it done. A general purpose derive_handler for fintype unfortunately doesn't exist, but this seems like the sort of thing @cipher1024 likes. :-)

[semorrison]

So what's the status of

This means that we can now correctly derive the existence of these special limits from has_finite_limits and has_finite_colimits.

What do you think of adding a bunch of lines like:

def has_equalizers_of_has_finite_limits [has_finite_limits.{v} C] : has_equalizers.{v} C :=
{ has_limits_of_shape := by apply_instance }

These shouldn't be global instances, but available in case someone wants them.