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
• Functor.EssSurj: type class on a functor F containing the data of the preimages and the isomorphisms F.obj (preimage d) ≅ d.
• Functor.IsEquivalence: type class on a functor F which is full, faithful and essentially surjective.

Main results

• Equivalence.mk: upgrade an equivalence to a (half-)adjoint equivalence
• isEquivalence_iff_of_iso: when F and G are isomorphic functors, F is an equivalence iff G is.
• Functor.asEquivalenceFunctor: construction of an equivalence of categories from a functor F which satisfies the property F.IsEquivalence (i.e. F is full, faithful and essentially surjective).

Notation

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

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

An equivalence of categories.

We define an equivalence between C and D, with notation C ≌ D, as a half-adjoint equivalence: a pair of functors F : C ⥤ D and G : D ⥤ C with a unit η : 𝟭 C ≅ F ⋙ G and counit ε : G ⋙ F ≅ 𝟭 D, such that the natural isomorphisms η and ε satisfy the triangle law for F: namely, Fη ≫ εF = 𝟙 F. Or, in other words, the composite F ⟶ F ⋙ G ⋙ F ⟶ F is the identity.

In unit_inverse_comp, we show that this is sufficient to establish a full adjoint equivalence. I.e., the composite G ⟶ G ⋙ F ⋙ G ⟶ G is also the identity.

The triangle equation functor_unitIso_comp 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 either have to insert natural transformations like F ⟶ F𝟭 or abuse defeq.

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

  The forwards direction of an equivalence.

• inverse : Functor D C

  The backwards direction of an equivalence.

• unitIso : Functor.id C ≅ self.functor.comp self.inverse

  The composition functor ⋙ inverse is isomorphic to the identity.

• counitIso : self.inverse.comp self.functor ≅ Functor.id D

  The composition inverse ⋙ functor is isomorphic to the identity.

• functor_unitIso_comp (X : C) : CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryStruct.id (self.functor.obj X)

  The triangle law for the forwards direction of an equivalence: the unit and counit compose to the identity when whiskered along the forwards direction.

  We state this as a family of equalities among morphisms instead of an equality of natural transformations to avoid abusing defeq or inserting natural transformations like F ⟶ F𝟭.

• )

theorem CategoryTheory.Equivalence.ext {C : Type u₁} {D : Type u₂} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : Category.{v₂, u₂} D} {x y : C ≌ D} (functor : x.functor = y.functor) (inverse : x.inverse = y.inverse) (unitIso : x.unitIso ≍ y.unitIso) (counitIso : x.counitIso ≍ y.counitIso) : x = y

theorem CategoryTheory.Equivalence.ext_iff {C : Type u₁} {D : Type u₂} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : Category.{v₂, u₂} D} {x y : C ≌ D} : x = y ↔ x.functor = y.functor ∧ x.inverse = y.inverse ∧ x.unitIso ≍ y.unitIso ∧ x.counitIso ≍ y.counitIso

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

An equivalence of categories.

We define an equivalence between C and D, with notation C ≌ D, as a half-adjoint equivalence: a pair of functors F : C ⥤ D and G : D ⥤ C with a unit η : 𝟭 C ≅ F ⋙ G and counit ε : G ⋙ F ≅ 𝟭 D, such that the natural isomorphisms η and ε satisfy the triangle law for F: namely, Fη ≫ εF = 𝟙 F. Or, in other words, the composite F ⟶ F ⋙ G ⋙ F ⟶ F is the identity.

In unit_inverse_comp, we show that this is sufficient to establish a full adjoint equivalence. I.e., the composite G ⟶ G ⋙ F ⋙ G ⟶ G is also the identity.

The triangle equation functor_unitIso_comp 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 either have to insert natural transformations like F ⟶ F𝟭 or abuse defeq.

@[reducible, inline]

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

The unit of an equivalence of categories.

@[reducible, inline]

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

The inverse of the unit of an equivalence of categories.

@[reducible, inline]

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

The counit of an equivalence of categories.

@[reducible, inline]

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

The inverse of the counit of an equivalence of categories.

theorem CategoryTheory.Equivalence.unitIso_hom_inv_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryStruct.comp (e.unit.app X) (e.unitInv.app X) = CategoryStruct.id X

theorem CategoryTheory.Equivalence.unitIso_hom_inv_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (e.unit.app X) (CategoryStruct.comp (e.unitInv.app X) h) = h

theorem CategoryTheory.Equivalence.unitIso_inv_hom_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryStruct.comp (e.unitInv.app X) (e.unit.app X) = CategoryStruct.id (e.inverse.obj (e.functor.obj X))

theorem CategoryTheory.Equivalence.unitIso_inv_hom_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : C} (h : e.inverse.obj (e.functor.obj X) ⟶ Z) : CategoryStruct.comp (e.unitInv.app X) (CategoryStruct.comp (e.unit.app X) h) = h

theorem CategoryTheory.Equivalence.counitIso_hom_inv_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryStruct.comp (e.counit.app Y) (e.counitInv.app Y) = CategoryStruct.id (e.functor.obj (e.inverse.obj Y))

theorem CategoryTheory.Equivalence.counitIso_hom_inv_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) : CategoryStruct.comp (e.counit.app Y) (CategoryStruct.comp (e.counitInv.app Y) h) = h

theorem CategoryTheory.Equivalence.counitIso_inv_hom_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryStruct.comp (e.counitInv.app Y) (e.counit.app Y) = CategoryStruct.id Y

theorem CategoryTheory.Equivalence.counitIso_inv_hom_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : D} (h : Y ⟶ Z) : CategoryStruct.comp (e.counitInv.app Y) (CategoryStruct.comp (e.counit.app Y) h) = h

@[instance_reducible]

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

@[implicit_reducible]

def CategoryTheory.Equivalence.mkHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ⟶ f.functor) : e ⟶ f

Promote a natural transformation e.functor ⟶ f.functor to a morphism in C ≌ D.

@[implicit_reducible]

def CategoryTheory.Equivalence.asNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} (η : e ⟶ f) : e.functor ⟶ f.functor

Recover a natural transformation between e.functor and f.functor from the data of a morphism e ⟶ f.

theorem CategoryTheory.Equivalence.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} {α β : e ⟶ f} (h : asNatTrans α = asNatTrans β) : α = β

theorem CategoryTheory.Equivalence.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} {α β : e ⟶ f} : α = β ↔ asNatTrans α = asNatTrans β

@[simp]

theorem CategoryTheory.Equivalence.mkHom_asNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ⟶ f.functor) : mkHom (asNatTrans η) = η

@[simp]

theorem CategoryTheory.Equivalence.asNatTrans_mkHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} (η : e ⟶ f) : asNatTrans (mkHom η) = η

@[simp]

theorem CategoryTheory.Equivalence.id_asNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e : C ≌ D} : asNatTrans (CategoryStruct.id e) = CategoryStruct.id e.functor

@[simp]

theorem CategoryTheory.Equivalence.comp_asNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f g : C ≌ D} (α : e ⟶ f) (β : f ⟶ g) : asNatTrans (CategoryStruct.comp α β) = CategoryStruct.comp (asNatTrans α) (asNatTrans β)

theorem CategoryTheory.Equivalence.comp_asNatTrans_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f g : C ≌ D} (α : e ⟶ f) (β : f ⟶ g) {Z : Functor C D} (h : g.functor ⟶ Z) : CategoryStruct.comp (asNatTrans (CategoryStruct.comp α β)) h = CategoryStruct.comp (asNatTrans α) (CategoryStruct.comp (asNatTrans β) h)

@[simp]

theorem CategoryTheory.Equivalence.mkHom_id_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e : C ≌ D} : mkHom (CategoryStruct.id e.functor) = CategoryStruct.id e

@[simp]

theorem CategoryTheory.Equivalence.mkHom_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f g : C ≌ D} (α : e.functor ⟶ f.functor) (β : f.functor ⟶ g.functor) : mkHom (CategoryStruct.comp α β) = CategoryStruct.comp (mkHom α) (mkHom β)

