Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 15:03 0e1387bb

View on Github →

feat(category_theory): the category of small categories has all small limits (#12979)

Estimated changes

Modified src/category_theory/category/Cat.lean

added theorem category_theory.Cat.comp_map

added theorem category_theory.Cat.comp_obj

added theorem category_theory.Cat.id_map

Created src/category_theory/category/Cat/limit.lean

added def category_theory.Cat.has_limits.hom_diagram

added def category_theory.Cat.has_limits.limit_cone

added def category_theory.Cat.has_limits.limit_cone_X

added def category_theory.Cat.has_limits.limit_cone_is_limit

added def category_theory.Cat.has_limits.limit_cone_lift

added theorem category_theory.Cat.has_limits.limit_π_hom_diagram_eq_to_hom

Modified src/category_theory/grothendieck.lean