Commit 2023-06-11 13:19 45f44831

View on Github →

Port/Algebra.Category.Module.FilteredColimits (#4949)

Estimated changes

Modified Mathlib.lean

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

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

added theorem ModuleCat.FilteredColimits.M.mk_eq

added def ModuleCat.FilteredColimits.coconeMorphism

added def ModuleCat.FilteredColimits.colimit

added def ModuleCat.FilteredColimits.colimitCocone

added def ModuleCat.FilteredColimits.colimitCoconeIsColimit

added def ModuleCat.FilteredColimits.colimitDesc

added def ModuleCat.FilteredColimits.colimitSmulAux

added theorem ModuleCat.FilteredColimits.colimitSmulAux_eq_of_rel

added theorem ModuleCat.FilteredColimits.colimit_smul_mk_eq

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

modified def CategoryTheory.HasForget₂.mk'

modified def CategoryTheory.forget₂

modified def CategoryTheory.hasForgetToType