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 : 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
    • One or more equations did not get rendered due to their size.
    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
      • 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).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