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

• 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
• IsEquivalence: type class on a functor F containing the data of the inverse G as well as the natural isomorphisms η and ε.
• EssSurj: 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
• IsEquivalence.equivOfIso: when F and G are isomorphic functors, F is an equivalence iff G is.
• Equivalence.ofFullyFaithfullyEssSurj: 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 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₂)

• mk' :: (
• functor : CategoryTheory.Functor C D

  A functor in one direction

• inverse : CategoryTheory.Functor D C

  A functor in the other direction

• unitIso : CategoryTheory.Functor.id C ≅ CategoryTheory.Functor.comp s.functor s.inverse

  The composition functor ⋙ inverse is isomorphic to the identity

• counitIso : CategoryTheory.Functor.comp s.inverse s.functor ≅ CategoryTheory.Functor.id D

  The composition inverse ⋙ functor is also isomorphic to the identity

• functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.functor.map (s.unitIso.hom.app X)) (s.counitIso.hom.app (s.functor.obj X)) = CategoryTheory.CategoryStruct.id (s.functor.obj X)

  The natural isomorphisms compose to the identity.

• )

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

def CategoryTheory.«term_≌_» : Lean.TrailingParserDescr

We infix the usual notation for an equivalence

Equations

• CategoryTheory.«term_≌_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_≌_ 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≌ ") (Lean.ParserDescr.cat `term 10))

@[inline, reducible]

abbrev CategoryTheory.Equivalence.unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Functor.id C ⟶ CategoryTheory.Functor.comp e.functor e.inverse

The unit of an equivalence of categories.

Equations

• e.unit = e.unitIso.hom

@[inline, reducible]

abbrev CategoryTheory.Equivalence.counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Functor.comp e.inverse e.functor ⟶ CategoryTheory.Functor.id D

The counit of an equivalence of categories.

Equations

• e.counit = e.counitIso.hom

@[inline, reducible]

abbrev CategoryTheory.Equivalence.unitInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Functor.comp e.functor e.inverse ⟶ CategoryTheory.Functor.id C

The inverse of the unit of an equivalence of categories.

Equations

• e.unitInv = e.unitIso.inv

@[inline, reducible]

abbrev CategoryTheory.Equivalence.counitInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Functor.id D ⟶ CategoryTheory.Functor.comp e.inverse e.functor

The inverse of the counit of an equivalence of categories.

Equations

• e.counitInv = e.counitIso.inv

