Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-28 20:15 042c290d

View on Github →

refactor(category_theory/opposites): Make opposite irreducible

Estimated changes

Modified src/category_theory/adjunction.lean

Modified src/category_theory/limits/cones.lean

modified theorem category_theory.cocones_map

modified theorem category_theory.cocones_obj

modified def category_theory.functor.cocones

modified theorem category_theory.functor.cones_map_app

modified theorem category_theory.functor.cones_obj

modified def category_theory.limits.cocone.extensions

Modified src/category_theory/limits/limits.lean

modified def category_theory.limits.is_colimit.nat_iso

modified def category_theory.limits.limit.hom_iso

Modified src/category_theory/opposites.lean

deleted theorem category_theory.functor.category.op_comp_app

deleted theorem category_theory.functor.category.op_id_app

modified theorem category_theory.functor.hom_obj

modified theorem category_theory.functor.op_hom.map_app

modified theorem category_theory.functor.op_hom.obj

modified theorem category_theory.functor.op_inv.obj

modified theorem category_theory.functor.op_map

modified theorem category_theory.functor.op_obj

modified theorem category_theory.functor.unop_map

modified theorem category_theory.functor.unop_obj

added def category_theory.has_hom.hom.op

added theorem category_theory.has_hom.hom.op_inj

added theorem category_theory.has_hom.hom.op_unop

added def category_theory.has_hom.hom.unop

added theorem category_theory.has_hom.hom.unop_inj

added theorem category_theory.has_hom.hom.unop_op

modified def category_theory.op

added theorem category_theory.op_comp

added theorem category_theory.op_id

added theorem category_theory.op_unop

added def category_theory.opposite

added def category_theory.unop

added theorem category_theory.unop_comp

added theorem category_theory.unop_id

added theorem category_theory.unop_op

Modified src/category_theory/yoneda.lean

modified theorem category_theory.coyoneda.map_app

modified theorem category_theory.coyoneda.obj_map

modified theorem category_theory.coyoneda.obj_obj

modified theorem category_theory.yoneda.map_app

modified theorem category_theory.yoneda.obj_map

modified theorem category_theory.yoneda.obj_map_id

modified theorem category_theory.yoneda.obj_obj

modified def category_theory.yoneda_sections

modified def category_theory.yoneda_sections_small