Theorems · Definition · category theory

CategoryTheory.ComposableArrows.opEquivalence

(C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (n : ℕ) → (CategoryTheory.ComposableArrows C n)ᵒᵖ ≌ CategoryTheory.ComposableArrows Cᵒᵖ n

The equivalence (ComposableArrows C n)ᵒᵖ ≌ ComposableArrows Cᵒᵖ n obtained by reversing the arrows.

Defined in: Mathlib.CategoryTheory.ComposableArrows.Basic
Cited by: 10 results in Mathlib
Foundations: Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

CategoryTheory.Categorystatement and proof · cited by 32,673
Oppositestatement · cited by 8,081
CategoryTheory.ComposableArrowsstatement · cited by 627
CategoryTheory.Equivalencestatement · cited by 601
CategoryTheory.Equivalence.symmproof · cited by 195
CategoryTheory.Equivalence.transproof · cited by 57
CategoryTheory.Equivalence.opproof · cited by 57
CategoryTheory.Equivalence.congrLeftproof · cited by 46
OrderIso.equivalenceproof · cited by 16
CategoryTheory.orderDualEquivalenceproof · cited by 15
CategoryTheory.Functor.leftOpRightOpEquivproof · cited by 15
Fin.revOrderIsoproof · cited by 11

Cited by11

Results whose statement or proof uses this declaration.

CategoryTheory.Functor.mapComposableArrowsOpIsostatement and proof · cited by 1
CategoryTheory.Localization.essSurj_mapComposableArrowsproof · cited by 1
CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_appstatement · cited by 0
CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_appstatement · cited by 0
CategoryTheory.ComposableArrows.opEquivalence_functor_map_appstatement and proof · cited by 0
CategoryTheory.ComposableArrows.opEquivalence_functor_obj_mapstatement and proof · cited by 0
CategoryTheory.ComposableArrows.opEquivalence_functor_obj_objstatement and proof · cited by 0
CategoryTheory.ComposableArrows.opEquivalence_inverse_mapstatement and proof · cited by 0
CategoryTheory.ComposableArrows.opEquivalence_inverse_objstatement and proof · cited by 0
CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_appstatement · cited by 0
CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_appstatement · cited by 0