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.

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.

    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.

      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