Commit 2023-05-24 22:02 cc66f52f

View on Github →

feat: port Algebra.Category.Module.Limits (#4297)

Estimated changes

Modified Mathlib.lean

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

added theorem ModuleCat.forget_map

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

added def ModuleCat.HasLimits.limitCone

added def ModuleCat.HasLimits.limitConeIsLimit

added def ModuleCat.directLimitCocone

added def ModuleCat.directLimitDiagram

added def ModuleCat.directLimitIsColimit

added def ModuleCat.forget₂AddCommGroupPreservesLimitsAux

added theorem ModuleCat.hasLimitsOfSize

added def ModuleCat.limitπLinearMap

added def ModuleCat.sectionsSubmodule