@[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.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.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.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.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.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.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.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : (CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).counitInv = counit_iso.inv

@[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 {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 {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 {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)

@[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))

@[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))

def CategoryTheory.Equivalence.adjointifyη {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ CategoryTheory.Functor.comp F G) (ε : CategoryTheory.Functor.comp G F ≅ CategoryTheory.Functor.id D) : CategoryTheory.Functor.id C ≅ CategoryTheory.Functor.comp F G

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.

theorem CategoryTheory.Equivalence.adjointify_η_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ CategoryTheory.Functor.comp F G) (ε : CategoryTheory.Functor.comp G F ≅ CategoryTheory.Functor.id D) (X : C) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (ε.hom.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Equivalence.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) (η : CategoryTheory.Functor.id C ≅ CategoryTheory.Functor.comp F G) (ε : CategoryTheory.Functor.comp G F ≅ CategoryTheory.Functor.id 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

• CategoryTheory.Equivalence.mk F G η ε = CategoryTheory.Equivalence.mk' F G (CategoryTheory.Equivalence.adjointifyη η ε) ε

@[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_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Equivalence.refl.unitIso = CategoryTheory.Iso.refl (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

@[simp]

theorem CategoryTheory.Equivalence.refl_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Equivalence.refl.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.comp (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C))

def CategoryTheory.Equivalence.refl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : C ≌ C

Equivalence of categories is reflexive.

Equations

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

instance CategoryTheory.Equivalence.instInhabitedEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : Inhabited (C ≌ C)

Equations

• CategoryTheory.Equivalence.instInhabitedEquivalence = { default := CategoryTheory.Equivalence.refl }

@[simp]

theorem CategoryTheory.Equivalence.symm_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.functor = e.inverse

@[simp]

theorem CategoryTheory.Equivalence.symm_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.inverse = e.functor

@[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]

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

def CategoryTheory.Equivalence.symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : D ≌ C

Equivalence of categories is symmetric.

Equations

• e.symm = CategoryTheory.Equivalence.mk' e.inverse e.functor e.counitIso.symm e.unitIso.symm

@[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 = CategoryTheory.Functor.comp f.inverse e.inverse

@[simp]

theorem CategoryTheory.Equivalence.trans_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) (f : D ≌ E) : (e.trans f).counitIso = CategoryTheory.isoWhiskerLeft f.inverse (CategoryTheory.isoWhiskerRight e.counitIso f.functor) ≪≫ f.counitIso

@[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 = CategoryTheory.Functor.comp e.functor f.functor

@[simp]

theorem CategoryTheory.Equivalence.trans_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) (f : D ≌ E) : (e.trans f).unitIso = e.unitIso ≪≫ CategoryTheory.isoWhiskerLeft e.functor (CategoryTheory.isoWhiskerRight f.unitIso e.inverse)

def CategoryTheory.Equivalence.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] (e : C ≌ D) (f : D ≌ E) : C ≌ E

Equivalence of categories is transitive.

Equations

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

def CategoryTheory.Equivalence.funInvIdAssoc {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) : CategoryTheory.Functor.comp e.functor (CategoryTheory.Functor.comp e.inverse F) ≅ F

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.

@[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) : (CategoryTheory.Equivalence.funInvIdAssoc e 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) : (CategoryTheory.Equivalence.funInvIdAssoc e F).inv.app X = F.map (e.unit.app X)

def CategoryTheory.Equivalence.invFunIdAssoc {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) : CategoryTheory.Functor.comp e.inverse (CategoryTheory.Functor.comp e.functor F) ≅ F

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.

@[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) : (CategoryTheory.Equivalence.invFunIdAssoc e 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) : (CategoryTheory.Equivalence.invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X)

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_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) : (CategoryTheory.Equivalence.congrLeft e).functor = (CategoryTheory.whiskeringLeft D C E).obj e.inverse

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_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) : (CategoryTheory.Equivalence.congrLeft e).unitIso = CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents fun F => (CategoryTheory.Equivalence.funInvIdAssoc e F).symm) (CategoryTheory.NatIso.ofComponents fun F => CategoryTheory.Equivalence.invFunIdAssoc e F)

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_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) : (CategoryTheory.Equivalence.congrLeft e).counitIso = CategoryTheory.NatIso.ofComponents fun F => CategoryTheory.Equivalence.invFunIdAssoc e F

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_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) : (CategoryTheory.Equivalence.congrLeft e).inverse = (CategoryTheory.whiskeringLeft C D E).obj e.functor

def CategoryTheory.Equivalence.congrLeft {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) : CategoryTheory.Functor C E ≌ CategoryTheory.Functor D E

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.

@[simp]

theorem CategoryTheory.Equivalence.congrRight_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) : (CategoryTheory.Equivalence.congrRight e).inverse = (CategoryTheory.whiskeringRight E D C).obj e.inverse

@[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) : (CategoryTheory.Equivalence.congrRight e).unitIso = CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents fun F => (CategoryTheory.Functor.rightUnitor F).symm ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso ≪≫ CategoryTheory.Functor.associator F e.functor e.inverse) (CategoryTheory.NatIso.ofComponents fun F => CategoryTheory.Functor.associator F e.inverse e.functor ≪≫ CategoryTheory.isoWhiskerLeft F e.counitIso ≪≫ CategoryTheory.Functor.rightUnitor F)

@[simp]

theorem CategoryTheory.Equivalence.congrRight_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) : (CategoryTheory.Equivalence.congrRight e).functor = (CategoryTheory.whiskeringRight E C D).obj e.functor

@[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) : (CategoryTheory.Equivalence.congrRight e).counitIso = CategoryTheory.NatIso.ofComponents fun F => CategoryTheory.Functor.associator F e.inverse e.functor ≪≫ CategoryTheory.isoWhiskerLeft F e.counitIso ≪≫ CategoryTheory.Functor.rightUnitor F

