Theorems · Definition · category theory
CategoryTheory.MonoidalOpposite.unmop
{C : Type u₁} → Cᴹᵒᵖ → CThe object of C represented by x : MonoidalOpposite C.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Opposite
- Cited by
- 108 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.MonoidalOppositestatement and proof · cited by 179
Cited by116
Results whose statement or proof uses this declaration.
- Quiver.Hom.unmopstatement and proof · cited by 40
- CategoryTheory.unmopFunctorproof · cited by 24
- MonObj.mopEquivproof · cited by 14
- CategoryTheory.Iso.unmopstatement · cited by 4
- CategoryTheory.MonoidalOpposite.tensorLeftIsostatement · cited by 2
- CategoryTheory.MonoidalOpposite.tensorLeftUnmopIsostatement and proof · cited by 2
- CategoryTheory.MonoidalOpposite.tensorRightIsostatement · cited by 2
- CategoryTheory.MonoidalOpposite.tensorRightUnmopIsostatement and proof · cited by 2
- CategoryTheory.MonoidalOpposite.unmop_injectivestatement and proof · cited by 1
- Quiver.Hom.unmop_injstatement · cited by 1
- CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomstatement · cited by 0