Theorems · Definition · combinatorics
Quiver.Hom.op
{V : Type u_1} → [inst : Quiver V] → {X Y : V} → (X ⟶ Y) → (Opposite.op Y ⟶ Opposite.op X)The opposite of an arrow in V.
- Defined in
- Mathlib.Combinatorics.Quiver.Basic
- Cited by
- 1,948 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.
Cites3
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 · cited by 8,081
- Quiverstatement and proof · cited by 405
Cited by2,449
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.opproof · cited by 997
- CategoryTheory.Functor.rightOpproof · cited by 214
- CategoryTheory.SimplicialObject.δproof · cited by 188
- CategoryTheory.GrothendieckTopology.Cover.indexproof · cited by 142
- AlgebraicGeometry.Scheme.Hom.appLEproof · cited by 138
- CategoryTheory.Functor.unopproof · cited by 138
- CategoryTheory.SimplicialObject.σproof · cited by 106
- CategoryTheory.ShortComplex.opproof · cited by 88
- CategoryTheory.Presieve.FamilyOfElements.Compatibleproof · cited by 79
- CategoryTheory.op_compstatement · cited by 72
- CategoryTheory.eqToHom_opstatement and proof · cited by 68
- SSet.constproof · cited by 62
Showing the 200 most cited of 2,449.