Commit 2023-06-26 01:21 d93a0a4d

View on Github →

feat: port Algebra.Category.Mon.Colimits (#5466)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean

Created Mathlib/Algebra/Category/MonCat/Colimits.lean

added def MonCat.Colimits.ColimitType

added inductive MonCat.Colimits.Prequotient

added inductive MonCat.Colimits.Relation

added def MonCat.Colimits.coconeFun

added def MonCat.Colimits.coconeMorphism

added theorem MonCat.Colimits.cocone_naturality

added theorem MonCat.Colimits.cocone_naturality_components

added def MonCat.Colimits.colimit

added def MonCat.Colimits.colimitCocone

added def MonCat.Colimits.colimitIsColimit

added def MonCat.Colimits.colimitSetoid

added def MonCat.Colimits.descFun

added def MonCat.Colimits.descFunLift

added def MonCat.Colimits.descMorphism

added theorem MonCat.Colimits.quot_mul

added theorem MonCat.Colimits.quot_one

Renamed Mathlib/Algebra/Category/Mon/FilteredColimits.lean to Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean