Mathlib Changelog
v4
Changelog
About
Github
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