theorem CategoryTheory.Equivalence.mkHom_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f g : C ≌ D} (α : e.functor ⟶ f.functor) (β : f.functor ⟶ g.functor) {Z : C ≌ D} (h : g ⟶ Z) : CategoryStruct.comp (mkHom (CategoryStruct.comp α β)) h = CategoryStruct.comp (mkHom α) (CategoryStruct.comp (mkHom β) h)

@[implicit_reducible]

def CategoryTheory.Equivalence.mkIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ≅ f.functor) : e ≅ f

Construct an isomorphism in C ≌ D from a natural isomorphism between the functors of the equivalences.

@[simp]

theorem CategoryTheory.Equivalence.mkIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ≅ f.functor) : (mkIso η).hom = mkHom η.hom

@[simp]

theorem CategoryTheory.Equivalence.mkIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ≅ f.functor) : (mkIso η).inv = mkHom η.inv

@[implicit_reducible]

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

The functor functor that sends an equivalence of categories to its functor.

@[simp]

theorem CategoryTheory.Equivalence.functorFunctor_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : C ≌ D} (α : X✝ ⟶ Y✝) : (functorFunctor C D).map α = asNatTrans α

@[simp]

theorem CategoryTheory.Equivalence.functorFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (f : C ≌ D) : (functorFunctor C D).obj f = f.functor

While these abbreviations are convenient, they also cause some trouble, preventing structure projections from unfolding.

@[simp]

theorem CategoryTheory.Equivalence.Equivalence_mk'_unit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (functor : Functor C D) (inverse : Functor D C) (unit_iso : Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ Functor.id D) (f : ∀ (X : C), CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (functor : Functor C D) (inverse : Functor D C) (unit_iso : Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ Functor.id D) (f : ∀ (X : C), CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (functor : Functor C D) (inverse : Functor D C) (unit_iso : Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ Functor.id D) (f : ∀ (X : C), CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (functor : Functor C D) (inverse : Functor D C) (unit_iso : Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ Functor.id D) (f : ∀ (X : C), CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counitInv = counit_iso.inv

theorem CategoryTheory.Equivalence.counit_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : X ⟶ Y) : CategoryStruct.comp (e.functor.map (e.inverse.map f)) (e.counit.app Y) = CategoryStruct.comp (e.counit.app X) f

theorem CategoryTheory.Equivalence.counitInv_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : Y ⟶ X) {Z : D} (h : e.functor.obj (e.inverse.obj X) ⟶ Z) : CategoryStruct.comp (e.counitInv.app Y) (CategoryStruct.comp (e.functor.map (e.inverse.map f)) h) = CategoryStruct.comp f (CategoryStruct.comp (e.counitInv.app X) h)

theorem CategoryTheory.Equivalence.counit_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : X ⟶ Y) {Z : D} (h : Y ⟶ Z) : CategoryStruct.comp (e.functor.map (e.inverse.map f)) (CategoryStruct.comp (e.counit.app Y) h) = CategoryStruct.comp (e.counit.app X) (CategoryStruct.comp f h)

theorem CategoryTheory.Equivalence.counitInv_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : Y ⟶ X) : CategoryStruct.comp (e.counitInv.app Y) (e.functor.map (e.inverse.map f)) = CategoryStruct.comp f (e.counitInv.app X)

theorem CategoryTheory.Equivalence.unit_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (e.unit.app X) (e.inverse.map (e.functor.map f)) = CategoryStruct.comp f (e.unit.app Y)

theorem CategoryTheory.Equivalence.unit_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z) : CategoryStruct.comp (e.unit.app X) (CategoryStruct.comp (e.inverse.map (e.functor.map f)) h) = CategoryStruct.comp f (CategoryStruct.comp (e.unit.app Y) h)

theorem CategoryTheory.Equivalence.unitInv_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : Y ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (e.inverse.map (e.functor.map f)) (CategoryStruct.comp (e.unitInv.app X) h) = CategoryStruct.comp (e.unitInv.app Y) (CategoryStruct.comp f h)

theorem CategoryTheory.Equivalence.unitInv_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : Y ⟶ X) : CategoryStruct.comp (e.inverse.map (e.functor.map f)) (e.unitInv.app X) = CategoryStruct.comp (e.unitInv.app Y) f

