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
๐Ÿ”ธ coverage
def CategoryTheory.Cat.opFunctor :
Functor Cat Cat

The endofunctor Cat โฅค Cat assigning to each category its opposite category.

Equations
    Instances For
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem CategoryTheory.Cat.opFunctor_obj (C : Cat) :
      opFunctor.obj C = of (โ†‘C)แต’แต–
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem CategoryTheory.Cat.opFunctor_map {Xโœ Yโœ : Cat} (F : Xโœ โŸถ Yโœ) :
      opFunctor.map F = F.toFunctor.op.toCatHom
      source
      ๐Ÿ”ธ coverage
      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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ”ธ coverage
          def CategoryTheory.Cat.opEquivalence :
          Cat โ‰Œ Cat

          The equivalence Cat โ‰Œ Cat associating each category with its opposite category.

          Equations
            Instances For
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem CategoryTheory.Cat.opEquivalence_inverse :
              opEquivalence.inverse = opFunctor
              source
              ๐Ÿ“ coverage
              @[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
              ๐Ÿ“ coverage
              @[simp]
              theorem CategoryTheory.Cat.opEquivalence_functor :
              opEquivalence.functor = opFunctor
              source
              ๐Ÿ“ coverage
              @[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