Mathlib Changelog
v3
Changelog
About
Github
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