feat(category_theory/limits/shapes/diagonal): The diagonal object of a morphism.

[erdOne]

---

[b-mehta]

Does this relate to any of the things about kernel pairs that we already have?

[erdOne]

Since this file mainly focuses on the diagonal morphism Δ_{X/Y} ⟶ X, there was only one lemma that I was able to generalize in terms of kernel pairs.

[jcommelin]

Thanks :tada:

bors merge

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Build failed (retrying...):

• Build mathlib
• Lint mathlib
• Run tests

[jcommelin]

bors merge p=4

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[erdOne]

bors cancel

[bors[bot]]

Canceled.

[jcommelin]

bors merge p=0

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests