Commit 2020-09-19 19:03 02b492ab

View on Github →

feat(category_theory/Mon): Mon_ C has limits when C does (#4133) If C has limits, so does Mon_ C. (This could potentially replace many individual constructions for concrete categories, in particular Mon, SemiRing, Ring, and Algebra R.)

Estimated changes

Modified src/category_theory/functorial.lean

added theorem category_theory.functorial.map_comp

added theorem category_theory.functorial.map_id

added theorem category_theory.map_as_map

Modified src/category_theory/monoidal/functorial.lean

Modified src/category_theory/monoidal/internal.lean

Modified src/category_theory/monoidal/internal/Module.lean

Modified src/category_theory/monoidal/internal/functor_category.lean

Created src/category_theory/monoidal/internal/limits.lean

added def Mon_.forget_map_cone_limit_cone_iso

added def Mon_.limit

added def Mon_.limit_cone

added def Mon_.limit_cone_is_limit

Modified src/category_theory/monoidal/limits.lean

added theorem category_theory.limits.lim_lax_ε

added theorem category_theory.limits.lim_lax_μ