feat(Algebra/Category/Ring/Colimits): category of (possibly non-commutative ring) has colimits

[jjaassoonn]

We already have that category of commutative rings has colimits, the same construction works for category of rings.

---

[github-actions[bot]]

PR summary a8d9b6c464

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ColimitType + ColimitType.AddGroup + ColimitType.AddGroupWithOne + ColimitType.instAdd + ColimitType.instNeg + ColimitType.instZero + InhabitedColimitType + Prequotient + Relation + coconeFun + coconeMorphism + cocone_naturality + cocone_naturality_components + colimit + colimitCocone + colimitIsColimit + colimitSetoid + descFun + descFunLift + descMorphism + hasColimits_ringCat + instance : Inhabited (Prequotient F) + instance : Ring (ColimitType.{v} F) + quot_add + quot_mul + quot_neg + quot_one + quot_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[erdOne]

If it is the same construction, can you show that CommRingCat => RingCat creates all colimits?

[jjaassoonn]

If it is the same construction, can you show that CommRingCat => RingCat creates all colimits?

I just realized I don't understand the maths proof: We need that the colimit of commutative ring viewed as objects of RingCat is still a commutative ring. I am not sure if this true in general. The colimit in RingCat is obtained by quotienting a relation that doesn't mention commutativity anywhere.

[erdOne]

Ah yes you are right. maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[kim-em]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style