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
    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
        Instances For
          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_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_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_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_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_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
            Instances For
              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_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_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_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'_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
                          @[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
                          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
                            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 ((Functor.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