Commit 2024-07-15 21:28 dccac13c

View on Github →

feat(Algebra/Category/Ring/Colimits): category of (possibly non-commutative ring) has colimits (#14413) We already have that category of commutative rings has colimits, the same construction works for category of rings.

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Colimits.lean

added def RingCat.Colimits.ColimitType

added inductive RingCat.Colimits.Prequotient

added inductive RingCat.Colimits.Relation

added def RingCat.Colimits.coconeFun

added def RingCat.Colimits.coconeMorphism

added theorem RingCat.Colimits.cocone_naturality

added theorem RingCat.Colimits.cocone_naturality_components

added def RingCat.Colimits.colimit

added def RingCat.Colimits.colimitCocone

added def RingCat.Colimits.colimitIsColimit

added def RingCat.Colimits.colimitSetoid

added def RingCat.Colimits.descFun

added def RingCat.Colimits.descFunLift

added def RingCat.Colimits.descMorphism

added theorem RingCat.Colimits.quot_add

added theorem RingCat.Colimits.quot_mul

added theorem RingCat.Colimits.quot_neg

added theorem RingCat.Colimits.quot_one

added theorem RingCat.Colimits.quot_zero