@[simp]

theorem CategoryTheory.Equivalence.functor_unit_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) = CategoryStruct.id (e.functor.obj X)

@[simp]

theorem CategoryTheory.Equivalence.counitInv_functor_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (CategoryStruct.comp (e.functor.map (e.unitInv.app X)) h) = h

@[simp]

theorem CategoryTheory.Equivalence.functor_unit_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryStruct.comp (e.functor.map (e.unit.app X)) (CategoryStruct.comp (e.counit.app (e.functor.obj X)) h) = h

@[simp]

theorem CategoryTheory.Equivalence.counitInv_functor_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) = CategoryStruct.id (e.functor.obj X)

theorem CategoryTheory.Equivalence.counit_app_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)

theorem CategoryTheory.Equivalence.counitInv_app_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)

@[simp]

theorem CategoryTheory.Equivalence.unit_inverse_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) = 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (CategoryStruct.comp (e.unitInv.app (e.inverse.obj Y)) h) = h

@[simp]

theorem CategoryTheory.Equivalence.unit_inverse_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (CategoryStruct.comp (e.inverse.map (e.counit.app Y)) h) = h

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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) = CategoryStruct.id (e.inverse.obj Y)

theorem CategoryTheory.Equivalence.unit_app_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [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₁} [Category.{v₁, u₁} C] {D : Type u₂} [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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) : e.functor.map (e.inverse.map f) = CategoryStruct.comp (e.counit.app X) (CategoryStruct.comp f (e.counitInv.app Y))

theorem CategoryTheory.Equivalence.fun_inv_map_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) : CategoryStruct.comp (e.functor.map (e.inverse.map f)) h = CategoryStruct.comp (e.counit.app X) (CategoryStruct.comp f (CategoryStruct.comp (e.counitInv.app Y) h))

@[simp]

theorem CategoryTheory.Equivalence.inv_fun_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) : e.inverse.map (e.functor.map f) = CategoryStruct.comp (e.unitInv.app X) (CategoryStruct.comp f (e.unit.app Y))

theorem CategoryTheory.Equivalence.inv_fun_map_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z) : CategoryStruct.comp (e.inverse.map (e.functor.map f)) h = CategoryStruct.comp (e.unitInv.app X) (CategoryStruct.comp f (CategoryStruct.comp (e.unit.app Y) h))

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

Equivalence of categories is reflexive.

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Equivalence.refl_inverse {C : Type u₁} [Category.{v₁, u₁} C] : refl.inverse = Functor.id C

@[simp]

theorem CategoryTheory.Equivalence.refl_functor {C : Type u₁} [Category.{v₁, u₁} C] : refl.functor = Functor.id C

@[instance_reducible]

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

@[implicit_reducible]

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

Equivalence of categories is symmetric.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

Equivalence of categories is transitive.

@[simp]

theorem CategoryTheory.Equivalence.trans_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).functor = e.functor.comp f.functor

@[simp]

theorem CategoryTheory.Equivalence.trans_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).unitIso = e.unitIso ≪≫ Functor.isoWhiskerRight (e.functor.rightUnitor.symm ≪≫ e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm) e.inverse ≪≫ (e.functor.comp f.functor).associator f.inverse e.inverse

@[simp]

theorem CategoryTheory.Equivalence.trans_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).counitIso = ((f.inverse.comp e.inverse).associator e.functor f.functor).symm ≪≫ Functor.isoWhiskerRight (f.inverse.associator e.inverse e.functor ≪≫ f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor) f.functor ≪≫ f.counitIso

@[simp]

theorem CategoryTheory.Equivalence.trans_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).inverse = f.inverse.comp e.inverse

@[implicit_reducible]

def CategoryTheory.Equivalence.funInvIdAssoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor C E) : e.functor.comp (e.inverse.comp F) ≅ F

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

@[simp]

theorem CategoryTheory.Equivalence.funInvIdAssoc_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor C E) (X : C) : (e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)

@[implicit_reducible]

def CategoryTheory.Equivalence.invFunIdAssoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor D E) : e.inverse.comp (e.functor.comp F) ≅ F

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

@[simp]

theorem CategoryTheory.Equivalence.invFunIdAssoc_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor D E) (X : D) : (e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app X)

@[implicit_reducible]

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

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

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrLeft.inverse = (Functor.whiskeringLeft C D E).obj e.functor

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (X : Functor C E) : e.congrLeft.unitIso.inv.app X = (e.funInvIdAssoc X).hom

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (X : Functor D E) : e.congrLeft.counitIso.hom.app X = (e.invFunIdAssoc X).hom

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (X : Functor C E) : e.congrLeft.unitIso.hom.app X = (e.funInvIdAssoc X).inv

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (X : Functor D E) : e.congrLeft.counitIso.inv.app X = (e.invFunIdAssoc X).inv

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrLeft.functor = (Functor.whiskeringLeft D C E).obj e.inverse

@[implicit_reducible]

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

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

@[simp]

theorem CategoryTheory.Equivalence.congrRight_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (X : Functor E D) : e.congrRight.counitIso.inv.app X = CategoryStruct.comp X.rightUnitor.inv (CategoryStruct.comp (X.whiskerLeft e.counitIso.inv) (X.associator e.inverse e.functor).inv)

@[simp]

theorem CategoryTheory.Equivalence.congrRight_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrRight.functor = (Functor.whiskeringRight E C D).obj e.functor

@[simp]

theorem CategoryTheory.Equivalence.congrRight_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (X : Functor E D) : e.congrRight.counitIso.hom.app X = CategoryStruct.comp (X.associator e.inverse e.functor).hom (CategoryStruct.comp (X.whiskerLeft e.counitIso.hom) X.rightUnitor.hom)

@[simp]

theorem CategoryTheory.Equivalence.congrRight_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (X : Functor E C) : e.congrRight.unitIso.hom.app X = CategoryStruct.comp X.rightUnitor.inv (CategoryStruct.comp (X.whiskerLeft e.unitIso.hom) (X.associator e.functor e.inverse).hom)

@[simp]

theorem CategoryTheory.Equivalence.congrRight_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (X : Functor E C) : e.congrRight.unitIso.inv.app X = CategoryStruct.comp (X.associator e.functor e.inverse).inv (CategoryStruct.comp (X.whiskerLeft e.unitIso.inv) X.rightUnitor.hom)

@[simp]

theorem CategoryTheory.Equivalence.congrRight_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrRight.inverse = (Functor.whiskeringRight E D C).obj e.inverse

@[implicit_reducible]

def CategoryTheory.Equivalence.congrRightFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : Functor (C ≌ D) (Functor E C ≌ Functor E D)

Promoting Equivalence.congrRight to a functor.

@[simp]

theorem CategoryTheory.Equivalence.congrRightFunctor_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {e f : C ≌ D} (α : e ⟶ f) : (congrRightFunctor E).map α = mkHom ((Functor.whiskeringRight E C D).map (asNatTrans α))

@[simp]

theorem CategoryTheory.Equivalence.congrRightFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (e : C ≌ D) : (congrRightFunctor E).obj e = e.congrRight

@[simp]

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

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

@[simp]

theorem CategoryTheory.Equivalence.cancel_unitInv_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) : CategoryStruct.comp f (e.unitInv.app Y) = CategoryStruct.comp f' (e.unitInv.app Y) ↔ f = f'

@[simp]

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

@[simp]

theorem CategoryTheory.Equivalence.cancel_counit_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) : CategoryStruct.comp f (e.counit.app Y) = CategoryStruct.comp f' (e.counit.app Y) ↔ f = f'

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Equivalence.cancel_unit_right_assoc' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (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) : CategoryStruct.comp f (CategoryStruct.comp g (CategoryStruct.comp h (e.unit.app Z))) = CategoryStruct.comp f' (CategoryStruct.comp g' (CategoryStruct.comp h' (e.unit.app Z))) ↔ CategoryStruct.comp f (CategoryStruct.comp g h) = CategoryStruct.comp f' (CategoryStruct.comp g' h')

@[simp]

theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (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) : CategoryStruct.comp f (CategoryStruct.comp g (CategoryStruct.comp h (e.counitInv.app Z))) = CategoryStruct.comp f' (CategoryStruct.comp g' (CategoryStruct.comp h' (e.counitInv.app Z))) ↔ CategoryStruct.comp f (CategoryStruct.comp g h) = CategoryStruct.comp f' (CategoryStruct.comp g' h')

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

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

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

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

@[instance_reducible]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance CategoryTheory.Equivalence.essSurj_functor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.EssSurj

The functor of an equivalence of categories is essentially surjective.

instance CategoryTheory.Equivalence.essSurj_inverse {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.EssSurj

@[implicit_reducible]

def CategoryTheory.Equivalence.fullyFaithfulFunctor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.FullyFaithful

The functor of an equivalence of categories is fully faithful.

@[implicit_reducible]

def CategoryTheory.Equivalence.fullyFaithfulInverse {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.FullyFaithful

The inverse of an equivalence of categories is fully faithful.

instance CategoryTheory.Equivalence.faithful_functor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.Faithful

The functor of an equivalence of categories is faithful.

instance CategoryTheory.Equivalence.faithful_inverse {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.Faithful

instance CategoryTheory.Equivalence.full_functor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.Full

The functor of an equivalence of categories is full.

instance CategoryTheory.Equivalence.full_inverse {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.Full

@[implicit_reducible]

def CategoryTheory.Equivalence.changeFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) : C ≌ D

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.

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) : (e.changeFunctor iso).functor = G

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.hom.app X = CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.hom.app X)

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.hom.app X = CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.inv.app X = CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.inv.app X = CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) : (e.changeFunctor iso).inverse = e.inverse

theorem CategoryTheory.Equivalence.changeFunctor_refl {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.changeFunctor (Iso.refl e.functor) = e

Compatibility of changeFunctor with identity isomorphisms of functors

theorem CategoryTheory.Equivalence.changeFunctor_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G G' : 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

@[implicit_reducible]

def CategoryTheory.Equivalence.changeInverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) : C ≌ D

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.

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) : (e.changeInverse iso).functor = e.functor

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.hom.app X = CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.hom.app X = CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.inv.app X = CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.inv.app X = CategoryStruct.comp (iso.inv.app (e.functor.obj X)) (e.unitIso.inv.app X)

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) : (e.changeInverse iso).inverse = G

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

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

• faithful : F.Faithful
• full : F.Full
• essSurj : F.EssSurj

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

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

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

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.

@[implicit_reducible]

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

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

@[implicit_reducible]

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

Interpret a functor that is an equivalence as an equivalence.

@[simp]

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

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

theorem CategoryTheory.Functor.asEquivalence_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] (X : C) : F.asEquivalence.unitIso.hom.app X = F.preimage (F.objObjPreimageIso (F.obj X)).inv

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

theorem CategoryTheory.Functor.asEquivalence_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] (X : C) : F.asEquivalence.unitIso.inv.app X = F.preimage (F.objObjPreimageIso (F.obj X)).hom

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

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

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

instance CategoryTheory.Functor.isEquivalence_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [F.IsEquivalence] [G.IsEquivalence] : (F.comp G).IsEquivalence

instance CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) [F.IsEquivalence] : ((whiskeringLeft C D E).obj F).IsEquivalence

instance CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) [F.IsEquivalence] : ((whiskeringRight E C D).obj F).IsEquivalence

@[simp]

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

@[simp]

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

theorem CategoryTheory.Functor.isEquivalence_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (e : F ≅ G) [F.IsEquivalence] : G.IsEquivalence

theorem CategoryTheory.Functor.isEquivalence_iff_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (e : F ≅ G) : F.IsEquivalence ↔ G.IsEquivalence

