Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-02 08:08 ef11fb3d

View on Github →

feat(category_theory/limits/opposites): (co)limits in opposite categories (#926)

(co)limits in opposite categories
moving lemmas
moving stuff about complete lattices to separate PR
renaming category_of_preorder elsewhere
build limits functor/shape at a time
removing stray commas, and making one-liners
remove non-terminal simps

Estimated changes

Modified src/category_theory/const.lean

added def category_theory.functor.const.op_obj_op

added theorem category_theory.functor.const.op_obj_op_hom_app

added theorem category_theory.functor.const.op_obj_op_inv_app

added def category_theory.functor.const.op_obj_unop

added theorem category_theory.functor.const.op_obj_unop_hom_app

added theorem category_theory.functor.const.op_obj_unop_inv_app

Modified src/category_theory/limits/cones.lean

added def category_theory.limits.cocone_left_op_of_cone

added theorem category_theory.limits.cocone_left_op_of_cone_X

added theorem category_theory.limits.cocone_left_op_of_cone_ι_app

added def category_theory.limits.cocone_of_cone_left_op

added theorem category_theory.limits.cocone_of_cone_left_op_X

added theorem category_theory.limits.cocone_of_cone_left_op_ι_app

added def category_theory.limits.cone_left_op_of_cocone

added theorem category_theory.limits.cone_left_op_of_cocone_X

added theorem category_theory.limits.cone_left_op_of_cocone_π_app

added def category_theory.limits.cone_of_cocone_left_op

added theorem category_theory.limits.cone_of_cocone_left_op_X

added theorem category_theory.limits.cone_of_cocone_left_op_π_app

Created src/category_theory/limits/opposites.lean

Modified src/category_theory/opposites.lean

added theorem category_theory.functor.left_op_map

added theorem category_theory.functor.left_op_obj

added theorem category_theory.functor.right_op_map

added theorem category_theory.functor.right_op_obj

added theorem category_theory.nat_trans.left_op_app

added theorem category_theory.nat_trans.op_app

added theorem category_theory.nat_trans.right_op_app

added theorem category_theory.nat_trans.unop_app

Modified src/category_theory/yoneda.lean