[Merged by Bors] - feat(category_theory): wide pullbacks and limits in the over category

[b-mehta]

This PR introduces wide pullbacks.
Ordinary pullbacks are then defined as a special case of wide pullbacks, which simplifies some of the definitions and proofs there.
Finally we show that the existence of wide pullbacks in C gives products in the slice C/B, and in fact gives all limits.

TO CONTRIBUTORS:

This PR may break some downstream code using pullbacks, but only slightly (as can be seen in pullbacks.lean). In particular, the only thing that used to work that doesn't any more would be applying cases to a walking_cospan - but thanks to the super helpful pullback_cone.is_limit.mk and pullback_cone.equalizer_ext, one shouldn't need to take cases on a walking_cospan anyway.

I haven't done the dual construction - of course before this PR is merged it should probably be included.

The new proof would of course follow by not changing the definition of pullback the same and showing an equivalence of categories between wide_pullback_shape walking_pair and walking_cospan, but since the change does simplify some proofs I've kept it for now.

The docs linter complains about

abbreviation walking_cospan.left : walking_cospan := some walking_pair.left
abbreviation walking_cospan.right : walking_cospan := some walking_pair.right
abbreviation walking_cospan.one : walking_cospan := none

and I'd appreciate suggestions of what sort of docs would be helpful here.

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

For reviewers: code review check list

If you're confused by comments on your PR like bors r+ or bors d+, please see our notes on bors for information on our merging workflow.

[semorrison]

Regarding how to document the abbreviation, just write something

/-- The left point of the walking cospan. -/
abbreviation walking_cospan.left : walking_cospan := some walking_pair.left

[semorrison]

Do you think you could add some larger scale documentation, in the module doc-strings in these files, explaining the motivation for introducing wide pullbacks in the first place:

• That/if they actually make life easier talking about binary pullbacks?
• Constructing arbitrary limits in slice categories.

[b-mehta]

I mentioned this linter warning on zulip here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Linter.20rejects.20automatic.20instance - not sure how to fix this.

[semorrison]

Okay, I think I'm happy with this. Do you want to add the dual statements to this PR?

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib