Documentation

Mathlib.CategoryTheory.Equivalence.Symmetry

Functoriality of the symmetry of equivalences #

Using the calculus of mates in Mathlib.CategoryTheory.Adjunction.Mates, we prove that passing to the symmetric equivalence defines an equivalence between C ≌ D and (D ≌ C)ᵒᵖ, and provides the definition of the functor that takes an equivalence to its inverse.

Main definitions #

source
def CategoryTheory.Equivalence.symmEquivFunctor (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] :
Functor (C ≌ D) (D ≌ C)ᵒᵖ

The forward functor of the equivalence (C ≌ D) ≌ (D ≌ C)ᵒᵖ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Equivalence.symmEquivFunctor_obj (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (e : C ≌ D) :
    (symmEquivFunctor C D).obj e = Opposite.op e.symm
    source
    @[simp]
    theorem CategoryTheory.Equivalence.symmEquivFunctor_map (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] {e f : C ≌ D} (α : e ⟶ f) :
    (symmEquivFunctor C D).map α = (mkHom ((conjugateEquiv f.toAdjunction e.toAdjunction) (asNatTrans α))).op
    source
    def CategoryTheory.Equivalence.symmEquivInverse (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] :
    Functor (D ≌ C)ᵒᵖ (C ≌ D)

    The inverse functor of the equivalence (C ≌ D) ≌ (D ≌ C)ᵒᵖ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Equivalence.symmEquivInverse_map_app (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] {X✝ Y✝ : (D ≌ C)ᵒᵖ} (f : X✝ ⟶ Y✝) (X : C) :
      ((symmEquivInverse C D).map f).app X = CategoryStruct.comp ((Opposite.unop X✝).inverse.map ((Opposite.unop Y✝).symm.unit.app X)) (CategoryStruct.comp ((Opposite.unop X✝).inverse.map ((asNatTrans f.unop).app ((Opposite.unop Y✝).inverse.obj X))) ((Opposite.unop X✝).symm.counit.app ((Opposite.unop Y✝).inverse.obj X)))
      source
      @[simp]
      theorem CategoryTheory.Equivalence.symmEquivInverse_obj_inverse (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (X : (D ≌ C)ᵒᵖ) :
      ((symmEquivInverse C D).obj X).inverse = (Opposite.unop X).functor
      source
      @[simp]
      theorem CategoryTheory.Equivalence.symmEquivInverse_obj_unitIso_inv (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (X : (D ≌ C)ᵒᵖ) :
      ((symmEquivInverse C D).obj X).unitIso.inv = (Opposite.unop X).counitIso.hom
      source
      @[simp]
      theorem CategoryTheory.Equivalence.symmEquivInverse_obj_functor (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (X : (D ≌ C)ᵒᵖ) :
      ((symmEquivInverse C D).obj X).functor = (Opposite.unop X).inverse
      source
      @[simp]
      theorem CategoryTheory.Equivalence.symmEquivInverse_obj_counitIso_hom (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (X : (D ≌ C)ᵒᵖ) :
      ((symmEquivInverse C D).obj X).counitIso.hom = (Opposite.unop X).unitIso.inv
      source
      @[simp]
      theorem CategoryTheory.Equivalence.symmEquivInverse_obj_counitIso_inv (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (X : (D ≌ C)ᵒᵖ) :
      ((symmEquivInverse C D).obj X).counitIso.inv = (Opposite.unop X).unitIso.hom
      source
      @[simp]
      theorem CategoryTheory.Equivalence.symmEquivInverse_obj_unitIso_hom (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (X : (D ≌ C)ᵒᵖ) :
      ((symmEquivInverse C D).obj X).unitIso.hom = (Opposite.unop X).counitIso.inv
      source
      def CategoryTheory.Equivalence.symmEquiv (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] :
      (C ≌ D) ≌ (D ≌ C)ᵒᵖ

      Taking the symmetric of an equivalence induces an equivalence of categories (C ≌ D) ≌ (D ≌ C)ᵒᵖ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Equivalence.symmEquiv_functor (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] :
        (symmEquiv C D).functor = symmEquivFunctor C D
        source
        @[simp]
        theorem CategoryTheory.Equivalence.symmEquiv_inverse (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] :
        (symmEquiv C D).inverse = symmEquivInverse C D
        source
        @[simp]
        theorem CategoryTheory.Equivalence.symmEquiv_unitIso (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] :
        (symmEquiv C D).unitIso = NatIso.ofComponents (fun (e : C ≌ D) => Iso.refl ((Functor.id (C ≌ D)).obj e)) ⋯
        source
        @[simp]
        theorem CategoryTheory.Equivalence.symmEquiv_counitIso (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] :
        (symmEquiv C D).counitIso = NatIso.ofComponents (fun (e : (D ≌ C)ᵒᵖ) => (Iso.refl (Opposite.unop e)).op) ⋯
        source
        def CategoryTheory.Equivalence.inverseFunctor (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] :
        Functor (C ≌ D) (Functor D C)ᵒᵖ

        The inverse functor that sends a functor to its inverse.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Equivalence.inverseFunctor_map (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] {X✝ Y✝ : C ≌ D} (f : X✝ ⟶ Y✝) :
          (inverseFunctor C D).map f = ((conjugateEquiv Y✝.toAdjunction X✝.toAdjunction) (asNatTrans f)).op
          source
          @[simp]
          theorem CategoryTheory.Equivalence.inverseFunctor_obj (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (X : C ≌ D) :
          (inverseFunctor C D).obj X = Opposite.op X.inverse
          source
          def CategoryTheory.Equivalence.inverseFunctorObjIso {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (e : C ≌ D) :
          (inverseFunctor C D).obj e ≅ Opposite.op e.inverse

          The inverse functor sends an equivalence to its inverse.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Equivalence.inverseFunctorObjIso_hom {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (e : C ≌ D) :
            e.inverseFunctorObjIso.hom = CategoryStruct.id (Opposite.op e.inverse)
            source
            @[simp]
            theorem CategoryTheory.Equivalence.inverseFunctorObjIso_inv {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (e : C ≌ D) :
            e.inverseFunctorObjIso.inv = CategoryStruct.id (Opposite.op e.inverse)
            source
            theorem CategoryTheory.Equivalence.inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] {e f : C ≌ D} (α : e ≅ f) :
            ((inverseFunctor C D).mapIso α.symm).unop = ((functorFunctor C D).mapIso α).isoInverseOfIsoFunctor

            We can compare the way we obtain a natural isomorphism e.inverse ≅ f.inverse from an isomorphism e ≌ f via inverseFunctor with the way we get one through Iso.isoInverseOfIsoFunctor.

            source
            def CategoryTheory.Equivalence.inverseFunctorObj' {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (e : C ≌ D) :
            Opposite.unop ((inverseFunctor C D).obj e) ≅ e.inverse

            An "unopped" version of the equivalence `inverseFunctorObj'.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Equivalence.inverseFunctorObj'_inv_app {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (e : C ≌ D) (X : D) :
              e.inverseFunctorObj'.inv.app X = CategoryStruct.id (e.inverse.obj X)
              source
              @[simp]
              theorem CategoryTheory.Equivalence.inverseFunctorObj'_hom_app {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (e : C ≌ D) (X : D) :
              e.inverseFunctorObj'.hom.app X = CategoryStruct.id (e.inverse.obj X)
              source
              def CategoryTheory.Equivalence.congrLeftFunctor (C : Type u_1) [Category.{u_4, u_1} C] (D : Type u_2) [Category.{u_5, u_2} D] (E : Type u_3) [Category.{u_6, u_3} E] :
              Functor (C ≌ D) (Functor C E ≌ Functor D E)ᵒᵖ

              Promoting Equivalence.congrLeft to a functor.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Equivalence.congrLeftFunctor_map (C : Type u_1) [Category.{u_4, u_1} C] (D : Type u_2) [Category.{u_5, u_2} D] (E : Type u_3) [Category.{u_6, u_3} E] {X✝ Y✝ : C ≌ D} (f : X✝ ⟶ Y✝) :
                (congrLeftFunctor C D E).map f = (mkHom ((whiskeringLeft D C E).map ((conjugateEquiv Y✝.toAdjunction X✝.toAdjunction) (asNatTrans f)))).op
                source
                @[simp]
                theorem CategoryTheory.Equivalence.congrLeftFunctor_obj (C : Type u_1) [Category.{u_4, u_1} C] (D : Type u_2) [Category.{u_5, u_2} D] (E : Type u_3) [Category.{u_6, u_3} E] (X : C ≌ D) :
                (congrLeftFunctor C D E).obj X = Opposite.op X.congrLeft