Commit 2023-02-11 10:25 5a92eb06

View on Github →

feat: port CategoryTheory.Opposites (#2195)

depends on: #1287 ~~- [x] depends on tactic tidy?~~

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Iso.lean

added theorem CategoryTheory.Iso.nonempty_iso_refl

Created Mathlib/CategoryTheory/Opposites.lean

added def CategoryTheory.Equivalence.op

added def CategoryTheory.Equivalence.unop

added def CategoryTheory.Functor.leftOpRightOpEquiv

added def CategoryTheory.Functor.leftOpRightOpIso

added def CategoryTheory.Functor.opHom

added def CategoryTheory.Functor.opInv

added def CategoryTheory.Functor.opUnopEquiv

added def CategoryTheory.Functor.opUnopIso

added def CategoryTheory.Functor.rightOpLeftOpIso

added theorem CategoryTheory.Functor.rightOp_leftOp_eq

added def CategoryTheory.Functor.unopOpIso

added theorem CategoryTheory.Iso.op_unop

added def CategoryTheory.Iso.unop

added theorem CategoryTheory.Iso.unop_op

added theorem CategoryTheory.NatTrans.leftOp_comp

added theorem CategoryTheory.NatTrans.leftOp_id

added theorem CategoryTheory.NatTrans.op_id

added theorem CategoryTheory.NatTrans.removeLeftOp_id

added theorem CategoryTheory.NatTrans.removeOp_id

added theorem CategoryTheory.NatTrans.removeRightOp_id

added theorem CategoryTheory.NatTrans.removeUnop_id

added theorem CategoryTheory.NatTrans.rightOp_comp

added theorem CategoryTheory.NatTrans.rightOp_id

added theorem CategoryTheory.NatTrans.unop_id

added theorem CategoryTheory.isIso_of_op

added theorem CategoryTheory.isIso_op_iff

added theorem CategoryTheory.isIso_unop_iff

added def CategoryTheory.isoOpEquiv

added def CategoryTheory.opEquiv

added def CategoryTheory.opOp

added def CategoryTheory.opOpEquivalence

added theorem CategoryTheory.op_comp

added theorem CategoryTheory.op_id

added theorem CategoryTheory.op_id_unop

added theorem CategoryTheory.op_inv

added def CategoryTheory.unopUnop

added theorem CategoryTheory.unop_comp

added theorem CategoryTheory.unop_id

added theorem CategoryTheory.unop_id_op

added theorem CategoryTheory.unop_inv

added theorem Quiver.Hom.op_inj

added theorem Quiver.Hom.op_unop

added theorem Quiver.Hom.unop_inj

added theorem Quiver.Hom.unop_op