Documentation

Mathlib.CategoryTheory.Equivalence

Equivalence of categories #

An equivalence of categories C and D is a pair of functors F : C ⥤ D and G : D ⥤ C such that η : 𝟭 C ≅ F ⋙ G and ε : G ⋙ F ≅ 𝟭 D. In many situations, equivalences are a better notion of "sameness" of categories than the stricter isomorphism of categories.

Recall that one way to express that two functors F : C ⥤ D and G : D ⥤ C are adjoint is using two natural transformations η : 𝟭 C ⟶ F ⋙ G and ε : G ⋙ F ⟶ 𝟭 D, called the unit and the counit, such that the compositions F ⟶ FGF ⟶ F and G ⟶ GFG ⟶ G are the identity. Unfortunately, it is not the case that the natural isomorphisms η and ε in the definition of an equivalence automatically give an adjunction. However, it is true that

For this reason, in mathlib we define an equivalence to be a "half-adjoint equivalence", which is a tuple (F, G, η, ε) as in the first paragraph such that the composite F ⟶ FGF ⟶ F is the identity. By the remark above, this already implies that the tuple is an "adjoint equivalence", i.e., that the composite G ⟶ GFG ⟶ G is also the identity.

We also define essentially surjective functors and show that a functor is an equivalence if and only if it is full, faithful and essentially surjective.

Main definitions #

Main results #

Notations #

We write C ≌ D (\backcong, not to be confused with /\cong) for a bundled equivalence.

structure CategoryTheory.Equivalence (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] :
Type (max (max (max u₁ u₂) v₁) v₂)

We define an equivalence as a (half)-adjoint equivalence, a pair of functors with a unit and counit which are natural isomorphisms and the triangle law Fη ≫ εF = 1, or in other words the composite F ⟶ FGF ⟶ F is the identity.

In unit_inverse_comp, we show that this is actually an adjoint equivalence, i.e., that the composite G ⟶ GFG ⟶ G is also the identity.

The triangle equation is written as a family of equalities between morphisms, it is more complicated if we write it as an equality of natural transformations, because then we would have to insert natural transformations like F ⟶ F1.

See