def CategoryTheory.Equivalence.congrRight {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) : CategoryTheory.Functor E C ≌ CategoryTheory.Functor E D

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.

@[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) : CategoryTheory.CategoryStruct.comp f (e.unit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unit.app Y) ↔ f = f'

@[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)) : CategoryTheory.CategoryStruct.comp f (e.counit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counit.app Y) ↔ f = f'

@[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'

@[simp]

theorem CategoryTheory.Equivalence.cancel_unit_right_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W : C} {X : C} {X' : C} {Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.unit.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.unit.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'

@[simp]

theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W : D} {X : D} {X' : D} {Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.counitInv.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.counitInv.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'

@[simp]

theorem CategoryTheory.Equivalence.cancel_unit_right_assoc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W : C} {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.unit.app Z))) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.unit.app Z))) ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')

@[simp]

theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W : D} {X : D} {X' : D} {Y : D} {Y' : D} {Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.counitInv.app Z))) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.counitInv.app Z))) ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')

def CategoryTheory.Equivalence.powNat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (e : C ≌ C) : ℕ → (C ≌ C)

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

Equations

• CategoryTheory.Equivalence.powNat e 0 = CategoryTheory.Equivalence.refl
• CategoryTheory.Equivalence.powNat e 1 = e
• CategoryTheory.Equivalence.powNat e (Nat.succ (Nat.succ n)) = e.trans (CategoryTheory.Equivalence.powNat e (n + 1))

def CategoryTheory.Equivalence.pow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (e : C ≌ C) : ℤ → (C ≌ C)

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

Equations

• CategoryTheory.Equivalence.pow e x = match x with | Int.ofNat n => CategoryTheory.Equivalence.powNat e n | Int.negSucc n => CategoryTheory.Equivalence.powNat e.symm (n + 1)

instance CategoryTheory.Equivalence.instPowEquivalenceInt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : Pow (C ≌ C) ℤ

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]

theorem CategoryTheory.Equivalence.pow_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (e : C ≌ C) : e ^ 1 = e

@[simp]

theorem CategoryTheory.Equivalence.pow_neg_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (e : C ≌ C) : e ^ (-1) = e.symm

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₂)

• mk' :: (
• inverse : CategoryTheory.Functor D C

  The inverse functor to F

• unitIso : CategoryTheory.Functor.id C ≅ CategoryTheory.Functor.comp F (CategoryTheory.IsEquivalence.inverse F)

  Composition F ⋙ inverse is isomorphic to the identity.

• counitIso : CategoryTheory.Functor.comp (CategoryTheory.IsEquivalence.inverse F) F ≅ CategoryTheory.Functor.id D

  Composition inverse ⋙ F is isomorphic to the identity.

• functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.IsEquivalence.unitIso.hom.app X)) (CategoryTheory.IsEquivalence.counitIso.hom.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)

  The natural isomorphisms are inverse.

• )

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

@[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 : (CategoryTheory.Functor.id D).obj (F.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.IsEquivalence.unitIso.hom.app X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.counitIso.hom.app (F.obj X)) h) = h

instance CategoryTheory.IsEquivalence.ofEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ≌ D) : CategoryTheory.IsEquivalence F.functor

Equations

• CategoryTheory.IsEquivalence.ofEquivalence F = CategoryTheory.IsEquivalence.mk' F.inverse F.unitIso F.counitIso

instance CategoryTheory.IsEquivalence.ofEquivalenceInverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ≌ D) : CategoryTheory.IsEquivalence F.inverse

Equations

• CategoryTheory.IsEquivalence.ofEquivalenceInverse F = CategoryTheory.IsEquivalence.ofEquivalence F.symm

def CategoryTheory.IsEquivalence.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (G : CategoryTheory.Functor D C) (η : CategoryTheory.Functor.id C ≅ CategoryTheory.Functor.comp F G) (ε : CategoryTheory.Functor.comp G F ≅ CategoryTheory.Functor.id D) : CategoryTheory.IsEquivalence F

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

