Commit 2023-04-27 23:33 4e9ad32a

View on Github →

feat : port CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (#3605) This was harder than it looked (the proofs are long and broke).

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

added theorem CategoryTheory.Limits.colimitLimitToLimitColimit_injective

added theorem CategoryTheory.Limits.colimitLimitToLimitColimit_surjective

added theorem CategoryTheory.Limits.comp_lim_obj_ext

added theorem CategoryTheory.Limits.ι_colimitLimitIso_limit_π

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean