# 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.

source
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𝟭`.

- )

Instances For

source
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
source
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
source
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.

Equations

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

Instances For

source
@[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.

Equations

- e.unit = e.unitIso.hom

Instances For

source
@[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.

Equations

- e.counit = e.counitIso.hom

Instances For

source
@[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.

Equations

- e.unitInv = e.unitIso.inv

Instances For

source
@[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.

Equations

- e.counitInv = e.counitIso.inv

Instances For

source
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)
Equations

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

source
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`.

Equations

- CategoryTheory.Equivalence.mkHom η = η

Instances For

source
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`.

Equations

- CategoryTheory.Equivalence.asNatTrans η = η

Instances For

source
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 β) :
α = β
source
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 β
source
@[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 η) = η
source
@[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 η) = η
source
@[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
source
@[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 β)
source
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)
source
@[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
source
@[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 β)
source
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)
source
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.

Equations

- CategoryTheory.Equivalence.mkIso η = { hom := CategoryTheory.Equivalence.mkHom η.hom, inv := CategoryTheory.Equivalence.mkHom η.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source
@[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
source
@[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
source
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.

Equations

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

Instances For

source
@[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
source
@[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 α
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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)
source
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)
source
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)
source
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 : X ⟶ Y) :
CategoryStruct.comp (e.counitInv.app X) (e.functor.map (e.inverse.map f)) = CategoryStruct.comp f (e.counitInv.app Y)
source
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 : X ⟶ Y) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) :
CategoryStruct.comp (e.counitInv.app X) (CategoryStruct.comp (e.functor.map (e.inverse.map f)) h) = CategoryStruct.comp f (CategoryStruct.comp (e.counitInv.app Y) h)
source
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 : X ⟶ Y) :
CategoryStruct.comp (e.inverse.map (e.functor.map f)) (e.unitInv.app Y) = CategoryStruct.comp (e.unitInv.app X) f
source
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 : X ⟶ Y) {Z : C} (h : Y ⟶ Z) :
CategoryStruct.comp (e.inverse.map (e.functor.map f)) (CategoryStruct.comp (e.unitInv.app Y) h) = CategoryStruct.comp (e.unitInv.app X) (CategoryStruct.comp f h)
source
@[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)
source
@[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
source
@[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)
source
@[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
source
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)
source
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)
source
@[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

source
@[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
source
@[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)
source
@[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
source
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)
source
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)
source
@[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))
source
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))
source
@[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))
source
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))
source
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`.

Equations

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

Instances For

