Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-11 18:59 5c323cdc

View on Github →

feat(category_theory): over and under categories (#549)

Estimated changes

Modified category_theory/comma.lean

modified theorem category_theory.comma.map_right_obj_hom

added theorem category_theory.over.comp_left

added def category_theory.over.forget

added theorem category_theory.over.forget_map

added theorem category_theory.over.forget_obj

added def category_theory.over.hom_mk

added theorem category_theory.over.hom_mk_left

added theorem category_theory.over.id_left

added def category_theory.over.map

added theorem category_theory.over.map_map_left

added theorem category_theory.over.map_obj_hom

added theorem category_theory.over.map_obj_left

added def category_theory.over.mk

added theorem category_theory.over.mk_hom

added theorem category_theory.over.mk_left

added theorem category_theory.over.over_morphism.ext

added theorem category_theory.over.over_morphism_right

added theorem category_theory.over.over_right

added def category_theory.over.post

added theorem category_theory.over.w

added def category_theory.over

added theorem category_theory.under.comp_right

added def category_theory.under.forget

added theorem category_theory.under.forget_map

added theorem category_theory.under.forget_obj

added def category_theory.under.hom_mk

added theorem category_theory.under.hom_mk_right

added theorem category_theory.under.id_right

added def category_theory.under.map

added theorem category_theory.under.map_map_right

added theorem category_theory.under.map_obj_hom

added theorem category_theory.under.map_obj_right

added def category_theory.under.mk

added theorem category_theory.under.mk_hom

added theorem category_theory.under.mk_right

added def category_theory.under.post

added theorem category_theory.under.under_left

added theorem category_theory.under.under_morphism.ext

added theorem category_theory.under.under_morphism_left

added theorem category_theory.under.w

added def category_theory.under

Created category_theory/limits/over.lean

added def category_theory.functor.to_cocone

added theorem category_theory.functor.to_cocone_X

added theorem category_theory.functor.to_cocone_ι

added def category_theory.functor.to_cone

added theorem category_theory.functor.to_cone_X

added theorem category_theory.functor.to_cone_π

added def category_theory.over.colimit

added theorem category_theory.over.colimit_X_hom

added theorem category_theory.over.colimit_ι_app

added def category_theory.over.forget_colimit_is_colimit

added def category_theory.under.forget_limit_is_limit

added def category_theory.under.limit

added theorem category_theory.under.limit_X_hom

added theorem category_theory.under.limit_π_app