• CategoryTheory.IsEquivalence.mk G η ε = CategoryTheory.IsEquivalence.mk' G (CategoryTheory.Equivalence.adjointifyη η ε) ε

def CategoryTheory.Functor.asEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] : C ≌ D

Interpret a functor that is an equivalence as an equivalence.

Equations

• CategoryTheory.Functor.asEquivalence F = CategoryTheory.Equivalence.mk' F (CategoryTheory.IsEquivalence.inverse F) CategoryTheory.IsEquivalence.unitIso CategoryTheory.IsEquivalence.counitIso

instance CategoryTheory.Functor.isEquivalenceRefl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.IsEquivalence (CategoryTheory.Functor.id C)

Equations

• CategoryTheory.Functor.isEquivalenceRefl = CategoryTheory.IsEquivalence.ofEquivalence CategoryTheory.Equivalence.refl

def CategoryTheory.Functor.inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] : CategoryTheory.Functor D C

The inverse functor of a functor that is an equivalence.

Equations

• CategoryTheory.Functor.inv F = CategoryTheory.IsEquivalence.inverse F

instance CategoryTheory.Functor.isEquivalenceInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] : CategoryTheory.IsEquivalence (CategoryTheory.Functor.inv F)

Equations

• CategoryTheory.Functor.isEquivalenceInv F = CategoryTheory.IsEquivalence.ofEquivalence (CategoryTheory.Functor.asEquivalence F).symm

@[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) [CategoryTheory.IsEquivalence F] : (CategoryTheory.Functor.asEquivalence F).functor = F

@[simp]

theorem CategoryTheory.Functor.asEquivalence_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] : (CategoryTheory.Functor.asEquivalence F).inverse = CategoryTheory.Functor.inv F

@[simp]

theorem CategoryTheory.Functor.asEquivalence_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.IsEquivalence F] : (CategoryTheory.Functor.asEquivalence F).unitIso = CategoryTheory.IsEquivalence.unitIso

@[simp]

theorem CategoryTheory.Functor.asEquivalence_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.IsEquivalence F] : (CategoryTheory.Functor.asEquivalence F).counitIso = CategoryTheory.IsEquivalence.counitIso

@[simp]

theorem CategoryTheory.Functor.inv_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] : CategoryTheory.Functor.inv (CategoryTheory.Functor.inv F) = F

instance CategoryTheory.Functor.isEquivalenceTrans {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) [CategoryTheory.IsEquivalence F] [CategoryTheory.IsEquivalence G] : CategoryTheory.IsEquivalence (CategoryTheory.Functor.comp F G)

Equations

• CategoryTheory.Functor.isEquivalenceTrans F G = CategoryTheory.IsEquivalence.ofEquivalence ((CategoryTheory.Functor.asEquivalence F).trans (CategoryTheory.Functor.asEquivalence G))

@[simp]

theorem CategoryTheory.Equivalence.functor_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : C ≌ D) : CategoryTheory.Functor.inv E.functor = E.inverse

@[simp]

theorem CategoryTheory.Equivalence.inverse_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : C ≌ D) : CategoryTheory.Functor.inv E.inverse = E.functor

@[simp]

theorem CategoryTheory.Equivalence.functor_asEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : C ≌ D) : CategoryTheory.Functor.asEquivalence E.functor = E

@[simp]

theorem CategoryTheory.Equivalence.inverse_asEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : C ≌ D) : CategoryTheory.Functor.asEquivalence E.inverse = E.symm

@[simp]

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) [CategoryTheory.IsEquivalence F] (X : D) (Y : D) (f : X ⟶ Y) : F.map ((CategoryTheory.Functor.inv F).map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.asEquivalence F).counit.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Functor.asEquivalence F).counitInv.app Y))

@[simp]

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) [CategoryTheory.IsEquivalence F] (X : C) (Y : C) (f : X ⟶ Y) : (CategoryTheory.Functor.inv F).map (F.map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.asEquivalence F).unitInv.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Functor.asEquivalence F).unit.app Y))

@[simp]

