Documentation

Mathlib.CategoryTheory.Category.Cat.Op

The dualizing functor on Cat #

We define a (strict) functor opFunctor and an equivalence assigning opposite categories to categories. We then show that this functor is strictly involutive and that it induces an equivalence on Cat.

source
def CategoryTheory.Cat.opFunctor :
Functor Cat Cat

The endofunctor Cat ⥤ Cat assigning to each category its opposite category.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Cat.opFunctor_obj (C : Cat) :
    opFunctor.obj C = of (↑C)ᵒᵖ
    source
    @[simp]
    theorem CategoryTheory.Cat.opFunctor_map {X✝ Y✝ : Cat} (F : Functor ↑X✝ ↑Y✝) :
    opFunctor.map F = F.op
    source
    def CategoryTheory.Cat.opFunctorInvolutive :
    opFunctor.comp opFunctor ≅ Functor.id Cat

    The natural isomorphism between the double application of Cat.opFunctor and the identity functor on Cat.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Cat.opFunctorInvolutive_hom_app_map (X : Cat) {X✝ Y✝ : (↑X)ᵒᵖᵒᵖ} (f : X✝ ⟶ Y✝) :
      (opFunctorInvolutive.hom.app X).map f = f.unop.unop
      source
      @[simp]
      theorem CategoryTheory.Cat.opFunctorInvolutive_inv_app_map (X : Cat) {X✝ Y✝ : ↑X} (f : X✝ ⟶ Y✝) :
      (opFunctorInvolutive.inv.app X).map f = f.op.op
      source
      @[simp]
      theorem CategoryTheory.Cat.opFunctorInvolutive_inv_app_obj (X : Cat) (X✝ : ↑X) :
      (opFunctorInvolutive.inv.app X).obj X✝ = Opposite.op (Opposite.op X✝)
      source
      @[simp]
      theorem CategoryTheory.Cat.opFunctorInvolutive_hom_app_obj (X : Cat) (X✝ : (↑X)ᵒᵖᵒᵖ) :
      (opFunctorInvolutive.hom.app X).obj X✝ = Opposite.unop (Opposite.unop X✝)
      source
      def CategoryTheory.Cat.opEquivalence :
      Cat ≌ Cat

      The equivalence Cat ≌ Cat associating each category with its opposite category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Cat.opEquivalence_counitIso :
        opEquivalence.counitIso = NatIso.ofComponents (fun (x : Cat) => { hom := unopUnop ↑x, inv := opOp ↑((Functor.id Cat).obj x), hom_inv_id := ⋯, inv_hom_id := ⋯ }) @opEquivalence.proof_6
        source
        @[simp]
        theorem CategoryTheory.Cat.opEquivalence_functor :
        opEquivalence.functor = opFunctor
        source
        @[simp]
        theorem CategoryTheory.Cat.opEquivalence_inverse :
        opEquivalence.inverse = opFunctor
        source
        @[simp]
        theorem CategoryTheory.Cat.opEquivalence_unitIso :
        opEquivalence.unitIso = NatIso.ofComponents (fun (x : Cat) => { hom := opOp ↑((Functor.id Cat).obj x), inv := unopUnop ↑x, hom_inv_id := ⋯, inv_hom_id := ⋯ }) @opEquivalence.proof_3