Theorems · Definition · combinatorics
Quiver.Hom.unop
{V : Type u_1} → [inst : Quiver V] → {X Y : Vᵒᵖ} → (X ⟶ Y) → (Opposite.unop Y ⟶ Opposite.unop X)Given an arrow in Vᵒᵖ, we can take the "unopposite" back in V.
- Defined in
- Mathlib.Combinatorics.Quiver.Basic
- Cited by
- 903 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 6 definitions · uses no axioms
- Assumes
- Quiver
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- Oppositestatement and proof · cited by 8,081
- Opposite.unopstatement and proof · cited by 2,231
- Quiverstatement and proof · cited by 405
Cited by1,160
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.opproof · cited by 997
- CategoryTheory.yonedaproof · cited by 351
- CategoryTheory.Functor.leftOpproof · cited by 187
- CategoryTheory.Functor.unopproof · cited by 138
- CategoryTheory.MorphismProperty.opproof · cited by 71
- CategoryTheory.nerveproof · cited by 68
- AlgebraicGeometry.Scheme.Specproof · cited by 57
- CategoryTheory.GrothendieckTopology.plusObjproof · cited by 56
- Quiver.Hom.op_injproof · cited by 45
- CategoryTheory.ShortComplex.unopproof · cited by 44
- HomologicalComplex.opFunctorproof · cited by 34
- CategoryTheory.Iso.unopproof · cited by 33
Showing the 200 most cited of 1,160.