Theorems · Definition · category theory

CategoryTheory.isoOpEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (A B : Cᵒᵖ) → (A ≅ B) ≃ (Opposite.unop B ≅ Opposite.unop A)

The equivalence between isomorphisms of the form A ≅ B and B.unop ≅ A.unop. Note this is definitionally the same as the other three variants: * (Opposite.op A ≅ B) ≃ (B.unop ≅ A) * (A ≅ Opposite.op B) ≃ (B ≅ A.unop) * (Opposite.op A ≅ Opposite.op B) ≃ (B ≅ A)

Defined in

Mathlib.CategoryTheory.Opposites

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

CategoryTheory.Category