source
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)
source
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
source
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`.

Equations

- CategoryTheory.Equivalence.mk F G η ε = { functor := F, inverse := G, unitIso := CategoryTheory.Equivalence.adjointifyη η ε, counitIso := ε, functor_unitIso_comp := ⋯ }

Instances For

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

Equivalence of categories is reflexive.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Equivalence.refl_counitIso {C : Type u₁} [Category.{v₁, u₁} C] :
refl.counitIso = Iso.refl ((Functor.id C).comp (Functor.id C))
source
@[simp]
theorem CategoryTheory.Equivalence.refl_functor {C : Type u₁} [Category.{v₁, u₁} C] :
refl.functor = Functor.id C
source
@[simp]
theorem CategoryTheory.Equivalence.refl_unitIso {C : Type u₁} [Category.{v₁, u₁} C] :
refl.unitIso = Iso.refl (Functor.id C)
source
@[simp]
theorem CategoryTheory.Equivalence.refl_inverse {C : Type u₁} [Category.{v₁, u₁} C] :
refl.inverse = Functor.id C
source
instance CategoryTheory.Equivalence.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] :
Inhabited (C ≌ C)
Equations

- CategoryTheory.Equivalence.instInhabited = { default := CategoryTheory.Equivalence.refl }

source
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.

Equations

- e.symm = { functor := e.inverse, inverse := e.functor, unitIso := e.counitIso.symm, counitIso := e.unitIso.symm, functor_unitIso_comp := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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.

Equations

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

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
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.

Equations

- e.funInvIdAssoc F = (e.functor.associator e.inverse F).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight e.unitIso.symm F ≪≫ F.leftUnitor

Instances For

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

Equations

- e.invFunIdAssoc F = (e.inverse.associator e.functor F).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight e.counitIso F ≪≫ F.leftUnitor

Instances For

source
@[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)
source
@[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)
source
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`.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_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) :
e.congrLeft.unitIso = NatIso.ofComponents (fun (F : Functor C E) => (e.funInvIdAssoc F).symm) ⋯
source
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_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) :
e.congrLeft.counitIso = NatIso.ofComponents (fun (F : Functor D E) => e.invFunIdAssoc F) ⋯
source
@[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
source
@[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
source
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`.

Equations

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

Instances For

source
@[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
source
@[simp]
theorem CategoryTheory.Equivalence.congrRight_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) :
e.congrRight.counitIso = NatIso.ofComponents (fun (F : Functor E D) => F.associator e.inverse e.functor ≪≫ F.isoWhiskerLeft e.counitIso ≪≫ F.rightUnitor) ⋯
source
@[simp]
theorem CategoryTheory.Equivalence.congrRight_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) :
e.congrRight.unitIso = NatIso.ofComponents (fun (F : Functor E C) => F.rightUnitor.symm ≪≫ F.isoWhiskerLeft e.unitIso ≪≫ F.associator e.functor e.inverse) ⋯
source
@[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
source
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.

Equations

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

Instances For

source
@[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
source
@[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 α))
source
@[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'
source
@[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'
source
@[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'
source
@[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'
source
@[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'
source
@[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'
source
@[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')
source
@[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')
source
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.

Equations

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

Instances For

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

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

Equations

- e.pow (Int.ofNat n) = e.powNat n
- e.pow (Int.negSucc n) = e.symm.powNat (n + 1)

Instances For

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

- CategoryTheory.Equivalence.instPowInt = { pow := CategoryTheory.Equivalence.pow }

source
@[simp]
theorem CategoryTheory.Equivalence.pow_zero {C : Type u₁} [Category.{v₁, u₁} C] (e : C ≌ C) :
e ^ 0 = refl
source
@[simp]
theorem CategoryTheory.Equivalence.pow_one {C : Type u₁} [Category.{v₁, u₁} C] (e : C ≌ C) :
e ^ 1 = e
source
@[simp]
theorem CategoryTheory.Equivalence.pow_neg_one {C : Type u₁} [Category.{v₁, u₁} C] (e : C ≌ C) :
e ^ (-1) = e.symm
source
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.

source
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
source
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.

Equations

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

Instances For

source
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.

Equations

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

Instances For

source
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.

source
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
source
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.

source
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
source
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`.

Equations

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

Instances For

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

source
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

source
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`.

Equations

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

Instances For

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

Instances

source
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
source
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
source
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.

source
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.

Equations

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

Instances For

source
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.

Equations

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

Instances For

source
@[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
source
instance CategoryTheory.Functor.isEquivalence_refl {C : Type u₁} [Category.{v₁, u₁} C] :
(Functor.id C).IsEquivalence
source
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
source
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
source
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
source
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
source
@[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))
source
@[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))
source
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
source
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
source
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.{u_2, 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.

source
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.{u_2, 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.

source
instance CategoryTheory.Equivalence.essSurjInducedFunctor {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D) :
(inducedFunctor ⇑e).EssSurj
source
instance CategoryTheory.Equivalence.inducedFunctorOfEquiv {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D) :
(inducedFunctor ⇑e).IsEquivalence
source
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
source
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`.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.ObjectProperty.fullSubcategoryCongr_inverse {C : Type u₁} [Category.{v₁, u₁} C] {P P' : ObjectProperty C} (h : P = P') :
(fullSubcategoryCongr h).inverse = ιOfLE ⋯
source
@[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 ⋯))
source
@[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)
source
@[simp]
theorem CategoryTheory.ObjectProperty.fullSubcategoryCongr_functor {C : Type u₁} [Category.{v₁, u₁} C] {P P' : ObjectProperty C} (h : P = P') :
(fullSubcategoryCongr h).functor = ιOfLE ⋯
source
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`.

Equations

- i.compInverseIso = CategoryTheory.Functor.isoWhiskerRight i H.inverse ≪≫ G.associator H.functor H.inverse ≪≫ G.isoWhiskerLeft H.unitIso.symm ≪≫ G.rightUnitor

Instances For

source
@[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))
source
@[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))
source
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`.

Equations

- i.isoCompInverse = G.rightUnitor.symm ≪≫ G.isoWhiskerLeft H.unitIso ≪≫ (G.associator H.functor H.inverse).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight i H.inverse

Instances For

source
@[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))
source
@[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))
source
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`.

Equations

- i.inverseCompIso = G.inverse.isoWhiskerLeft i ≪≫ (G.inverse.associator G.functor H).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight G.counitIso H ≪≫ H.leftUnitor

Instances For

source
@[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))
source
@[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))
source
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`.

Equations

- i.isoInverseComp = H.leftUnitor.symm ≪≫ CategoryTheory.Functor.isoWhiskerRight G.counitIso.symm H ≪≫ G.inverse.associator G.functor H ≪≫ G.inverse.isoWhiskerLeft i

Instances For

source
@[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))
source
@[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))
source
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`.

Equations

- i.isoInverseOfIsoFunctor = ((G.inverse.isoWhiskerLeft i).symm ≪≫ G.counitIso).isoCompInverse ≪≫ G'.inverse.leftUnitor

Instances For

source
@[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)))
source
@[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)))
source
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`.

Equations

- i.isoFunctorOfIsoInverse = i.isoInverseOfIsoFunctor

Instances For

source
@[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)))
source
@[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)))
source
@[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`.

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