theorem CategoryTheory.Functor.isEquivalence_of_comp_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor C D) (G : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor C D) (G : 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.

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

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

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

@[implicit_reducible]

def CategoryTheory.ObjectProperty.fullSubcategoryCongr {C : Type u₁} [Category.{v₁, u₁} C] {P P' : ObjectProperty C} (h : P = P') : P.FullSubcategory ≌ P'.FullSubcategory

An equality of properties of objects of a category C induces an equivalence of the respective induced full subcategories of C.

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryCongr_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {P P' : ObjectProperty C} (h : P = P') : (fullSubcategoryCongr h).unitIso = Iso.refl (Functor.id P.FullSubcategory)

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryCongr_functor {C : Type u₁} [Category.{v₁, u₁} C] {P P' : ObjectProperty C} (h : P = P') : (fullSubcategoryCongr h).functor = ιOfLE ⋯

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryCongr_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {P P' : ObjectProperty C} (h : P = P') : (fullSubcategoryCongr h).counitIso = Iso.refl ((ιOfLE ⋯).comp (ιOfLE ⋯))

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryCongr_inverse {C : Type u₁} [Category.{v₁, u₁} C] {P P' : ObjectProperty C} (h : P = P') : (fullSubcategoryCongr h).inverse = ιOfLE ⋯

@[implicit_reducible]

def CategoryTheory.Iso.compInverseIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) : F.comp H.inverse ≅ G

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

@[simp]

theorem CategoryTheory.Iso.compInverseIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.inv.app X = 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.hom.app X = CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))

@[implicit_reducible]

def CategoryTheory.Iso.isoCompInverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) : G ≅ F.comp H.inverse

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

@[simp]

theorem CategoryTheory.Iso.isoCompInverse_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.inv.app X = 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.hom.app X = CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.hom.app X))

@[implicit_reducible]

def CategoryTheory.Iso.inverseCompIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) : G.inverse.comp F ≅ H

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

@[simp]

theorem CategoryTheory.Iso.inverseCompIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.hom.app X = CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))

@[simp]

theorem CategoryTheory.Iso.inverseCompIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.inv.app X = CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj X))

@[implicit_reducible]

def CategoryTheory.Iso.isoInverseComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) : H ≅ G.inverse.comp F

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

@[simp]

theorem CategoryTheory.Iso.isoInverseComp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.inv.app X = 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.hom.app X = CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))

@[implicit_reducible]

def CategoryTheory.Iso.isoInverseOfIsoFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) : G.inverse ≅ G'.inverse

As a special case, given two equivalences G and G' between the same categories, construct an isomorphism G.inverse ≅ G.inverse from an isomorphism G.functor ≅ G.functor.

@[simp]

theorem CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.hom.app X = CategoryStruct.comp (G'.unitIso.hom.app (G.inverse.obj X)) (CategoryStruct.comp (G'.inverse.map (i.inv.app (G.inverse.obj X))) (G'.inverse.map (G.counitIso.hom.app X)))

@[simp]

theorem CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.inv.app X = CategoryStruct.comp (G'.inverse.map (G.counitIso.inv.app X)) (CategoryStruct.comp (G'.inverse.map (i.hom.app (G.inverse.obj X))) (G'.unitIso.inv.app (G.inverse.obj X)))

@[implicit_reducible]

def CategoryTheory.Iso.isoFunctorOfIsoInverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) : G.functor ≅ G'.functor

As a special case, given two equivalences G and G' between the same categories, construct an isomorphism G.functor ≅ G.functor from an isomorphism G.inverse ≅ G.inverse.

@[simp]

theorem CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.hom.app X = CategoryStruct.comp (G'.counitIso.inv.app (G.functor.obj X)) (CategoryStruct.comp (G'.functor.map (i.inv.app (G.functor.obj X))) (G'.functor.map (G.unitIso.inv.app X)))

@[simp]

theorem CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.inv.app X = CategoryStruct.comp (G'.functor.map (G.unitIso.hom.app X)) (CategoryStruct.comp (G'.functor.map (i.hom.app (G.functor.obj X))) (G'.counitIso.hom.app (G.functor.obj X)))

@[simp]

theorem CategoryTheory.Iso.isoFunctorOfIsoInverse_isoInverseOfIsoFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) : i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i

Sanity check: isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i) is just i.

@[simp]

theorem CategoryTheory.Iso.isoInverseOfIsoFunctor_isoFunctorOfIsoInverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) : i.isoFunctorOfIsoInverse.isoInverseOfIsoFunctor = i