Commit 2023-06-06 14:18 0a8cda96

View on Github →

feat: port Algebra.Category.Module.Colimits (#4282)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Abelian.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

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

added def ModuleCat.Colimits.ColimitType.mk

added def ModuleCat.Colimits.ColimitType

added inductive ModuleCat.Colimits.Prequotient

added inductive ModuleCat.Colimits.Relation

added def ModuleCat.Colimits.coconeFun

added def ModuleCat.Colimits.coconeMorphism

added theorem ModuleCat.Colimits.cocone_naturality

added theorem ModuleCat.Colimits.cocone_naturality_components

added def ModuleCat.Colimits.colimit

added def ModuleCat.Colimits.colimitCocone

added def ModuleCat.Colimits.colimitCoconeIsColimit

added def ModuleCat.Colimits.colimitSetoid

added def ModuleCat.Colimits.descFun

added def ModuleCat.Colimits.descFunLift

added def ModuleCat.Colimits.descMorphism

added theorem ModuleCat.Colimits.quot_add

added theorem ModuleCat.Colimits.quot_neg

added theorem ModuleCat.Colimits.quot_smul

added theorem ModuleCat.Colimits.quot_zero

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean

modified def ModuleCat.HasLimits.limitCone

modified def ModuleCat.HasLimits.limitConeIsLimit

modified def ModuleCat.forget₂AddCommGroupPreservesLimitsAux

modified theorem ModuleCat.hasLimitsOfSize

modified def ModuleCat.limitπLinearMap

modified def ModuleCat.sectionsSubmodule