Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-30 09:51 ff66d924

View on Github →

chore(category_theory/limits): facts about opposites of limit cones (#4250) Simple facts about limit cones and opposite categories.

Estimated changes

Modified src/category_theory/adjunction/opposites.lean

Modified src/category_theory/limits/cones.lean

added def category_theory.functor.map_cocone_op

added def category_theory.functor.map_cone_op

added def category_theory.limits.cocone.op

added def category_theory.limits.cocone.unop

added def category_theory.limits.cocone_equivalence_op_cone_op

added def category_theory.limits.cone.op

added def category_theory.limits.cone.unop

Modified src/category_theory/limits/limits.lean

added def category_theory.limits.is_colimit.op

added def category_theory.limits.is_colimit.unop

added def category_theory.limits.is_colimit_equiv_is_limit_op

added def category_theory.limits.is_limit.op

added def category_theory.limits.is_limit.unop

added def category_theory.limits.is_limit_equiv_is_colimit_op

Modified src/category_theory/monad/equiv_mon.lean

added def category_theory.Monad.Monad_Mon_equiv.counit_iso

added def category_theory.Monad.Monad_Mon_equiv.unit_iso

added def category_theory.Monad.Monad_Mon_equiv.unit_iso_hom

added def category_theory.Monad.Monad_Mon_equiv.unit_iso_inv

deleted def category_theory.Monad.of_to_mon_end_iso

deleted def category_theory.Monad.to_of_mon_end_iso

Modified src/category_theory/opposites.lean

added def category_theory.equivalence.op

added def category_theory.equivalence.unop

added def category_theory.functor.op_hom

added def category_theory.functor.op_inv

added theorem category_theory.nat_iso.remove_op_hom

added theorem category_theory.nat_iso.remove_op_inv

modified theorem category_theory.nat_iso.unop_hom

modified theorem category_theory.nat_iso.unop_inv

added theorem category_theory.nat_trans.remove_left_op_app

added theorem category_theory.nat_trans.remove_op_id

deleted theorem category_theory.nat_trans.right_op_app

modified theorem category_theory.nat_trans.unop_id

Modified src/data/opposite.lean