# mathlibdocumentation

category_theory.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 isomorphims 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

• if one of the two compositions is the identity, then so is the other, and
• given an equivalence of categories, it is always possible to refine Ī· in such a way that the identities are satisfied.

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 #

• equivalence: bundled (half-)adjoint equivalences of categories
• is_equivalence: type class on a functor F containing the data of the inverse G as well as the natural isomorphisms Ī· and Īµ.
• ess_surj: type class on a functor F containing the data of the preimages and the isomorphisms F.obj (preimage d) ā d.

## Main results #

• equivalence.mk: upgrade an equivalence to a (half-)adjoint equivalence
• is_equivalence.equiv_of_iso: when F and G are isomorphic functors, F is an equivalence iff G is.
• equivalence.of_fully_faithfully_ess_surj: a fully faithful essentially surjective functor is an equivalence.

## Notations #

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

structure category_theory.equivalence (C : Type uā) (D : Type uā)  :
Type (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.

Instances for category_theory.equivalence
theorem category_theory.equivalence.functor_unit_iso_comp {C : Type uā} {D : Type uā} (self : C ā D) (X : C) :
self.functor.map (self.unit_iso.hom.app X) ā« self.counit_iso.hom.app (self.functor.obj X) = š (self.functor.obj X)
@[reducible]
def category_theory.equivalence.unit {C : Type uā} {D : Type uā} (e : C ā D) :

The unit of an equivalence of categories.

@[reducible]
def category_theory.equivalence.counit {C : Type uā} {D : Type uā} (e : C ā D) :

The counit of an equivalence of categories.

@[reducible]
def category_theory.equivalence.unit_inv {C : Type uā} {D : Type uā} (e : C ā D) :

The inverse of the unit of an equivalence of categories.

@[reducible]
def category_theory.equivalence.counit_inv {C : Type uā} {D : Type uā} (e : C ā D) :

The inverse of the counit of an equivalence of categories.

@[simp]
theorem category_theory.equivalence.equivalence_mk'_unit {C : Type uā} {D : Type uā} (functor : C ā„¤ D) (inverse : D ā„¤ C) (unit_iso : š­ C ā functor ā inverse) (counit_iso : inverse ā functor ā š­ D) (f : (ā (X : C), functor.map (unit_iso.hom.app X) ā« counit_iso.hom.app (functor.obj X) = š (functor.obj X)) . "obviously") :
{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.unit = unit_iso.hom
@[simp]
theorem category_theory.equivalence.equivalence_mk'_counit {C : Type uā} {D : Type uā} (functor : C ā„¤ D) (inverse : D ā„¤ C) (unit_iso : š­ C ā functor ā inverse) (counit_iso : inverse ā functor ā š­ D) (f : (ā (X : C), functor.map (unit_iso.hom.app X) ā« counit_iso.hom.app (functor.obj X) = š (functor.obj X)) . "obviously") :
{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.counit = counit_iso.hom
@[simp]
theorem category_theory.equivalence.equivalence_mk'_unit_inv {C : Type uā} {D : Type uā} (functor : C ā„¤ D) (inverse : D ā„¤ C) (unit_iso : š­ C ā functor ā inverse) (counit_iso : inverse ā functor ā š­ D) (f : (ā (X : C), functor.map (unit_iso.hom.app X) ā« counit_iso.hom.app (functor.obj X) = š (functor.obj X)) . "obviously") :
{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.unit_inv = unit_iso.inv
@[simp]
theorem category_theory.equivalence.equivalence_mk'_counit_inv {C : Type uā} {D : Type uā} (functor : C ā„¤ D) (inverse : D ā„¤ C) (unit_iso : š­ C ā functor ā inverse) (counit_iso : inverse ā functor ā š­ D) (f : (ā (X : C), functor.map (unit_iso.hom.app X) ā« counit_iso.hom.app (functor.obj X) = š (functor.obj X)) . "obviously") :
{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.counit_inv = counit_iso.inv
@[simp]
theorem category_theory.equivalence.functor_unit_comp {C : Type uā} {D : Type uā} (e : C ā D) (X : C) :
@[simp]
theorem category_theory.equivalence.counit_inv_functor_comp {C : Type uā} {D : Type uā} (e : C ā D) (X : C) :
theorem category_theory.equivalence.counit_inv_app_functor {C : Type uā} {D : Type uā} (e : C ā D) (X : C) :
theorem category_theory.equivalence.counit_app_functor {C : Type uā} {D : Type uā} (e : C ā D) (X : C) :
@[simp]
theorem category_theory.equivalence.unit_inverse_comp {C : Type uā} {D : Type uā} (e : C ā D) (Y : D) :

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

@[simp]
theorem category_theory.equivalence.inverse_counit_inv_comp {C : Type uā} {D : Type uā} (e : C ā D) (Y : D) :
theorem category_theory.equivalence.unit_app_inverse {C : Type uā} {D : Type uā} (e : C ā D) (Y : D) :
theorem category_theory.equivalence.unit_inv_app_inverse {C : Type uā} {D : Type uā} (e : C ā D) (Y : D) :
@[simp]
theorem category_theory.equivalence.fun_inv_map {C : Type uā} {D : Type uā} (e : C ā D) (X Y : D) (f : X ā¶ Y) :
@[simp]
theorem category_theory.equivalence.inv_fun_map {C : Type uā} {D : Type uā} (e : C ā D) (X Y : C) (f : X ā¶ Y) :
def category_theory.equivalence.adjointify_Ī· {C : Type uā} {D : Type uā} {F : C ā„¤ D} {G : D ā„¤ C} (Ī· : š­ C ā F ā G) (Īµ : G ā F ā š­ D) :

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
theorem category_theory.equivalence.adjointify_Ī·_Īµ {C : Type uā} {D : Type uā} {F : C ā„¤ D} {G : D ā„¤ C} (Ī· : š­ C ā F ā G) (Īµ : G ā F ā š­ D) (X : C) :
F.map X) ā« Īµ.hom.app (F.obj X) = š (F.obj X)
@[protected]
def category_theory.equivalence.mk {C : Type uā} {D : Type uā} (F : C ā„¤ D) (G : D ā„¤ C) (Ī· : š­ C ā F ā G) (Īµ : G ā F ā š­ D) :
C ā D

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
@[simp]
theorem category_theory.equivalence.refl_counit_iso {C : Type uā}  :
@[simp]
theorem category_theory.equivalence.refl_inverse {C : Type uā}  :
@[simp]
theorem category_theory.equivalence.refl_unit_iso {C : Type uā}  :
@[refl]
def category_theory.equivalence.refl {C : Type uā}  :
C ā C

Equivalence of categories is reflexive.

Equations
@[simp]
theorem category_theory.equivalence.refl_functor {C : Type uā}  :
@[protected, instance]
def category_theory.equivalence.inhabited {C : Type uā}  :
Equations
@[simp]
theorem category_theory.equivalence.symm_inverse {C : Type uā} {D : Type uā} (e : C ā D) :
@[simp]
theorem category_theory.equivalence.symm_functor {C : Type uā} {D : Type uā} (e : C ā D) :
@[symm]
def category_theory.equivalence.symm {C : Type uā} {D : Type uā} (e : C ā D) :
D ā C

Equivalence of categories is symmetric.

Equations
@[simp]
theorem category_theory.equivalence.symm_unit_iso {C : Type uā} {D : Type uā} (e : C ā D) :
@[simp]
theorem category_theory.equivalence.symm_counit_iso {C : Type uā} {D : Type uā} (e : C ā D) :
@[trans]
def category_theory.equivalence.trans {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (f : D ā E) :
C ā E

Equivalence of categories is transitive.

Equations
@[simp]
theorem category_theory.equivalence.trans_functor {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (f : D ā E) :
(e.trans f).functor =
@[simp]
theorem category_theory.equivalence.trans_counit_iso {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (f : D ā E) :
@[simp]
theorem category_theory.equivalence.trans_inverse {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (f : D ā E) :
(e.trans f).inverse =
@[simp]
theorem category_theory.equivalence.trans_unit_iso {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (f : D ā E) :
def category_theory.equivalence.fun_inv_id_assoc {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (F : C ā„¤ E) :

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

Equations
@[simp]
theorem category_theory.equivalence.fun_inv_id_assoc_hom_app {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (F : C ā„¤ E) (X : C) :
@[simp]
theorem category_theory.equivalence.fun_inv_id_assoc_inv_app {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (F : C ā„¤ E) (X : C) :
(e.fun_inv_id_assoc F).inv.app X = F.map (e.unit.app X)
def category_theory.equivalence.inv_fun_id_assoc {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (F : D ā„¤ E) :

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

Equations
@[simp]
theorem category_theory.equivalence.inv_fun_id_assoc_hom_app {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (F : D ā„¤ E) (X : D) :
@[simp]
theorem category_theory.equivalence.inv_fun_id_assoc_inv_app {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) (F : D ā„¤ E) (X : D) :
@[simp]
theorem category_theory.equivalence.congr_left_counit_iso {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :
@[simp]
theorem category_theory.equivalence.congr_left_unit_iso {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :
@[simp]
theorem category_theory.equivalence.congr_left_functor {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :
def category_theory.equivalence.congr_left {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :

If C is equivalent to D, then C ā„¤ E is equivalent to D ā„¤ E.

Equations
@[simp]
theorem category_theory.equivalence.congr_left_inverse {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :
@[simp]
theorem category_theory.equivalence.congr_right_counit_iso {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :
def category_theory.equivalence.congr_right {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :

If C is equivalent to D, then E ā„¤ C is equivalent to E ā„¤ D.

Equations
@[simp]
theorem category_theory.equivalence.congr_right_functor {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :
@[simp]
theorem category_theory.equivalence.congr_right_unit_iso {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :
@[simp]
theorem category_theory.equivalence.congr_right_inverse {C : Type uā} {D : Type uā} {E : Type uā} (e : C ā D) :
@[simp]
theorem category_theory.equivalence.cancel_unit_right {C : Type uā} {D : Type uā} (e : C ā D) {X Y : C} (f f' : X ā¶ Y) :
f ā« e.unit.app Y = f' ā« e.unit.app Y ā f = f'
@[simp]
theorem category_theory.equivalence.cancel_unit_inv_right {C : Type uā} {D : Type uā} (e : C ā D) {X Y : C} (f f' : X ā¶ e.inverse.obj (e.functor.obj Y)) :
@[simp]
theorem category_theory.equivalence.cancel_counit_right {C : Type uā} {D : Type uā} (e : C ā D) {X Y : D} (f f' : X ā¶ e.functor.obj (e.inverse.obj Y)) :
f ā« e.counit.app Y = f' ā« e.counit.app Y ā f = f'
@[simp]
theorem category_theory.equivalence.cancel_counit_inv_right {C : Type uā} {D : Type uā} (e : C ā D) {X Y : D} (f f' : X ā¶ Y) :
@[simp]
theorem category_theory.equivalence.cancel_unit_right_assoc {C : Type uā} {D : Type uā} (e : C ā D) {W X X' Y : C} (f : W ā¶ X) (g : X ā¶ Y) (f' : W ā¶ X') (g' : X' ā¶ Y) :
f ā« g ā« e.unit.app Y = f' ā« g' ā« e.unit.app Y ā f ā« g = f' ā« g'
@[simp]
theorem category_theory.equivalence.cancel_counit_inv_right_assoc {C : Type uā} {D : Type uā} (e : C ā D) {W X X' Y : D} (f : W ā¶ X) (g : X ā¶ Y) (f' : W ā¶ X') (g' : X' ā¶ Y) :
@[simp]
theorem category_theory.equivalence.cancel_unit_right_assoc' {C : Type uā} {D : Type uā} (e : C ā D) {W X X' Y Y' Z : C} (f : W ā¶ X) (g : X ā¶ Y) (h : Y ā¶ Z) (f' : W ā¶ X') (g' : X' ā¶ Y') (h' : Y' ā¶ Z) :
@[simp]
theorem category_theory.equivalence.cancel_counit_inv_right_assoc' {C : Type uā} {D : Type uā} (e : C ā D) {W X X' Y Y' Z : D} (f : W ā¶ X) (g : X ā¶ Y) (h : Y ā¶ Z) (f' : W ā¶ X') (g' : X' ā¶ Y') (h' : Y' ā¶ Z) :
def category_theory.equivalence.pow_nat {C : Type uā} (e : C ā C) :
ā ā (C ā C)

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

Equations
def category_theory.equivalence.pow {C : Type uā} (e : C ā C) :
ā¤ ā (C ā C)

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

Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.equivalence.pow_zero {C : Type uā} (e : C ā C) :
@[simp]
theorem category_theory.equivalence.pow_one {C : Type uā} (e : C ā C) :
e ^ 1 = e
@[simp]
theorem category_theory.equivalence.pow_neg_one {C : Type uā} (e : C ā C) :
e ^ -1 = e.symm
@[class]
structure category_theory.is_equivalence {C : Type uā} {D : Type uā} (F : C ā„¤ D) :
Type (max uā uā vā vā)
• inverse : D ā„¤ C
• unit_iso :
• counit_iso :
• functor_unit_iso_comp' : (ā (X : C), = š (F.obj X)) . "obviously"

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

Instances of this typeclass
Instances of other typeclasses for category_theory.is_equivalence
• category_theory.is_equivalence.has_sizeof_inst
@[simp]
theorem category_theory.is_equivalence.functor_unit_iso_comp {C : Type uā} {D : Type uā} {F : C ā„¤ D} [self : category_theory.is_equivalence F] (X : C) :
@[simp]
theorem category_theory.is_equivalence.functor_unit_iso_comp_assoc {C : Type uā} {D : Type uā} {F : C ā„¤ D} [self : category_theory.is_equivalence F] (X : C) {X' : D} (f' : F.obj X ā¶ X') :
@[protected, instance]
def category_theory.is_equivalence.of_equivalence {C : Type uā} {D : Type uā} (F : C ā D) :
Equations
@[protected, instance]
def category_theory.is_equivalence.of_equivalence_inverse {C : Type uā} {D : Type uā} (F : C ā D) :
Equations
@[protected]
def category_theory.is_equivalence.mk {C : Type uā} {D : Type uā} {F : C ā„¤ D} (G : D ā„¤ C) (Ī· : š­ C ā F ā G) (Īµ : G ā F ā š­ D) :

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
def category_theory.functor.as_equivalence {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :
C ā D

Interpret a functor that is an equivalence as an equivalence.

Equations
@[protected, instance]
def category_theory.functor.is_equivalence_refl {C : Type uā}  :
Equations
def category_theory.functor.inv {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :

The inverse functor of a functor that is an equivalence.

Equations
Instances for category_theory.functor.inv
@[protected, instance]
def category_theory.functor.is_equivalence_inv {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :
Equations
@[simp]
theorem category_theory.functor.as_equivalence_functor {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :
@[simp]
theorem category_theory.functor.as_equivalence_inverse {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :
@[simp]
theorem category_theory.functor.as_equivalence_unit {C : Type uā} {D : Type uā} {F : C ā„¤ D}  :
@[simp]
theorem category_theory.functor.as_equivalence_counit {C : Type uā} {D : Type uā} {F : C ā„¤ D}  :
@[simp]
theorem category_theory.functor.inv_inv {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :
F.inv.inv = F
@[protected, instance]
def category_theory.functor.is_equivalence_trans {C : Type uā} {D : Type uā} {E : Type uā} (F : C ā„¤ D) (G : D ā„¤ E)  :
Equations
@[simp]
theorem category_theory.equivalence.functor_inv {C : Type uā} {D : Type uā} (E : C ā D) :
@[simp]
theorem category_theory.equivalence.inverse_inv {C : Type uā} {D : Type uā} (E : C ā D) :
@[simp]
theorem category_theory.equivalence.functor_as_equivalence {C : Type uā} {D : Type uā} (E : C ā D) :
@[simp]
theorem category_theory.equivalence.inverse_as_equivalence {C : Type uā} {D : Type uā} (E : C ā D) :
@[simp]
theorem category_theory.is_equivalence.fun_inv_map {C : Type uā} {D : Type uā} (F : C ā„¤ D) (X Y : D) (f : X ā¶ Y) :
F.map (F.inv.map f) = ā«
@[simp]
theorem category_theory.is_equivalence.inv_fun_map {C : Type uā} {D : Type uā} (F : C ā„¤ D) (X Y : C) (f : X ā¶ Y) :
F.inv.map (F.map f) = ā« f ā«
def category_theory.is_equivalence.of_iso {C : Type uā} {D : Type uā} {F G : C ā„¤ D} (e : F ā G)  :

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

Equations
@[simp]
theorem category_theory.is_equivalence.of_iso_counit_iso {C : Type uā} {D : Type uā} {F G : C ā„¤ D} (e : F ā G)  :
@[simp]
theorem category_theory.is_equivalence.of_iso_inverse {C : Type uā} {D : Type uā} {F G : C ā„¤ D} (e : F ā G)  :
@[simp]
theorem category_theory.is_equivalence.of_iso_unit_iso {C : Type uā} {D : Type uā} {F G : C ā„¤ D} (e : F ā G)  :
theorem category_theory.is_equivalence.of_iso_trans {C : Type uā} {D : Type uā} {F G H : C ā„¤ D} (e : F ā G) (e' : G ā H)  :

Compatibility of of_iso with the composition of isomorphisms of functors

theorem category_theory.is_equivalence.of_iso_refl {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :

Compatibility of of_iso with identity isomorphisms of functors

def category_theory.is_equivalence.equiv_of_iso {C : Type uā} {D : Type uā} {F G : C ā„¤ D} (e : F ā G) :

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

Equations
@[simp]
theorem category_theory.is_equivalence.equiv_of_iso_symm_apply {C : Type uā} {D : Type uā} {F G : C ā„¤ D} (e : F ā G)  :
@[simp]
theorem category_theory.is_equivalence.equiv_of_iso_apply {C : Type uā} {D : Type uā} {F G : C ā„¤ D} (e : F ā G)  :
@[simp]
def category_theory.is_equivalence.cancel_comp_right {C : Type uā} {D : Type uā} {E : Type u_1} (F : C ā„¤ D) (G : D ā„¤ E) (hGF : category_theory.is_equivalence (F ā G)) :

If G and F ā G are equivalence of categories, then F is also an equivalence.

Equations
@[simp]
def category_theory.is_equivalence.cancel_comp_left {C : Type uā} {D : Type uā} {E : Type u_1} (F : C ā„¤ D) (G : D ā„¤ E) (hGF : category_theory.is_equivalence (F ā G)) :

If F and F ā G are equivalence of categories, then G is also an equivalence.

Equations
theorem category_theory.equivalence.ess_surj_of_equivalence {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :

An equivalence is essentially surjective.

@[protected, instance]
def category_theory.equivalence.faithful_of_equivalence {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :

An equivalence is faithful.

@[protected, instance]
def category_theory.equivalence.full_of_equivalence {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :

An equivalence is full.

Equations
noncomputable def category_theory.equivalence.of_fully_faithfully_ess_surj {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :

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

Equations
@[simp]
theorem category_theory.equivalence.functor_map_inj_iff {C : Type uā} {D : Type uā} (e : C ā D) {X Y : C} (f g : X ā¶ Y) :
@[simp]
theorem category_theory.equivalence.inverse_map_inj_iff {C : Type uā} {D : Type uā} (e : C ā D) {X Y : D} (f g : X ā¶ Y) :
@[protected, instance]
def category_theory.equivalence.ess_surj_induced_functor {D : Type uā} {C' : Type u_1} (e : C' ā D) :
@[protected, instance]
noncomputable def category_theory.equivalence.induced_functor_of_equiv {D : Type uā} {C' : Type u_1} (e : C' ā D) :
Equations
@[protected, instance]
noncomputable def category_theory.equivalence.fully_faithful_to_ess_image {C : Type uā} {D : Type uā} (F : C ā„¤ D)  :
Equations