Instances For

    We infix the usual notation for an equivalence

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[inline, reducible]

      The unit of an equivalence of categories.

      Equations
      • e.unit = e.unitIso.hom
      Instances For
        @[inline, reducible]

        The counit of an equivalence of categories.

        Equations
        • e.counit = e.counitIso.hom
        Instances For
          @[inline, reducible]

          The inverse of the unit of an equivalence of categories.

          Equations
          • e.unitInv = e.unitIso.inv
          Instances For
            @[inline, reducible]

            The inverse of the counit of an equivalence of categories.

            Equations
            • e.counitInv = e.counitIso.inv
            Instances For
              @[simp]
              theorem CategoryTheory.Equivalence.Equivalence_mk'_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C CategoryTheory.Functor.comp functor inverse) (counit_iso : CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.toPrefunctor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (functor.toPrefunctor.obj X)) :
              (CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).unit = unit_iso.hom
              @[simp]
              theorem CategoryTheory.Equivalence.Equivalence_mk'_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C CategoryTheory.Functor.comp functor inverse) (counit_iso : CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.toPrefunctor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (functor.toPrefunctor.obj X)) :
              (CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).counit = counit_iso.hom
              @[simp]
              theorem CategoryTheory.Equivalence.Equivalence_mk'_unitInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C CategoryTheory.Functor.comp functor inverse) (counit_iso : CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.toPrefunctor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (functor.toPrefunctor.obj X)) :
              (CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).unitInv = unit_iso.inv
              @[simp]
              theorem CategoryTheory.Equivalence.Equivalence_mk'_counitInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C CategoryTheory.Functor.comp functor inverse) (counit_iso : CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.toPrefunctor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (functor.toPrefunctor.obj X)) :
              (CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).counitInv = counit_iso.inv
              @[simp]
              theorem CategoryTheory.Equivalence.functor_unit_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) {Z : D} (h : e.functor.toPrefunctor.obj X Z) :
              CategoryTheory.CategoryStruct.comp (e.functor.toPrefunctor.map (e.unit.app X)) (CategoryTheory.CategoryStruct.comp (e.counit.app (e.functor.toPrefunctor.obj X)) h) = h
              @[simp]
              theorem CategoryTheory.Equivalence.functor_unit_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) :
              CategoryTheory.CategoryStruct.comp (e.functor.toPrefunctor.map (e.unit.app X)) (e.counit.app (e.functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (e.functor.toPrefunctor.obj X)
              @[simp]
              theorem CategoryTheory.Equivalence.counitInv_functor_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) {Z : D} (h : e.functor.toPrefunctor.obj X Z) :
              CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp (e.functor.toPrefunctor.map (e.unitInv.app X)) h) = h
              @[simp]
              theorem CategoryTheory.Equivalence.counitInv_functor_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) :
              CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.toPrefunctor.obj X)) (e.functor.toPrefunctor.map (e.unitInv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.toPrefunctor.obj X)
              theorem CategoryTheory.Equivalence.counitInv_app_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) :
              e.counitInv.app (e.functor.toPrefunctor.obj X) = e.functor.toPrefunctor.map (e.unit.app X)
              theorem CategoryTheory.Equivalence.counit_app_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) :
              e.counit.app (e.functor.toPrefunctor.obj X) = e.functor.toPrefunctor.map (e.unitInv.app X)
              @[simp]
              theorem CategoryTheory.Equivalence.unit_inverse_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (Y : D) {Z : C} (h : e.inverse.toPrefunctor.obj Y Z) :
              CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.toPrefunctor.obj Y)) (CategoryTheory.CategoryStruct.comp (e.inverse.toPrefunctor.map (e.counit.app Y)) h) = h
              @[simp]
              theorem CategoryTheory.Equivalence.unit_inverse_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (Y : D) :
              CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.toPrefunctor.obj Y)) (e.inverse.toPrefunctor.map (e.counit.app Y)) = CategoryTheory.CategoryStruct.id (e.inverse.toPrefunctor.obj Y)

              The other triangle equality. The proof follows the following proof in Globular: http://globular.science/1905.001

              @[simp]
              theorem CategoryTheory.Equivalence.inverse_counitInv_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (Y : D) {Z : C} (h : e.inverse.toPrefunctor.obj Y Z) :
              CategoryTheory.CategoryStruct.comp (e.inverse.toPrefunctor.map (e.counitInv.app Y)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app (e.inverse.toPrefunctor.obj Y)) h) = h
              @[simp]
              theorem CategoryTheory.Equivalence.inverse_counitInv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (Y : D) :
              CategoryTheory.CategoryStruct.comp (e.inverse.toPrefunctor.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.toPrefunctor.obj Y)) = CategoryTheory.CategoryStruct.id (e.inverse.toPrefunctor.obj Y)
              theorem CategoryTheory.Equivalence.unit_app_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (Y : D) :
              e.unit.app (e.inverse.toPrefunctor.obj Y) = e.inverse.toPrefunctor.map (e.counitInv.app Y)
              theorem CategoryTheory.Equivalence.unitInv_app_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (Y : D) :
              e.unitInv.app (e.inverse.toPrefunctor.obj Y) = e.inverse.toPrefunctor.map (e.counit.app Y)
              theorem CategoryTheory.Equivalence.fun_inv_map_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : D) (Y : D) (f : X Y) {Z : D} (h : e.functor.toPrefunctor.obj (e.inverse.toPrefunctor.obj Y) Z) :
              CategoryTheory.CategoryStruct.comp (e.functor.toPrefunctor.map (e.inverse.toPrefunctor.map f)) h = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h))
              @[simp]
              theorem CategoryTheory.Equivalence.fun_inv_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : D) (Y : D) (f : X Y) :
              e.functor.toPrefunctor.map (e.inverse.toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y))
              theorem CategoryTheory.Equivalence.inv_fun_map_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) (Y : C) (f : X Y) {Z : C} (h : e.inverse.toPrefunctor.obj (e.functor.toPrefunctor.obj Y) Z) :
              CategoryTheory.CategoryStruct.comp (e.inverse.toPrefunctor.map (e.functor.toPrefunctor.map f)) h = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h))
              @[simp]
              theorem CategoryTheory.Equivalence.inv_fun_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) (Y : C) (f : X Y) :
              e.inverse.toPrefunctor.map (e.functor.toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (e.unit.app Y))

              If η : 𝟭 C ≅ F ⋙ G is part of a (not necessarily half-adjoint) equivalence, we can upgrade it to a refined natural isomorphism adjointifyη η : 𝟭 C ≅ F ⋙ G which exhibits the properties required for a half-adjoint equivalence. See Equivalence.mk.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Every equivalence of categories consisting of functors F and G such that F ⋙ G and G ⋙ F are naturally isomorphic to identity functors can be transformed into a half-adjoint equivalence without changing F or G.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.Equivalence.refl_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                  CategoryTheory.Equivalence.refl.inverse = CategoryTheory.Functor.id C
                  @[simp]
                  theorem CategoryTheory.Equivalence.refl_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                  CategoryTheory.Equivalence.refl.functor = CategoryTheory.Functor.id C

                  Equivalence of categories is reflexive.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • CategoryTheory.Equivalence.instInhabitedEquivalence = { default := CategoryTheory.Equivalence.refl }
                    @[simp]
                    theorem CategoryTheory.Equivalence.symm_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) :
                    e.symm.counitIso = e.unitIso.symm
                    @[simp]
                    theorem CategoryTheory.Equivalence.symm_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) :
                    e.symm.unitIso = e.counitIso.symm
                    @[simp]
                    @[simp]

                    Equivalence of categories is symmetric.

                    Equations
                    Instances For
                      @[simp]

                      Equivalence of categories is transitive.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Composing a functor with both functors of an equivalence yields a naturally isomorphic functor.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Composing a functor with both functors of an equivalence yields a naturally isomorphic functor.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            If C is equivalent to D, then C ⥤ E is equivalent to D ⥤ E.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              If C is equivalent to D, then E ⥤ C is equivalent to E ⥤ D.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem CategoryTheory.Equivalence.cancel_unit_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {X : C} {Y : C} (f : X Y) (f' : X Y) :
                                @[simp]
                                theorem CategoryTheory.Equivalence.cancel_unitInv_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {X : C} {Y : C} (f : X e.inverse.toPrefunctor.obj (e.functor.toPrefunctor.obj Y)) (f' : X e.inverse.toPrefunctor.obj (e.functor.toPrefunctor.obj Y)) :
                                CategoryTheory.CategoryStruct.comp f (e.unitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unitInv.app Y) f = f'
                                @[simp]
                                theorem CategoryTheory.Equivalence.cancel_counit_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {X : D} {Y : D} (f : X e.functor.toPrefunctor.obj (e.inverse.toPrefunctor.obj Y)) (f' : X e.functor.toPrefunctor.obj (e.inverse.toPrefunctor.obj Y)) :
                                @[simp]
                                theorem CategoryTheory.Equivalence.cancel_counitInv_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {X : D} {Y : D} (f : X Y) (f' : X Y) :
                                CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counitInv.app Y) f = f'

                                Natural number powers of an auto-equivalence. Use (^) instead.

                                Equations
                                Instances For

                                  Powers of an auto-equivalence. Use (^) instead.

                                  Equations
                                  Instances For
                                    Equations
                                    • CategoryTheory.Equivalence.instPowEquivalenceInt = { pow := CategoryTheory.Equivalence.pow }
                                    @[simp]
                                    theorem CategoryTheory.Equivalence.pow_zero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (e : C C) :
                                    e ^ 0 = CategoryTheory.Equivalence.refl
                                    @[simp]
                                    class CategoryTheory.IsEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                                    Type (max (max (max u₁ u₂) v₁) v₂)

                                    A functor that is part of a (half) adjoint equivalence

                                    Instances
                                      @[simp]
                                      theorem CategoryTheory.IsEquivalence.functor_unitIso_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [self : CategoryTheory.IsEquivalence F] (X : C) {Z : D} (h : F.toPrefunctor.obj X Z) :
                                      CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.IsEquivalence.unitIso.hom.app X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.counitIso.hom.app (F.toPrefunctor.obj X)) h) = h

                                      To see that a functor is an equivalence, it suffices to provide an inverse functor G such that F ⋙ G and G ⋙ F are naturally isomorphic to identity functors.

                                      Equations
                                      Instances For

                                        Interpret a functor that is an equivalence as an equivalence.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Equivalence.isEquivalence_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : C D) :
                                          CategoryTheory.IsEquivalence.unitIso = E.unitIso
                                          @[simp]
                                          theorem CategoryTheory.Equivalence.isEquivalence_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : C D) :
                                          CategoryTheory.IsEquivalence.counitIso = E.counitIso
                                          @[simp]
                                          theorem CategoryTheory.IsEquivalence.ofIso_unitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (e : F G) (hF : CategoryTheory.IsEquivalence F) (X : C) :
                                          CategoryTheory.IsEquivalence.unitIso.inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.IsEquivalence.inverse F).toPrefunctor.map (e.inv.app X)) (CategoryTheory.IsEquivalence.unitIso.inv.app X)
                                          @[simp]
                                          theorem CategoryTheory.IsEquivalence.ofIso_unitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (e : F G) (hF : CategoryTheory.IsEquivalence F) (X : C) :
                                          CategoryTheory.IsEquivalence.unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.unitIso.hom.app X) ((CategoryTheory.IsEquivalence.inverse F).toPrefunctor.map (e.hom.app X))
                                          @[simp]
                                          theorem CategoryTheory.IsEquivalence.ofIso_counitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (e : F G) (hF : CategoryTheory.IsEquivalence F) (X : D) :
                                          CategoryTheory.IsEquivalence.counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.counitIso.inv.app X) (e.hom.app ((CategoryTheory.IsEquivalence.inverse F).toPrefunctor.obj X))
                                          @[simp]
                                          theorem CategoryTheory.IsEquivalence.ofIso_counitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (e : F G) (hF : CategoryTheory.IsEquivalence F) (X : D) :
                                          CategoryTheory.IsEquivalence.counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.inv.app ((CategoryTheory.IsEquivalence.inverse F).toPrefunctor.obj X)) (CategoryTheory.IsEquivalence.counitIso.hom.app X)

                                          When a functor F is an equivalence of categories, and G is isomorphic to F, then G is also an equivalence of categories.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            When F and G are two isomorphic functors, then F is an equivalence iff G is.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

                                              If G and F ⋙ G are equivalence of categories, then F is also an equivalence.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                If F and F ⋙ G are equivalence of categories, then G is also an equivalence.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  An equivalence is full.

                                                  See .

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.

                                                  A functor which is full, faithful, and essentially surjective is an equivalence.

                                                  See .

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.Equivalence.functor_map_inj_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {X : C} {Y : C} (f : X Y) (g : X Y) :
                                                    e.functor.toPrefunctor.map f = e.functor.toPrefunctor.map g f = g
                                                    @[simp]
                                                    theorem CategoryTheory.Equivalence.inverse_map_inj_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {X : D} {Y : D} (f : X Y) (g : X Y) :
                                                    e.inverse.toPrefunctor.map f = e.inverse.toPrefunctor.map g f = g
                                                    @[simp]
                                                    theorem CategoryTheory.Iso.compInvIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [h : CategoryTheory.IsEquivalence H] (i : F CategoryTheory.Functor.comp G H) (X : C) :
                                                    (CategoryTheory.Iso.compInvIso i).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.inv H).toPrefunctor.map (i.hom.app X)) (CategoryTheory.IsEquivalence.unitIso.inv.app (G.toPrefunctor.obj X))
                                                    @[simp]
                                                    theorem CategoryTheory.Iso.compInvIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [h : CategoryTheory.IsEquivalence H] (i : F CategoryTheory.Functor.comp G H) (X : C) :
                                                    (CategoryTheory.Iso.compInvIso i).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.unitIso.hom.app (G.toPrefunctor.obj X)) ((CategoryTheory.Functor.inv H).toPrefunctor.map (i.inv.app X))

                                                    Construct an isomorphism F ⋙ H.inv ≅ G from an isomorphism F ≅ G ⋙ H.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.Iso.compInverseIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D E} (i : F CategoryTheory.Functor.comp G H.functor) (X : C) :
                                                      (CategoryTheory.Iso.compInverseIso i).hom.app X = CategoryTheory.CategoryStruct.comp (H.inverse.toPrefunctor.map (i.hom.app X)) (H.unitIso.inv.app (G.toPrefunctor.obj X))
                                                      @[simp]
                                                      theorem CategoryTheory.Iso.compInverseIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D E} (i : F CategoryTheory.Functor.comp G H.functor) (X : C) :
                                                      (CategoryTheory.Iso.compInverseIso i).inv.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.toPrefunctor.obj X)) (H.inverse.toPrefunctor.map (i.inv.app X))

                                                      Construct an isomorphism F ⋙ H.inverse ≅ G from an isomorphism F ≅ G ⋙ H.functor.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        @[simp]
                                                        @[simp]
                                                        theorem CategoryTheory.Iso.isoCompInverse_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D E} (i : CategoryTheory.Functor.comp G H.functor F) (X : C) :
                                                        (CategoryTheory.Iso.isoCompInverse i).inv.app X = CategoryTheory.CategoryStruct.comp (H.inverse.toPrefunctor.map (i.inv.app X)) (H.unitIso.inv.app (G.toPrefunctor.obj X))
                                                        @[simp]
                                                        theorem CategoryTheory.Iso.isoCompInverse_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D E} (i : CategoryTheory.Functor.comp G H.functor F) (X : C) :
                                                        (CategoryTheory.Iso.isoCompInverse i).hom.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.toPrefunctor.obj X)) (H.inverse.toPrefunctor.map (i.hom.app X))

                                                        Construct an isomorphism G ≅ F ⋙ H.inverse from an isomorphism G ⋙ H.functor ≅ F.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem CategoryTheory.Iso.invCompIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [h : CategoryTheory.IsEquivalence G] (i : F CategoryTheory.Functor.comp G H) (X : D) :
                                                          (CategoryTheory.Iso.invCompIso i).hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app ((CategoryTheory.Functor.inv G).toPrefunctor.obj X)) (H.toPrefunctor.map (CategoryTheory.IsEquivalence.counitIso.hom.app X))
                                                          @[simp]
                                                          theorem CategoryTheory.Iso.invCompIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [h : CategoryTheory.IsEquivalence G] (i : F CategoryTheory.Functor.comp G H) (X : D) :
                                                          (CategoryTheory.Iso.invCompIso i).inv.app X = CategoryTheory.CategoryStruct.comp (H.toPrefunctor.map (CategoryTheory.IsEquivalence.counitIso.inv.app X)) (i.inv.app ((CategoryTheory.Functor.inv G).toPrefunctor.obj X))

                                                          Construct an isomorphism G.inv ⋙ F ≅ H from an isomorphism F ≅ G ⋙ H.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.Iso.inverseCompIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C D} (i : F CategoryTheory.Functor.comp G.functor H) (X : D) :
                                                            (CategoryTheory.Iso.inverseCompIso i).hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.toPrefunctor.obj X)) (H.toPrefunctor.map (G.counitIso.hom.app X))
                                                            @[simp]
                                                            theorem CategoryTheory.Iso.inverseCompIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C D} (i : F CategoryTheory.Functor.comp G.functor H) (X : D) :
                                                            (CategoryTheory.Iso.inverseCompIso i).inv.app X = CategoryTheory.CategoryStruct.comp (H.toPrefunctor.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.toPrefunctor.obj X))

                                                            Construct an isomorphism G.inverse ⋙ F ≅ H from an isomorphism F ≅ G.functor ⋙ H.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              @[simp]
                                                              @[simp]
                                                              theorem CategoryTheory.Iso.isoInverseComp_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C D} (i : CategoryTheory.Functor.comp G.functor H F) (X : D) :
                                                              (CategoryTheory.Iso.isoInverseComp i).inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.toPrefunctor.obj X)) (H.toPrefunctor.map (G.counitIso.hom.app X))
                                                              @[simp]
                                                              theorem CategoryTheory.Iso.isoInverseComp_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C D} (i : CategoryTheory.Functor.comp G.functor H F) (X : D) :
                                                              (CategoryTheory.Iso.isoInverseComp i).hom.app X = CategoryTheory.CategoryStruct.comp (H.toPrefunctor.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.toPrefunctor.obj X))

                                                              Construct an isomorphism H ≅ G.inverse ⋙ F from an isomorphism G.functor ⋙ H ≅ F.

                                                              Equations
                                                              Instances For