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
    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 : X✝ ⟶ Y✝) :
      opFunctor.map F = F.toFunctor.op.toCatHom
      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
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Cat.opFunctorInvolutive_inv_app_toFunctor_obj (X : Cat) (X✝ : ↑X) :
          (opFunctorInvolutive.inv.app X).toFunctor.obj X✝ = Opposite.op (Opposite.op X✝)
          source
          @[simp]
          theorem CategoryTheory.Cat.opFunctorInvolutive_hom_app_toFunctor_map (X : Cat) {X✝ Y✝ : (↑X)ᵒᵖᵒᵖ} (f : X✝ ⟶ Y✝) :
          (opFunctorInvolutive.hom.app X).toFunctor.map f = f.unop.unop
          source
          @[simp]
          theorem CategoryTheory.Cat.opFunctorInvolutive_hom_app_toFunctor_obj (X : Cat) (X✝ : (↑X)ᵒᵖᵒᵖ) :
          (opFunctorInvolutive.hom.app X).toFunctor.obj X✝ = Opposite.unop (Opposite.unop X✝)
          source
          @[simp]
          theorem CategoryTheory.Cat.opFunctorInvolutive_inv_app_toFunctor_map (X : Cat) {X✝ Y✝ : ↑X} (f : X✝ ⟶ Y✝) :
          (opFunctorInvolutive.inv.app X).toFunctor.map f = f.op.op
          source
          def CategoryTheory.Cat.opEquivalence :
          Cat ≌ Cat

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

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Cat.opEquivalence_counitIso :
              opEquivalence.counitIso = NatIso.ofComponents (fun (x : Cat) => { hom := (unopUnop ↑x).toCatHom, inv := (opOp ↑x).toCatHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }) @opEquivalence._proof_4
              source
              @[simp]
              theorem CategoryTheory.Cat.opEquivalence_functor :
              opEquivalence.functor = opFunctor
              source
              @[simp]
              theorem CategoryTheory.Cat.opEquivalence_unitIso :
              opEquivalence.unitIso = NatIso.ofComponents (fun (x : Cat) => { hom := (opOp ↑x).toCatHom, inv := (unopUnop ↑x).toCatHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }) @opEquivalence._proof_3
              source
              @[simp]
              theorem CategoryTheory.Cat.opEquivalence_inverse :
              opEquivalence.inverse = opFunctor