Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-12-02 17:36
a5e2ebe9
View on Github →
feat(category_theory/limits/cones): (co)cones on a diagram
Estimated changes
Created
category_theory/limits/cones.lean
added
def
category_theory.functor.cocones
added
theorem
category_theory.functor.cocones_obj
added
def
category_theory.functor.cones
added
theorem
category_theory.functor.cones_obj
added
def
category_theory.functor.map_cocone
added
def
category_theory.functor.map_cocone_morphism
added
theorem
category_theory.functor.map_cocone_ι
added
def
category_theory.functor.map_cone
added
def
category_theory.functor.map_cone_morphism
added
theorem
category_theory.functor.map_cone_π
added
def
category_theory.limits.cocone.extend
added
def
category_theory.limits.cocone.extensions
added
def
category_theory.limits.cocone.precompose
added
theorem
category_theory.limits.cocone.w
added
def
category_theory.limits.cocone.whisker
added
theorem
category_theory.limits.cocone.whisker_ι_app
added
structure
category_theory.limits.cocone
added
theorem
category_theory.limits.cocone_morphism.ext
added
structure
category_theory.limits.cocone_morphism
added
theorem
category_theory.limits.cocones.comp.hom
added
def
category_theory.limits.cocones.ext
added
def
category_theory.limits.cocones.functoriality
added
theorem
category_theory.limits.cocones.id.hom
added
def
category_theory.limits.cone.extend
added
def
category_theory.limits.cone.extensions
added
def
category_theory.limits.cone.postcompose
added
theorem
category_theory.limits.cone.w
added
def
category_theory.limits.cone.whisker
added
theorem
category_theory.limits.cone.whisker_π_app
added
structure
category_theory.limits.cone
added
theorem
category_theory.limits.cone_morphism.ext
added
structure
category_theory.limits.cone_morphism
added
theorem
category_theory.limits.cones.comp.hom
added
def
category_theory.limits.cones.ext
added
def
category_theory.limits.cones.functoriality
added
theorem
category_theory.limits.cones.id.hom
Modified
category_theory/natural_isomorphism.lean
deleted
def
category_theory.functor.assoc
deleted
def
category_theory.functor.comp_id
deleted
def
category_theory.functor.id_comp
Modified
category_theory/yoneda.lean
added
theorem
category_theory.coyoneda.map_app
added
theorem
category_theory.coyoneda.obj_map
added
theorem
category_theory.coyoneda.obj_obj
added
def
category_theory.coyoneda
modified
def
category_theory.yoneda