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.

theorem CategoryTheory.Equivalence.ext {C : Type u₁} {D : Type u₂} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} (x y : C D), x.functor = y.functorx.inverse = y.inverseHEq x.unitIso y.unitIsoHEq x.counitIso y.counitIsox = y
theorem CategoryTheory.Equivalence.ext_iff {C : Type u₁} {D : Type u₂} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} (x y : C D), x = y x.functor = y.functor x.inverse = y.inverse HEq x.unitIso y.unitIso HEq x.counitIso y.counitIso
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 https://stacks.math.columbia.edu/tag/001J

Instances For
    theorem CategoryTheory.Equivalence.functor_unitIso_comp {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C D) (X : C) :
    CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryTheory.CategoryStruct.id (self.functor.obj X)

    The natural isomorphisms compose to the identity.

    We infix the usual notation for an equivalence

    Equations
    Instances For
      @[reducible, inline]

      The unit of an equivalence of categories.

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

        The counit of an equivalence of categories.

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

          The inverse of the unit of an equivalence of categories.

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

            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 functor.comp inverse) (counit_iso : inverse.comp functor CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) :
              { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.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 functor.comp inverse) (counit_iso : inverse.comp functor CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) :
              { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.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 functor.comp inverse) (counit_iso : inverse.comp functor CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) :
              { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.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 functor.comp inverse) (counit_iso : inverse.comp functor CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) :
              { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.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.obj X Z) :
              CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (CategoryTheory.CategoryStruct.comp (e.counit.app (e.functor.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.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) = CategoryTheory.CategoryStruct.id (e.functor.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.obj X Z) :
              CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (CategoryTheory.CategoryStruct.comp (e.functor.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.obj X)) (e.functor.map (e.unitInv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.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.obj X) = e.functor.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.obj X) = e.functor.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.obj Y Z) :
              CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (CategoryTheory.CategoryStruct.comp (e.inverse.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.obj Y)) (e.inverse.map (e.counit.app Y)) = CategoryTheory.CategoryStruct.id (e.inverse.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.obj Y Z) :
              CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app (e.inverse.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.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) = CategoryTheory.CategoryStruct.id (e.inverse.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.obj Y) = e.inverse.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.obj Y) = e.inverse.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.obj (e.inverse.obj Y) Z) :
              @[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.map (e.inverse.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.obj (e.functor.obj Y) Z) :
              @[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.map (e.functor.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_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                  CategoryTheory.Equivalence.refl.functor = CategoryTheory.Functor.id C
                  @[simp]
                  theorem CategoryTheory.Equivalence.refl_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                  CategoryTheory.Equivalence.refl.inverse = 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.instInhabited = { 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
                    • e.symm = { functor := e.inverse, inverse := e.functor, unitIso := e.counitIso.symm, counitIso := e.unitIso.symm, functor_unitIso_comp := }
                    Instances For
                      @[simp]
                      @[simp]
                      theorem CategoryTheory.Equivalence.trans_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C D) (f : D E) :
                      (e.trans f).inverse = f.inverse.comp e.inverse
                      @[simp]
                      theorem CategoryTheory.Equivalence.trans_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C D) (f : D E) :
                      (e.trans f).functor = e.functor.comp f.functor

                      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
                        Instances For
                          @[simp]
                          theorem CategoryTheory.Equivalence.funInvIdAssoc_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] (e : C D) (F : CategoryTheory.Functor C E) (X : C) :
                          (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)
                          @[simp]
                          theorem CategoryTheory.Equivalence.funInvIdAssoc_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] (e : C D) (F : CategoryTheory.Functor C E) (X : C) :
                          (e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)

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

                          Equations
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Equivalence.invFunIdAssoc_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] (e : C D) (F : CategoryTheory.Functor D E) (X : D) :
                            (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
                            @[simp]
                            theorem CategoryTheory.Equivalence.invFunIdAssoc_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] (e : C D) (F : CategoryTheory.Functor D E) (X : D) :
                            (e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app X)

                            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
                              @[simp]
                              theorem CategoryTheory.Equivalence.congrRight_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C D) :
                              e.congrRight.unitIso = CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor E C) => F.rightUnitor.symm ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso ≪≫ F.associator e.functor e.inverse) ) (CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor E D) => F.associator e.inverse e.functor ≪≫ CategoryTheory.isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor) )
                              @[simp]
                              theorem CategoryTheory.Equivalence.congrRight_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C D) :
                              e.congrRight.counitIso = CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor E D) => F.associator e.inverse e.functor ≪≫ CategoryTheory.isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor)

                              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.obj (e.functor.obj Y)) (f' : X e.inverse.obj (e.functor.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.obj (e.inverse.obj Y)) (f' : X e.functor.obj (e.inverse.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
                                • e.powNat 0 = CategoryTheory.Equivalence.refl
                                • e.powNat 1 = e
                                • e.powNat n.succ.succ = e.trans (e.powNat (n + 1))
                                Instances For

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

                                  Equations
                                  Instances For
                                    Equations
                                    • CategoryTheory.Equivalence.instPowInt = { 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]

                                    The functor of an equivalence of categories is essentially surjective.

                                    See https://stacks.math.columbia.edu/tag/02C3.

                                    Equations
                                    • =
                                    Equations
                                    • =

                                    The functor of an equivalence of categories is fully faithful.

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

                                      The inverse of an equivalence of categories is fully faithful.

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

                                        The functor of an equivalence of categories is faithful.

                                        See https://stacks.math.columbia.edu/tag/02C3.

                                        Equations
                                        • =
                                        Equations
                                        • =

                                        The functor of an equivalence of categories is full.

                                        See https://stacks.math.columbia.edu/tag/02C3.

                                        Equations
                                        • =
                                        Equations
                                        • =
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.changeFunctor_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor C D} (iso : e.functor G) :
                                        (e.changeFunctor iso).inverse = e.inverse
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.changeFunctor_counitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor C D} (iso : e.functor G) (X : D) :
                                        (e.changeFunctor iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor C D} (iso : e.functor G) (X : C) :
                                        (e.changeFunctor iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.changeFunctor_counitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor C D} (iso : e.functor G) (X : D) :
                                        (e.changeFunctor iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.hom.app X)
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.changeFunctor_unitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor C D} (iso : e.functor G) (X : C) :
                                        (e.changeFunctor iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.changeFunctor_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor C D} (iso : e.functor G) :
                                        (e.changeFunctor iso).functor = G

                                        If e : C ≌ D is an equivalence of categories, and iso : e.functor ≅ G is an isomorphism, then there is an equivalence of categories whose functor is G.

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

                                          Compatibility of changeFunctor with identity isomorphisms of functors

                                          theorem CategoryTheory.Equivalence.changeFunctor_trans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor C D} {G' : CategoryTheory.Functor C D} (iso₁ : e.functor G) (iso₂ : G G') :
                                          (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

                                          Compatibility of changeFunctor with the composition of isomorphisms of functors

                                          @[simp]
                                          theorem CategoryTheory.Equivalence.changeInverse_unitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor D C} (iso : e.inverse G) (X : C) :
                                          (e.changeInverse iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.functor.obj X)) (e.unitIso.inv.app X)
                                          @[simp]
                                          theorem CategoryTheory.Equivalence.changeInverse_counitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor D C} (iso : e.inverse G) (X : D) :
                                          (e.changeInverse iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)
                                          @[simp]
                                          theorem CategoryTheory.Equivalence.changeInverse_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor D C} (iso : e.inverse G) :
                                          (e.changeInverse iso).inverse = G
                                          @[simp]
                                          theorem CategoryTheory.Equivalence.changeInverse_counitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor D C} (iso : e.inverse G) (X : D) :
                                          (e.changeInverse iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))
                                          @[simp]
                                          theorem CategoryTheory.Equivalence.changeInverse_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor D C} (iso : e.inverse G) :
                                          (e.changeInverse iso).functor = e.functor
                                          @[simp]
                                          theorem CategoryTheory.Equivalence.changeInverse_unitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor D C} (iso : e.inverse G) (X : C) :
                                          (e.changeInverse iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))

                                          If e : C ≌ D is an equivalence of categories, and iso : e.functor ≅ G is an isomorphism, then there is an equivalence of categories whose inverse is G.

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

                                            A functor is an equivalence of categories if it is faithful, full and essentially surjective.

                                            • faithful : F.Faithful
                                            • full : F.Full
                                            • essSurj : F.EssSurj
                                            Instances
                                              Equations
                                              • =
                                              Equations
                                              • =

                                              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.

                                              A quasi-inverse D ⥤ C to a functor that F : C ⥤ D that is an equivalence, i.e. faithful, full, and essentially surjective.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.Functor.asEquivalence_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] :
                                                F.asEquivalence.functor = F

                                                Interpret a functor that is an equivalence as an equivalence.

                                                See https://stacks.math.columbia.edu/tag/02C3.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  • =
                                                  instance CategoryTheory.Functor.isEquivalence_trans {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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [G.IsEquivalence] :
                                                  (F.comp G).IsEquivalence
                                                  Equations
                                                  • =
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.fun_inv_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : D) (Y : D) (f : X Y) :
                                                  F.map (F.inv.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.inv_fun_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : C) (Y : C) (f : X Y) :
                                                  F.inv.map (F.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.unit.app Y))
                                                  theorem CategoryTheory.Functor.isEquivalence_of_comp_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.IsEquivalence] [(F.comp G).IsEquivalence] :
                                                  F.IsEquivalence

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

                                                  theorem CategoryTheory.Functor.isEquivalence_of_comp_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [(F.comp G).IsEquivalence] :
                                                  G.IsEquivalence

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

                                                  noncomputable instance CategoryTheory.Equivalence.inducedFunctorOfEquiv {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u_1} (e : C' D) :
                                                  (CategoryTheory.inducedFunctor e).IsEquivalence
                                                  Equations
                                                  • =
                                                  noncomputable instance CategoryTheory.Equivalence.fullyFaithfulToEssImage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] :
                                                  F.toEssImage.IsEquivalence
                                                  Equations
                                                  • =
                                                  @[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 G.comp H.functor) (X : C) :
                                                  i.compInverseIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.app X))
                                                  @[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 G.comp H.functor) (X : C) :
                                                  i.compInverseIso.hom.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))

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

                                                  Equations
                                                  Instances For
                                                    @[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 : G.comp H.functor F) (X : C) :
                                                    i.isoCompInverse.inv.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.inv.app X)) (H.unitIso.inv.app (G.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 : G.comp H.functor F) (X : C) :
                                                    i.isoCompInverse.hom.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.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.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 G.functor.comp H) (X : D) :
                                                      i.inverseCompIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj X))
                                                      @[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 G.functor.comp H) (X : D) :
                                                      i.inverseCompIso.hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))

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

                                                      Equations
                                                      Instances For
                                                        @[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 : G.functor.comp H F) (X : D) :
                                                        i.isoInverseComp.inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.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 : G.functor.comp H F) (X : D) :
                                                        i.isoInverseComp.hom.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))

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

                                                        Equations
                                                        Instances For
                                                          @[deprecated CategoryTheory.Functor.IsEquivalence]

                                                          Alias of CategoryTheory.Functor.IsEquivalence.


                                                          A functor is an equivalence of categories if it is faithful, full and essentially surjective.

                                                          Equations
                                                          Instances For
                                                            @[deprecated CategoryTheory.Functor.fun_inv_map]
                                                            theorem CategoryTheory.IsEquivalence.fun_inv_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : D) (Y : D) (f : X Y) :
                                                            F.map (F.inv.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))

                                                            Alias of CategoryTheory.Functor.fun_inv_map.

                                                            @[deprecated CategoryTheory.Functor.inv_fun_map]
                                                            theorem CategoryTheory.IsEquivalence.inv_fun_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : C) (Y : C) (f : X Y) :
                                                            F.inv.map (F.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.unit.app Y))

                                                            Alias of CategoryTheory.Functor.inv_fun_map.

                                                            @[deprecated CategoryTheory.Equivalence.changeFunctor]

                                                            Alias of CategoryTheory.Equivalence.changeFunctor.


                                                            If e : C ≌ D is an equivalence of categories, and iso : e.functor ≅ G is an isomorphism, then there is an equivalence of categories whose functor is G.

                                                            Equations
                                                            Instances For
                                                              @[deprecated CategoryTheory.Equivalence.changeFunctor_trans]
                                                              theorem CategoryTheory.IsEquivalence.ofIso_trans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) {G : CategoryTheory.Functor C D} {G' : CategoryTheory.Functor C D} (iso₁ : e.functor G) (iso₂ : G G') :
                                                              (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

                                                              Alias of CategoryTheory.Equivalence.changeFunctor_trans.


                                                              Compatibility of changeFunctor with the composition of isomorphisms of functors

                                                              @[deprecated CategoryTheory.Equivalence.changeFunctor_refl]

                                                              Alias of CategoryTheory.Equivalence.changeFunctor_refl.


                                                              Compatibility of changeFunctor with identity isomorphisms of functors

                                                              @[deprecated CategoryTheory.Functor.isEquivalence_iff_of_iso]

                                                              Alias of CategoryTheory.Functor.isEquivalence_iff_of_iso.

                                                              @[deprecated CategoryTheory.Functor.isEquivalence_of_comp_right]
                                                              theorem CategoryTheory.IsEquivalence.cancelCompRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.IsEquivalence] [(F.comp G).IsEquivalence] :
                                                              F.IsEquivalence

                                                              Alias of CategoryTheory.Functor.isEquivalence_of_comp_right.


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

                                                              @[deprecated CategoryTheory.Functor.isEquivalence_of_comp_left]
                                                              theorem CategoryTheory.IsEquivalence.cancelCompLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [(F.comp G).IsEquivalence] :
                                                              G.IsEquivalence

                                                              Alias of CategoryTheory.Functor.isEquivalence_of_comp_left.


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