Mathlib Map

Theorems · Definition · category theory

Opposite.unop

{α : Sort u} → αᵒᵖ → α

The canonical map αᵒᵖ → α.

Defined in
Mathlib.Data.Opposite
Cited by
2,231 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Functor.op · cited by 997Functor.opQuiver.Hom.unop · cited by 903Hom.unopCategoryTheory.yoneda · cited by 351CategoryTheory.yonedaCategoryTheory.Functor.leftOp · cited by 187Functor.leftOpCategoryTheory.Functor.unop · cited by 138Functor.unopCategoryTheory.MorphismProperty.op · cited by 71MorphismProperty.opCategoryTheory.nerve · cited by 68CategoryTheory.nerveCategoryTheory.SimplicialObject.Splitting.IndexSet · cited by 65Splitting.IndexSetSSet.const · cited by 62SSet.constSSet.stdSimplex.objEquiv · cited by 59stdSimplex.objEquivAlgebraicGeometry.Scheme.Spec · cited by 57Scheme.SpecCategoryTheory.GrothendieckTopology.plusObj · cited by 56GrothendieckTopology.plus…TopCat.Presheaf.stalkSpecializes · cited by 51Presheaf.stalkSpecializesCategoryTheory.SimplicialObject.Splitting.summand · cited by 48Splitting.summandCategoryTheory.SimplicialObject.Splitting.cofan · cited by 46Splitting.cofanOpposite · cited by 8081OppositeOpposite.unopCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Oppositestatement and proof · cited by 8,081

Cited by2,761

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 2,761.