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