theorem CategoryTheory.IsEquivalence.ofIso_inverse {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) : CategoryTheory.IsEquivalence.inverse G = CategoryTheory.IsEquivalence.inverse F

@[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).map (e.hom.app X))

@[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).map (e.inv.app X)) (CategoryTheory.IsEquivalence.unitIso.inv.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).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).obj X)) (CategoryTheory.IsEquivalence.counitIso.hom.app X)

def CategoryTheory.IsEquivalence.ofIso {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) : CategoryTheory.IsEquivalence 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

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

theorem CategoryTheory.IsEquivalence.ofIso_trans {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} {H : CategoryTheory.Functor C D} (e : F ≅ G) (e' : G ≅ H) (hF : CategoryTheory.IsEquivalence F) : CategoryTheory.IsEquivalence.ofIso e' (CategoryTheory.IsEquivalence.ofIso e hF) = CategoryTheory.IsEquivalence.ofIso (e ≪≫ e') hF

Compatibility of ofIso with the composition of isomorphisms of functors

theorem CategoryTheory.IsEquivalence.ofIso_refl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (hF : CategoryTheory.IsEquivalence F) : CategoryTheory.IsEquivalence.ofIso (CategoryTheory.Iso.refl F) hF = hF

Compatibility of ofIso with identity isomorphisms of functors

@[simp]

theorem CategoryTheory.IsEquivalence.equivOfIso_symm_apply {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 G) : ↑(CategoryTheory.IsEquivalence.equivOfIso e).symm hF = CategoryTheory.IsEquivalence.ofIso e.symm hF

@[simp]

theorem CategoryTheory.IsEquivalence.equivOfIso_apply {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) : ↑(CategoryTheory.IsEquivalence.equivOfIso e) hF = CategoryTheory.IsEquivalence.ofIso e hF

def CategoryTheory.IsEquivalence.equivOfIso {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) : CategoryTheory.IsEquivalence F ≃ CategoryTheory.IsEquivalence G

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.

def 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) (hG : CategoryTheory.IsEquivalence G) : CategoryTheory.IsEquivalence (CategoryTheory.Functor.comp F G) → CategoryTheory.IsEquivalence F

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.

def 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) (hF : CategoryTheory.IsEquivalence F) : CategoryTheory.IsEquivalence (CategoryTheory.Functor.comp F G) → CategoryTheory.IsEquivalence G

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.

theorem CategoryTheory.Equivalence.essSurj_of_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] : CategoryTheory.EssSurj F

An equivalence is essentially surjective.

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

instance CategoryTheory.Equivalence.faithfulOfEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] : CategoryTheory.Faithful F

An equivalence is faithful.

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

Equations

• @CategoryTheory.Equivalence.faithfulOfEquivalence = @CategoryTheory.Equivalence.faithfulOfEquivalence.proof_1

instance CategoryTheory.Equivalence.fullOfEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] : CategoryTheory.Full F

An equivalence is full.

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

Equations

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

noncomputable def CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] [CategoryTheory.EssSurj F] : CategoryTheory.IsEquivalence F

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

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

Equations

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

@[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.map f = e.functor.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.map f = e.inverse.map g ↔ f = g

instance CategoryTheory.Equivalence.essSurjInducedFunctor {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D) : CategoryTheory.EssSurj (CategoryTheory.inducedFunctor ↑e)

Equations

• @CategoryTheory.Equivalence.essSurjInducedFunctor = @CategoryTheory.Equivalence.essSurjInducedFunctor.proof_1

noncomputable instance CategoryTheory.Equivalence.inducedFunctorOfEquiv {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D) : CategoryTheory.IsEquivalence (CategoryTheory.inducedFunctor ↑e)

Equations

• CategoryTheory.Equivalence.inducedFunctorOfEquiv e = CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj (CategoryTheory.inducedFunctor ↑e)

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) [CategoryTheory.Full F] [CategoryTheory.Faithful F] : CategoryTheory.IsEquivalence (CategoryTheory.Functor.toEssImage F)

Equations

• CategoryTheory.Equivalence.fullyFaithfulToEssImage F = CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj (CategoryTheory.Functor.toEssImage F)